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

[Wolfgang Jeltsch]

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 
a point I had already considered some time ago: Wouldn’t it be good if we had 
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