Fixed-length vectors in Haskell
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"
Hi all Oleg, it seems to me that you're blurring two distinctions here. (i) fixed-length versus unknown length (ii) cons-list versus array There's no good reason why either the dependent-style vector
David Menendez wrote: ] data Vec n a where ] Nil :: Vec Zero a ] Cons :: a -> Vec n a -> Vec (Succ n) a
or the class-of-constructors representation (strangely familiar to me)
] data Vec_0 a = Nil ] data Vec_s v a = Cons a (v a)
S.M.Kahrs wrote: ] data Cons b a = a :. b a ] data NIL a = NIL
should eat any more memory or be harder to access than regular cons-lists. The length information is entirely static. This representation precisely does not suffer from the problem you quote with respect to nested types. Nested types such as the AVL trees in
http://www.haskell.org/pipermail/haskell/2003-April/011693.html
and the square matrix types suffer from the fact that their constructors must target all parameters uniformly, even if the recursive references are more specialised. You can only make the parameter bigger by going under a constructor, so if you want to make structures with size invariants, you get this prefix to build up the size which eats space and time. Here's a unary version of square matrices: data Nil a = Nil data Cons b a = a :. b a newtype Square a = Count Nil a data Count f a = Stop (f (f a)) | Step (Count (Cons f) a) As you can see, it's the Stop and Step which take up the extra space, recording the size of the matrix, and also concealing it from the type. This structure represents square matrices of any size, ie exists n. Vec (Vec n a) with the Steps and Stop representing the n, and then the vector of vectors stored as sized cons-lists. If you want to write a multiplier for matrices, you need to expose these sizes, and that's where type classes help a bit and indexed datatype families help a lot. For the same reason, it's easy to define the well-scoped lambda terms (Bird & Paterson 1999), because scope only gets bigger, data Tm x = Var x | App (Tm x) (Tm x) | Lam (Tm (Maybe x)) but trickier to define the simply-typed lambda terms, where it helps to be able to say 'lambda makes (s -> t)' as you can with datatype families (Altenkirch & Reus, 1999) and now with GADTs. It's great to see this stuff making it into Haskell. There are plenty more examples in the literature that should shift over with minimal fuss. Anyhow, when you say
to take the 1023d element of a 1024-element vector, we have to traverse 1023 Cons cells.
that's clearly to do with the cons-list representation, not the fixed length. Of course, I agree with you that the array representation of sequences is sometimes more appropriate than the cons-list representation, but the reverse is also true. It's good to have fixed-length versions of both.
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)
Vectors store their lengths implicitly, the way lists do; don't arrays store their bounds explicitly? But you're right, there's no reason to believe that the bound corresponds to the n...
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.
Indeed we do, so we shall certainly have to work with sizes in a principled way inside the abstraction barrier, eg tabulation of Ashley's functions from finite sets (another traditional dependent vector representation), or whatever. Especially if we want to justify (at least to ourselves) the use of non-bound-checked accesses, which is surely part of the point here. My point is just that the issue between inductive Vec and array PVector is just the cons-list versus array issue. It's not about how one works with sizes. In either approach, one inevitably comes up against the fact that sizes are numbers, ie a kind of data, and one would like them to behave accordingly. How hard the language makes it to treat these numbers like data is the measure of how well equipped it is to support this precise style of programming. The existence of crafty encodings cannot, in the long run, rescue an inappropriate design. All the best Conor -- http://www.cs.nott.ac.uk/~ctm
participants (2)
-
Conor McBride -
oleg＠pobox.com