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