Browse thread
Polymorphic recursion
[
Home
]
[ Index:
by date
|
by threads
]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
| Date: | -- (:) |
| From: | Loup Vaillant <loup.vaillant@g...> |
| Subject: | Polymorphic recursion |
I was reading Okasaki's book, "Purely functionnal data structures",
and discovered that ML (and Ocaml) doesn't support non uniforms
function definitions.
So, even if:
(**)
type 'a seq = Unit | Seq of ('a * ('a * 'a)seq);;
(**)
is correct,
(**)
let rec size = fun
| Unit -> 0
| Seq(_, b) -> 1 + 2 * size b;;
(**)
is not. Here is the error:
#
| Seq(_, b) -> 1 + 2 * size b;;
This expression (the last 'b') has type seq ('a * 'a) but is here used
with type seq 'a
#
Why?
Can't we design a type system which allow this "size" function?
Can't we implement non uniform recursive function (efficiently, or at all)?.
I suppose the problem is somewhat difficult, but I can't see where.
Regards,
Loup Vaillant