Haskell listó tipo

Question

Así que, solo por diversión, he estado jugando con un tipo CountedList en Haskell, usando los números de Peano y smart constructors.

Tipo seguro head y tail me parecen realmente geniales.

Y creo que he llegado al límite de lo que sé hacer

{-# LANGUAGE EmptyDataDecls #-} 
module CountedList (
    Zero, Succ, CountedList, 
    toList, ofList, 
    empty, cons, uncons, 
    head, tail, 
    fmap, map, foldl, foldr, filter 
) where 

import qualified List (foldr, foldl, filter) 
import Prelude hiding (map, head, foldl, foldr, tail, filter) 

data Zero 
data Succ n 
data CountedList n a = CL [a] 

toList :: CountedList n a -> [a] 
toList (CL as) = as 

ofList :: [a] -> CountedList n a 
ofList [] = empty 
ofList (a:as) = cons a $ ofList as 

empty :: CountedList Zero a 
empty = CL [] 

cons :: a -> CountedList n a -> CountedList (Succ n) a 
cons a = CL . (a:) . toList 

uncons :: CountedList (Succ n) a -> (a, CountedList n a) 
uncons (CL (a:as)) = (a, CL as) 

head :: CountedList (Succ n) a -> a 
head = fst . uncons 

tail :: CountedList (Succ n) a -> CountedList n a 
tail = snd . uncons 

instance Functor (CountedList n) where 
    fmap f = CL . fmap f . toList 

map :: (a -> b) -> CountedList n a -> CountedList n b 
map = fmap 

foldl :: (a -> b -> a) -> a -> CountedList n b -> a 
foldl f a = List.foldl f a . toList 

foldr :: (a -> b -> b) -> b -> CountedList n a -> b 
foldr f b = List.foldr f b . toList 

filter :: (a -> Bool) -> CountedList n a -> CountedList m a 
filter p = ofList . List.filter p . toList 

(lo siento por los errores de transcripción - la máquina que originalmente escribió esto en w/mi compilador de Haskell es actualmente abajo) .

La mayor parte de lo que he hecho se compila sin problemas, pero tengo problemas con ofList y filter. Creo que entiendo por qué, cuando digo ofList :: [a] -> CountedList n a, digo ofList :: forall n . [a] -> CountedList n a, que la lista creada puede ser del tipo de recuento deseado. Lo que quiero escribir es el equivalente al pseudo tipo ofList :: exists n . [a] -> CountedList n a, pero no sé cómo.

¿Hay alguna solución que me permita escribir ofList y filter funciones como las que estoy imaginando, o he llegado al límite de lo que puedo hacer con esto? Tengo la sensación de que hay un truco con existential types que me falta.

Answer 1

No se puede escribir

ofList :: [a] -> (exists n. CountedList n a) -- wrong 

pero se puede escribir

withCountedList :: [a] -> (forall n. CountedList n a -> b) -> b 

y le pasa una función que representa lo que habría hecho con el resultado de ofList, siempre que su tipo sea independiente de la longitud de la lista.

Por cierto, se puede asegurar el invariante que el tipo de una lista corresponde a su longitud en el sistema de tipos, y no depender de constructores inteligentes:

{-# LANGUAGE GADTs #-} 

data CountedList n a where 
    Empty :: CountedList Zero a 
    Cons :: a -> CountedList n a -> CountedList (Succ n) a 

Answer 2

No puede definir ofList o filter de esta manera porque están confundiendo las comprobaciones de tipo de nivel con los valores de tiempo de ejecución. En particular, en el tipo del resultado, CountedList n a, el tipo n se debe determinar en tiempo de compilación. El deseo implícito es que n debe ser proporcional a la longitud de la lista que es el primer argumento. Pero eso claramente no se puede saber hasta el tiempo de ejecución.

Ahora, podría ser posible definir una clase de tipos, digamos contado, y luego (con la extensión apropiada Haskell), define estos como:

ofList :: [a] -> (forall n. (CountedListable CountedList n) => CountedList n a) 

pero tendría dificultades para hacer cualquier cosa con tal resultado, ya que las únicas operaciones que CountedListable podrían soportar serían la extracción del conteo. No se podía, por ejemplo obtener el head de un valor tal, porque la cabeza no podía definirse para todas las instancias de CountedListable