Haskell counted list type
So, just for fun, I've been playing with a CountedList type in Haskell, using Peano numbers and smart constructors.
Type-safe head and tail just seem really cool to me.
And I think I've reached the limit of what I know how to do
{-# 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
(sorry for any transcription errors - the machine I originally wrote this on w/ my Haskell compiler is currently down).
Most of what I've done compiles w/o an issue, but I run into issues with ofList and filter . I think I understand why - when I say ofList :: [a] -> CountedList na , I'm saying ofList :: forall n . [a] -> CountedList na ofList :: forall n . [a] -> CountedList na - that the list created can be of any desired count type. What I want to write is the equivalent of the pseudo type ofList :: exists n . [a] -> CountedList na ofList :: exists n . [a] -> CountedList na , but I don't know how.
Is there a workaround that would let me write ofList and filter functions like I'm imagining, or have I reached the limit of what I can do with this? I have a sense that there's some trick with existential types that I'm missing.
You can't write
ofList :: [a] -> (exists n. CountedList n a) -- wrong
but you can write
withCountedList :: [a] -> (forall n. CountedList n a -> b) -> b
and pass it a function which represents what you would have done with the result of ofList , as long as its type is independent of the length of the list.
By the way, you can ensure the invariant that the type of a list corresponds to its length in the type system, and not rely on smart constructors:
{-# LANGUAGE GADTs #-}
data CountedList n a where
Empty :: CountedList Zero a
Cons :: a -> CountedList n a -> CountedList (Succ n) a
You can't define ofList or filter this way because they are confounding type-level checks with run-time values. In particular, in the type of the result, CountedList na , the type n must be determined at compile time. The implied desire is that n should be commensurate with the length of the list that is the first argument. But that clearly can't be known until run-time.
Now, it might be possible to define a typeclass, say Counted, and then (with the appropriate Haskell extension), define these like:
ofList :: [a] -> (forall n. (CountedListable CountedList n) => CountedList n a)
But you'd have a hard time doing anything with such a result, since the only operations that CountedListable could support would be extracting the count. You couldn't, say get the head of such a value because head couldn't be defined for all instances of CountedListable
上一篇: Haskell学什么语言？
下一篇: Haskell计算列表类型