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
