[TYPES] Equi recursive types: logical relations and intuition

[Marco Patrignani]

Dear types mailing list,
I have some questions related to equi recursive types.

** Background **

Together with my colleague Dominique Devriese (in cc) we were building a compiler from
      STLC extended with a fix operator (and without recursive types)
down to
      STLC with isorecursive types
in order to prove it fully abstract using a step-indexed logical relation.
This proof goes through but we noticed that it goes through exactly because of the extra step that a term of the form
      unfold fold v
consumes while reducing to
      v
Now if we were to replace iso recursive types in the target with equi recursive ones, that extra step would not be there and therefore the proof would fail.
( if you’re familiar with these kinds of logical relations, there’s a \later that ‘matches’ this reduction step and reduces the amount of steps by 1 )

However, this seems a limitation that stems purely out of the proof technique.
If we had something else to “decrease" rather than an operational step, the proof would go through.


** Q1 : logical relation for equi-recursive types **
Looking at logical relations for languages with recursive types, they all seem to have iso-recursive ones.
Is there a sound logical relation for a calculus with equi-recursive types?


** Q2 : full abstraction of iso and equi calculi **
To the best of our knowledge there is no known fully abstract compilation result from a calculus with iso recursive types to one with equi recursive ones.
Are we right?
( such a compiler would, intuitively, just erase fold/unfolds )


** Q3 : intuition behind equi-recursive types **
I have generally considered the difference between iso and equi recursive types to be one primarily of typechecking, the fold/unfold annotations being there to direct typechecking, and in fact fold/unfold are often somewhat implicit in the syntax of languages (as i recall from TAPL’s chapter on recursive types).

However, for logical relations it seems that the operational aspect (the extra reduction step) introduced by iso recursive types is a key distinguishing feature between iso and equi recursive types.
Are there other topics besides the logical relations (apart from typechecking) where the difference in the operational semantics between iso and equi typed terms play a role?


thanks!

marco
---
Marco Patrignani
http://theory.stanford.edu/~mp <http://theory.stanford.edu/~mp>
Stanford Computer Science Department, USA
& CISPA, Saarland University, Germany