# Another typing question

**Wolfgang Jeltsch
**
wolfgang@jeltsch.net

*Tue, 5 Aug 2003 15:23:09 +0200*

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