Another typing question

[Alastair Reid]

> > 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.
>
> Isn't that just the Haskell list type by another name?

I think it's quite different.

A Haskell list looks like this:

   1 : 2 : 3 : 4 : []    ::   [Int]

Note that the type gives no indication of the length of the list.

Wolfgang's lists look like this (I'm adding a 'T_' prefix to the names of the 
type constructors to remove some ambiguity)

  1 `TrueList` 2 `TrueList` 3 `TrueList` 4 `TrueList` EmptyList
  ::
  T_TrueList (T_TrueList (T_TrueList (T_TrueList T_EmptyList))) Int

Note that you can determine the length of the list from the _type_ by counting 
the occurences of T_TrueList in the type.

You can see a fully worked use of this approach in Mark Jones' paper about 
typechecking Java bytecodes by translating them into a Haskell program using 
this kind of encoding.  (I'm not sure if Mark would characterise the paper 
this way but it's what I remember him doing...)

http://www.cse.ogi.edu/~mpj/pubs/funJava.html

--
Alastair Reid