Haskell contó tipo de lista

Question

Por lo tanto, sólo por diversión, he estado jugando con un tipo CountedList en Haskell, el uso de números de Peano y constructores inteligentes .

head de tipo seguro y tail sólo parecen realmente bueno para mí.

Y creo que he llegado al límite de lo que sé cómo hacerlo

{-# 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 compila w / o un problema, pero que tenga problemas con ofList y filter. Creo que entiendo por qué - cuando digo ofList :: [a] -> CountedList n a, estoy diciendo ofList :: forall n . [a] -> CountedList n a - que la lista creada puede ser de cualquier tipo de conteo deseada. Lo que yo quiero escribir es el equivalente de la ofList :: exists n . [a] -> CountedList n a tipo pseudo, pero no sé cómo.

¿Hay una solución que me permitiera escribir funciones ofList y filter que estoy imaginando, o he alcanzado el límite de lo que puedo hacer con esto? Tengo la sensación de que hay algo de truco con tipos existenciales 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 pasarlo una función que representa lo que habría hecho con el resultado de ofList, siempre que su tipo es 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 se puede definir ofList o filter esta manera debido a que son de confusión controles de nivel de tipo con valores en tiempo de ejecución. En particular, en el tipo del resultado, CountedList n a, el tipo n debe ser determinado 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 que claramente no puede conocerse hasta en tiempo de ejecución.

Ahora, puede ser que sea posible definir una clase de tipos, digamos contados, y luego (con la extensión apropiada Haskell), definirlos como:

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

Sin embargo, usted tendría dificultades para hacer cualquier cosa con tal resultado, ya que las únicas operaciones que CountedListable podría apoyar sería extraer el recuento. 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