# [Haskell-cafe] Re: Implementing fixed-sized vectors (using datatype algebra? )

Wolfgang Jeltsch g9ks157k at acme.softbase.org
Thu Jan 31 17:35:21 EST 2008

```Am Donnerstag, 31. Januar 2008 18:30 schrieb Dominic Steinitz:
> Look at
>
> http://sneezy.cs.nott.ac.uk/fun/feb-07/jeremy-slides.pdf

This is essentially what I had in mind.  While Oleg’s implementation needs
a “thrusted core”, the GADT solution doesn’t.

It would be interesting to combine GADTs with decimal type-level naturals.
This could look like this:

> class Succ val succ | val -> succ, succ -> val where
>
>     […]
>
> data List len elem where
>
>     Nil :: List Sz elem
>
>     Cons :: (Succ len len') => elem -> List len elem -> List len' elem

Or with efficient contcatenation:

> class Sum val1 val2 sum
>     | val1 val2 -> sum, val1 sum -> val2, val2 sum -> val1 where
>
>     […]
>
> data List len elem where
>
>     Empty :: List Sz elem
>
>     Singleton :: List (D1 Sz) elem
>
>     Append :: (Add len1 len2 len') =>
>               List len1 elem -> List len2 elem -> List len' elem

Note, that type families might make this code even nicer.

Some words on the representation of decimal numbers as types. While the
representation with types of the form D1 (D2 (D3 Sz)) has the advantage of
allowing numbers of arbitrary size, it has the disadvantage of a growing
number of parantheses.  In my opinion, it would be nicer to have somethink
like D1 :- D2 :- D9 :- () with a right-associative operator :-.  We could
even build the digit list the other way round—() :- D1 :- D2 :- D9—using a
left-associative :-.  With the latter representation, we wouldn’t need to
reverse digit sequences when adding numbers.

Well, the representation (D1,D2,D9) might be considered more readable.  It has
the disadvantage of a fixed maximum size for the numbers.  Which takes me to
just a type

data Pair val1 val2 = Pair val1 val2

and if then (val1,val2,…,valn) would just be syntactic sugar for this:

val1 `Pair` (val2 `Pair` (…(valn `Pair` ())…))

Best wishes,
Wolfgang
```