Another typing question

[Konrad Hinsen]

On Tuesday 05 August 2003 15:23, Wolfgang Jeltsch wrote:

> There probably are ways to achieve this with Haskell's type system. The
> exact solution depends on what exactly you want.
>
> For just distinguishing between lists of different lengths you could us=
e
> tuples like (a,a) (list of length 2) (a,a,a) (list of length 3) etc.

What would be the advantage to using standard lists? In both cases I'd ne=
ed=20
explicit length checks everywhere.

> A better solution might be:
>     data EmptyList element =3D EmptyList
>     data TrueList list element =3D TrueList element (list element)
> A list of four Ints for example would be represented by a value of type
>     TrueList (TrueList (TrueList (TrueList EmptyList))) Int.

Isn't that just the Haskell list type by another name?

> You could define different types for different natural numbers:
>     data Zero =3D Zero
>     data Succ number =3D Succ number
> and do simple arithmetic with them at the type level:
>     class Sum a b c | (a, b) -> c
>     instance Sum 0 a a
>     instance Sum a b c =3D> Sum (Succ a) b (Succ c)

That looks interesting, I need to look into multiple parameter classes...

> At the moment, I cannot think of a way of defining a list type which is
> parameterized by such natural types. What I mean is having a type
>     List :: * -> * -> *
> where for our above example of a list of four Ints we would have the ty=
pe
>     List (Succ (Succ (Succ (Succ Zero)))) Int

That's what I would like...

> What I can think of, is an association between our above list types
> (EmptyList and TrueList) and our natural number types by a multi-parame=
ter
> class: class HasLength list length | list -> length
>     instance HasLength EmptyList Zero
>     instance HasLength list length =3D> HasLength (TrueList list) (Succ
> length)

Again those multi-parameter classes... and off I go to the Haskell Web si=
te=20
;-)

Thanks for your comments!

Konrad.