Another typing question

[Wolfgang Jeltsch]

On Tuesday, 2003-08-05, 12:23, CEST, Konrad Hinsen wrote:
> Is there any way to parametrize a type by a value, rather than another
> type? 

No, there isn't.

> What I would like to do is to define "list of length 3" and "list of length
> 4" as separate parametrization of the same type, such that I could write
> functions that accept lists (under my new typename) of any length as long as
> parameters have the same length. The goal is to remove the need for runtime
> checks all over the code.

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 use 
tuples like (a,a) (list of length 2) (a,a,a) (list of length 3) etc.

A better solution might be:
    data EmptyList element = EmptyList
    data TrueList list element = 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.

You could define different types for different natural numbers:
    data Zero = Zero
    data Succ number = 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 => Sum (Succ a) b (Succ c)

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 type
    List (Succ (Succ (Succ (Succ Zero)))) Int

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

It would be interesting to know if/how you could, e.g., define a concatenation 
function with a type like
    (Sum length1 length2 length,
     HasLength list1 length1,
     HasLength list2 length2,
     HasLength list length) =>
    list1 -> list2 -> list.

> Konrad.

Wolfgang