[Haskell] Fixed-length vectors in Haskell

[oleg at pobox.com]

David Menendez wrote:
] data Vec n a where
]     Nil  ::                 Vec Zero a
]     Cons :: a -> Vec n a -> Vec (Succ n) a

] data Vec_0   a = Nil
] data Vec_s v a = Cons a (v a)

Ashley Yakeley wrote:
] vcons a v Zero = a
] vcons a v (Succ n) = v n

S.M.Kahrs wrote:
] data Cons b a = a :. b a
] data NIL a = NIL

There is a common pattern in all these approaches to fixed-length
vectors: using *data* constructors to encode particular properties of
the data structure. This approach goes back to Chris Okasaki (``From
fast exponentiation to square matrices: An adventure in types.''
ICFP'99), who showed constructing not only of fixed-size vectors but
also matrices that are guaranteed to be square. He also showed
(quoting Ross Paterson, 1998) how to construct an AVL tree so that the
AVL invariant is enforced by construction:

http://www.haskell.org/pipermail/haskell/2003-April/011693.html

This approach has the immense advantage that the invariant cannot be
broken at all. One just can't have a list with fewer Cons cells than
there are elements in the list. Chris Okasaki (in the above message)
has also pointed out a drawback: all these data constructors take
space to be present in memory, and take time to traverse. So, in all
the above representations, to take the 1023d element of a 1024-element
vector, we have to traverse 1023 Cons cells.

The alternative is to encode the invariant -- the vector size, in our
problem -- in *type* constructors, in phantom types. For example,

> newtype PVector n a = PVector (Array Int a)

The run-time representation of PVector n a is the same as Array Int a,
which is quite efficient. There are no traces of the `Nat' can be
found: we use the type-level invariant for type-checking only. So, we
get additional assurances without distorting data structures and
without any run-time penalty whatsoever.

The drawback and the advantage of phantom types is that they are not
``bound'', so to speak, to a term -- they are just ``attached.'' If
the user gets hold of the PVector constructor, the user can easily
compromise our invariants. So, we have to hide PVector in a module and
expose only functions that build the values of PVector one way or the
other. We also have to make sure that these functions are correct --
because they constitute the trusted kernel of our invariant.  The
advantage of that approach is that we can implement very flexible
invariants. Come to think of it, this approach isn't that far from
LCF.


David Menendez wrote:

] We would like a function "vec :: a -> Vec n a", such that "vec x"
] returns a vector of length n with every element equal to x. The basic
] algorithm is simple:
]
]     vec{0}   x = Nil
]     vec{n+1} x = Cons x (vec{n} x)
]
] The usual way to declare a function like this involves a type class,
] which lets us define functions with different behaviors for different
] types:
]
]     class Nat n where vec :: a -> Vec n a
]
]     instance          Nat Zero     where vec x = Nil
]     instance Nat n => Nat (Succ n) where vec x = Cons x (vec x)
]
] This gives vec the type "Nat n => a -> Vec n a", which is good because
] it points out that the type argument to Vec must be a natural, formed
] from Zero or Succ applied to another natural.
]
] However, this solution is unsatisfactory, because it requires the Nat
] class to include every possible function which might depend on a
] type-level argument.

Actually it is not that difficult to create a Nat class with ``every
possible function'' as a member:

> class Nat' n e f where doit :: e a -> f n a

> newtype VecFN n a = VecFN (Vec n a)
> newtype ID a = ID a 
> unVecFN (VecFN x) = x
> unID (ID x) = x

> instance Nat' Zero ID VecFN where doit (ID a) = VecFN Nil
> instance Nat' n ID VecFN => Nat' (Succ n) ID VecFN where
>     doit (ID a) = VecFN (Cons a (unVecFN $ doit (ID a)))

> vec' :: Nat' n ID VecFN => a -> Vec n a
> vec' = unVecFN . doit . ID 

*Vector_GADT> vec' 2 :: (Vec Three Int)
[2,2,2]

If we wish now to implement fromList function, we do

> newtype FromList' n a = FromList'
>     { runFromList' :: Maybe (Vec n a) }
> 
> fromList' :: Nat' n [] FromList' => [a] -> Maybe (Vec n a)
> fromList' = runFromList' . doit
>
> instance Nat' Zero [] FromList' where doit = \l -> FromList' $ Just Nil
> instance Nat' n [] FromList' => Nat' (Succ n) [] FromList' where
>  doit = \l -> case l of
>                    x:xs -> FromList' (fmap (Cons x) (runFromList' $ doit xs))
>                    []   -> FromList' Nothing

*Vector_GADT> fromList' [1,2,3] :: (Maybe (Vec Three Int))
Just [1,2,3]
*Vector_GADT> fromList' [1,2] :: (Maybe (Vec Three Int))
Nothing

This tagging and untagging may be a bit annoying. OTH, FromList', ID,
etc. are all newtypes.


Ashley Yakeley wrote:
] > 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.

Well, we can write:

> impossible = impossible

Or, better,

> impossible = error "I'm afraid I can't do that, Dave"