Haskell подсчитал тип списка

Question

Итак, просто для удовольствия, я играл с типом CountedList в Haskell, используя цифры Peano и smart constructors.

Тип-сейф head и tail просто кажутся действительно крутыми для меня.

И я думаю, что я достиг предела того, что я знаю, как сделать

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

(извините за ошибки транскрипции - машина изначально я написал это на ж/мой Haskell компилятор в настоящее время вниз) ,

Большая часть того, что я сделал, компилирует без проблемы, но у меня возникают проблемы с ofList и filter. Думаю, я понимаю, почему - когда я говорю ofList :: [a] -> CountedList n a, я говорю ofList :: forall n . [a] -> CountedList n a - что созданный список может иметь любой желаемый тип счета. То, что я хочу написать, является эквивалентом псевдо-типа ofList :: exists n . [a] -> CountedList n a, но я не знаю, как это сделать.

Есть ли обходной путь, который позволил бы мне написать ofList и filter функции, как я себе представляю, или я достиг предела, что я могу сделать с этим? У меня есть чувство, что есть какая-то трюка с existential types, которую я пропускаю.

Answer 1

Вы не можете написать

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

, но вы можете написать

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

и передать ему функцию, которая представляет то, что вы бы сделали с результатом ofList, если его тип не зависит от длины списка.

Кстати, вы можете гарантировать инвариант, что тип списка соответствует его длине в системе типов, а не полагаться на смарт-конструкторами:

{-# LANGUAGE GADTs #-} 

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

Answer 2

Вы не можете определить ofList или filter таким образом, потому что они смешивают проверки уровня на уровне с значениями времени выполнения. В частности, в типе результата CountedList n a тип n должен быть определен во время компиляции. Предполагаемое желание состоит в том, что n должен быть соизмеримым с длиной списка, который является первым аргументом. Но это ясно неизвестно до времени выполнения.

Теперь, можно было бы определить класс типов, скажем, счетные, а затем (с соответствующим расширением Haskell), определяет этот как:

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

Но вы бы иметь трудное время делать что-либо с такой результат, так как единственные операции, которые может поддерживать CountedListable, будут извлекать счетчик. Вы не могли бы, скажем, получить head такого значения, потому что голова не может быть определена для всех экземпляров CountedListable