Version française
Home     About     Download     Resources     Contact us    
Browse thread
Polymorphic recursion
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ 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