Haskell Counted List Type

Question

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.

Answer 1

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

Answer 2

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