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

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

Типовые 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, как я представляю, или я достиг предела того, что я могу с этим сделать? У меня есть ощущение, что есть трюк с экзистенциальными типами, которые мне не хватает.

Ответ 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

Ответ 2

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

Теперь, возможно, можно определить класс типа, скажем, Counted, а затем (с соответствующим расширением Haskell), определите их как:

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

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