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

[Wolfgang Jeltsch]

Hello Ryan,

I hope, it’s okay to forward your message to the list:

> Date: Freitag, 1. Februar 2008 01:41
> From: "Ryan Ingram" <ryani.spam at gmail.com>
> To: "Wolfgang Jeltsch" <g9ks157k at acme.softbase.org>

This representation is not exactly the same when you include _|_.

For example:
> data None -- only _|_ / undefined are members of this type.
> data Pair a b = Pair a b
>
> -- There are three distinct inhabitants of the type Pair None (Pair None
> None): v1, v2, v3 :: Pair None (Pair None None)
> v1 = undefined
> v2 = Pair undefined undefined
> v3 = Pair undefined (Pair undefined undefined)
>
> -- whereas there are only two inhabitants of (None, None, None):
> p1, p2 :: (None, None, None)
> p1 = undefined
> p2 = (undefined, undefined, undefined)

You could solve it this way:
> data PairL a b = PairL a !b

where (a,b,c) is syntactic sugar for
PairL a (PairL b (PairL c ()))

Now we are back to only having two inhabitants of the type:
> x1, x2 :: PairL None (PairL None (PairL None ()))
> x1 = undefined
> x2 = PairL undefined (PairL undefined (PairL undefined ()))

There are still potential efficiency issues, although this could be
worked out in the compiler; right now it's a single operation to get
from a tuple to any member, but in PairL it takes n operations to get
from the root to the nth elment of the tuple.  The
"unbox-strict-fields" optimization can fix this.

On 1/31/08, Wolfgang Jeltsch <g9ks157k at acme.softbase.org> wrote:
> 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` ())…))