[Haskell] Fixed-length vectors in Haskell, Part 3: Using Fixed Enums

[Ashley Yakeley]

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