simbolos - listas infinitas haskell

Haskell cuenta el tipo de lista

Question

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

La head y la tail seguras para los tipos 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

(perdón por los errores de transcripción: la máquina en la que escribí esto originalmente con mi compilador Haskell está inactiva).

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

¿Hay alguna solución que me permita escribir funciones de ofList y filter como lo 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 los tipos existenciales que me estoy perdiendo.

Answer 1

No puede definir ofList o filter esta manera porque confunden las verificaciones de nivel de tipo con los valores de tiempo de ejecución. En particular, en el tipo del resultado, CountedList na , el tipo n debe determinarse en el momento de la 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 Counted, y luego (con la extensión Haskell apropiada), definir estos como:

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

Pero le resultaría difícil hacer algo con tal resultado, ya que las únicas operaciones que CountedListable podría admitir serían la extracción del conteo. No podría, digamos, obtener el head de tal valor porque el encabezado no podría definirse para todas las instancias de CountedListable

Answer 2

No puedes escribir

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

pero puedes escribir

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

y ofList una función que represente lo que ofList hecho con el resultado de ofList , siempre que su tipo sea independiente de la longitud de la lista.

Por cierto, puedes asegurarte de que el tipo de una lista corresponda a su longitud en el sistema de tipos, y no confiar en los constructores inteligentes:

{-# LANGUAGE GADTs #-}
data CountedList n a where
Empty :: CountedList Zero a
Cons :: a -> CountedList n a -> CountedList (Succ n) a