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
Recursive types
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2005-11-16 (08:52)
From: Jacques Garrigue <garrigue@m...>
Subject: Re: [Caml-list] Recursive types
From: Keiko Nakata <keiko@kurims.kyoto-u.ac.jp>

> I think that it is not easy to know when to apply eta-expansion, 
> namely, to replace a type name with its underlying definition.
> For instance, to check equivalence betweeen the types t and s below:
>  type t = < m : t * t >
>  type 'a tuple = 'a * 'a
>  type s = < m : s tuple >
> the algorithm should memorize that t * t and s tuple are equivalent,
> and then expands s tupl into s * s  
> so as to check between t * t and s * s? 

No need to memorize equivalences: s tuple expands at its head to s * s.
The type checker guarantees that it is always safe to expand the head
of a type (i.e., definitions are well-founded.)
But you're right that abbreviations complicate the unification
algorithm a lot.
In order for unification to succeed above, t must expand to
(< m: 'a * 'a> as 'a), and s too. But to print nicely types we must
keep the abbreviations. This is done by memoizing expansions inside 
the abbreviations themselves. I.e., the expansion of t is actually:
  (< m : t[t='a] * t[t='a] > as 'a)
and that of s is
  (< m : s[s='b] tuple[s='b]> as 'b)
where [t='a] is an internal annotation to the abbreviation. So when
unifying, you can actually check the underlying type of an
abbreviation. But maintaining these abbreviations is rather
Fo instance abbreviations must be propagated:
  type u = <m : w> and w = u * u
will expand to
  (<m : w[u='a]> as 'a)
so that, if we expand w, we fall back to
  (<m : u[u='a] * u[u='a]>)

Jacques Garrigue