Re: [Caml-list] Recursive types

[Keiko Nakata <keiko@kurims.kyoto-u.ac.jp>]

From: Alain Frisch <Alain.Frisch@inria.fr>
> 
> The restriction ensures that structural recursive types are necessarily
> regular. So standard coinductive algorithms (implemented by keeping
> track of visited nodes or by memoization) are ok.

Thanks for the reply.

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? 

When type abbreviations are more verobse as in 

 type 'a id = 'a 
 type 'a tuple = 'a id * 'a id 
 type u = < m : < m : u tuple> * < m : u tuple> > 

it seems difficult to know when to memorize in what representations
and when to eta-expand by the definitions.

I know easy standard coinductive algorithms found in textbooks,
but how to handle abbreviations is still unclear for me.

With best regards,
Keiko.