English version
Accueil     À propos     Téléchargement     Ressources     Contactez-nous    

Ce site est rarement mis à jour. Pour les informations les plus récentes, rendez-vous sur le nouveau site OCaml à l'adresse ocaml.org.

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: 2007-04-03 (16:59)
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