type de liste comptait Haskell

Question

Alors, juste pour le plaisir, je joue avec un type de CountedList en Haskell, en utilisant les numéros Peano et constructeurs intelligents .

head de type sûr et tail semblent vraiment cool pour moi.

Et je pense que je suis arrivé à la limite de ce que je sais comment faire

{-# 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

. (Désolé pour les erreurs de transcription - la machine j'ai écrit ceci sur w / mon compilateur Haskell est actuellement en bas)

La plupart de ce que je l'ai fait avec compile / o un problème, mais je rencontre des problèmes avec ofList et filter. Je pense que je comprends pourquoi - quand je dis ofList :: [a] -> CountedList n a, je dis ofList :: forall n . [a] -> CountedList n a - que la liste créée peut être de tout type de comptage souhaité. Ce que je veux écrire est l'équivalent du type pseudo ofList :: exists n . [a] -> CountedList n a, mais je ne sais pas comment.

Y at-il une solution qui me permettrait d'écrire ofList et fonctions filter comme j'imagine, ou ai-je atteint la limite de ce que je peux faire avec ça? Je sens qu'il ya un truc avec des types existentiels que je suis absent.

Answer 1

Vous ne pouvez pas écrire

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

mais vous pouvez écrire

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

et transmettre une fonction qui représente ce que vous auriez fait avec le résultat de ofList, tant que son type est indépendant de la longueur de la liste.

Par ailleurs, vous pouvez vous assurer l'invariant que le type d'une liste correspond à sa longueur dans le système de type, et ne pas compter sur les constructeurs intelligents:

{-# LANGUAGE GADTs #-}

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

Answer 2

Vous ne pouvez pas définir ofList ou filter cette façon parce qu'ils sont des contrôles au niveau du type de confusion avec des valeurs d'exécution. En particulier, dans le type du résultat, CountedList n a, le n de type doit être déterminée au moment de la compilation. Le désir implicite est que n doit être proportionnelle à la longueur de la liste qui est le premier argument. Mais cela ne peut pas être clairement connus jusqu'à ce qu'ils soient d'exécution.

Maintenant, il pourrait être possible de définir une classe de types, disons Compté, puis (avec l'extension Haskell appropriée), définir ceux-ci comme:

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

Mais vous auriez du mal à faire quoi que ce soit avec un tel résultat, étant donné que les seules opérations CountedListable pourrait soutenir serait extraire le compte. On ne pouvait pas, dire obtenir le head d'une telle valeur, car la tête ne peut pas être défini pour toutes les instances de CountedListable