Beyond Haskell 98, this requires only empty data-types (and even that could be worked around). First we create fixed enum types:

data Empty data OneMore n = Succ n | Zero impossible :: Empty -> a impossible _ = undefined

It's unfortunate that we can't define impossible without using bottom. I dislike using bottom, and here we have a function that cannot return bottom unless it is passed bottom. Such functions should be definable without using bottom, but this one isn't.

type Enum0 = Empty type Enum1 = OneMore Enum0 type Enum2 = OneMore Enum1 type Enum3 = OneMore Enum2

Now a BoundedEnum class. We can't just use Enum and Bounded, because Bounded instances have to have at least one value (nasty missed corner-case, that).

class BoundedEnum n where enum :: [n] enumFind :: [a] -> Maybe (n -> a) instance BoundedEnum Empty where enum = [] enumFind [] = Just impossible enumFind _ = Nothing instance (BoundedEnum n) => BoundedEnum (OneMore n) where enum = Zero:(fmap Succ enum) enumFind [] = Nothing enumFind (a:as) = fmap (\f n -> case n of Succ ns -> f ns Zero -> a ) (enumFind as)

Then we create our lists as functions from those types to the element type:

type Vec = (->)

vnil :: Vec Empty a vnil = impossible

vcons :: a -> Vec n a -> Vec (OneMore n) a vcons a v Zero = a vcons a v (Succ n) = v n

vhead :: Vec (OneMore n) a -> a vhead v = v Zero

vtail :: Vec (OneMore n) a -> Vec n a vtail v n = v (Succ n)

vzipwith (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c vzipwith f va vb n = f (va n) (vb n)

vtolist :: (BoundedEnum n) => Vec n a -> [a] vtolist = fmap v enum

vfoldr :: (BoundedEnum n) => (a -> b -> b) -> b -> Vec n a -> b vfoldr f b v = foldr f b (vtolist v)

vec :: a -> Vec n a vec = const

vfromList :: [a] -> Maybe (Vec n a) vfromList = enumFind

etc. -- Ashley Yakeley, Seattle WA