Haskell counted list type

Question

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 n a, I'm saying ofList :: forall n . [a] -> CountedList n a - 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 n a, 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.

Answer 1

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

Answer 2

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 n a, 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