Тип подсчитанного списка Haskell

Question

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

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

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 должно быть соизмеримо с длиной списка, который является первым аргументом.Но это явно не может быть известно до начала выполнения.

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

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

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