Haskell Counted List Type
-
20-09-2019 - |
Pergunta
Então, apenas por diversão, eu tenho jogado com um tipo de lista de contagem em Haskell, usando números de Peano e construtores inteligentes.
Tipo-seguro head
e tail
Parece muito legal para mim.
E acho que atingi o limite do que sei fazer
{-# 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
(Desculpe por quaisquer erros de transcrição - a máquina que escrevi originalmente isso no meu compilador Haskell está atualmente inativo).
A maior parte do que fiz compila sem um problema, mas eu encontro problemas com ofList
e filter
. Acho que entendo o porquê - quando digo ofList :: [a] -> CountedList n a
, Eu estou dizendo ofList :: forall n . [a] -> CountedList n a
- que a lista criada pode ser do tipo de contagem desejado. O que eu quero escrever é o equivalente ao tipo pseudo ofList :: exists n . [a] -> CountedList n a
, mas eu não sei como.
Existe uma solução alternativa que me deixaria escrever ofList
e filter
Funções como estou imaginando ou atingi o limite do que posso fazer com isso? Tenho a sensação de que há algum truque com tipos existenciais que estou perdendo.
Solução
Você não pode escrever
ofList :: [a] -> (exists n. CountedList n a) -- wrong
Mas você pode escrever
withCountedList :: [a] -> (forall n. CountedList n a -> b) -> b
e passar uma função que representa o que você teria feito com o resultado de ofList
, desde que seu tipo seja independente do comprimento da lista.
A propósito, você pode garantir o invariante que o tipo de lista corresponda ao seu comprimento no sistema de tipos e não depender de construtores inteligentes:
{-# LANGUAGE GADTs #-}
data CountedList n a where
Empty :: CountedList Zero a
Cons :: a -> CountedList n a -> CountedList (Succ n) a
Outras dicas
Você não pode definir ofList
ou filter
Dessa forma, porque eles estão confundindo verificações no nível do tipo com valores de tempo de execução. Em particular, no tipo do resultado, CountedList n a
, o tipo n
deve ser determinado no tempo de compilação. O desejo implícito é que n
deve ser proporcional ao comprimento da lista que é o primeiro argumento. Mas isso claramente não pode ser conhecido até o tempo de execução.
Agora, pode ser possível definir um TypeClass, digamos contado e, em seguida, (com a extensão Haskell apropriada), defina isso como:
ofList :: [a] -> (forall n. (CountedListable CountedList n) => CountedList n a)
Mas você teria dificuldade em fazer qualquer coisa com esse resultado, já que as únicas operações que CountedListable
poderia apoiar seria extrair a contagem. Você não poderia, dizer, pegue o head
de tal valor porque o chefe não poderia ser definido para todas as instâncias de CountedListable