heterogeneous lists??

Hello:

I found a reference on the internet to a puzzle posed by Bruce Duba.
The challenge is to define Nil and Cons to make the following type
check:

fun length (Nil) = 0
| length (Cons (_, x)) = 1 + length (x);
val heterogeneous = Cons (1, Cons (true, Cons (fn x => x, Nil)));

I banged my head against this problem for a while, and nothing seems
to come up. Can someone please give me a hint here?

Thanks,

Mayer

Mayer <mayer.goldberg@gmail.com> writes:

> I found a reference on the internet to a puzzle posed by Bruce Duba.
> The challenge is to define Nil and Cons to make the following type
> check:
>
> fun length (Nil) = 0
> | length (Cons (_, x)) = 1 + length (x);
> val heterogeneous = Cons (1, Cons (true, Cons (fn x => x, Nil)));
>
> I banged my head against this problem for a while, and nothing seems
> to come up. Can someone please give me a hint here?

Hmm. I assume this is Standard ML, so you have polymorphic recursion
in datatypes, but you don't have it in functions.


So here is my take:

datatype ('a,'b,'c) hlist = Nil | Cons of ('a * ('b,'c,'a) hlist)

which typechecks fine in Moscow ML:

Moscow ML version 2.01 (January 2004)
Enter `quit();' to quit.
> New type names: =hlist
datatype ('a, 'b, 'c) hlist =
(('a, 'b, 'c) hlist,
{con ('a, 'b, 'c) Cons : ('a * ('b, 'c, 'a) hlist) -> ('a, 'b, 'c) hlist,
con ('a, 'b, 'c) Nil : ('a, 'b, 'c) hlist})
con ('a, 'b, 'c) Cons = fn : ('a * ('b, 'c, 'a) hlist) -> ('a, 'b, 'c) hlist
con ('a, 'b, 'c) Nil = Nil : ('a, 'b, 'c) hlist
val 'a length = fn : ('a, 'a, 'a) hlist -> int
> val 'a heterogeneous = Cons(1, Cons(true, Cons(fn, Nil))) :
(int, bool, 'a -> 'a) hlist[closing file "hlist.ml"]
-


Torben