[TYPES] Equi recursive types: logical relations and intuition

[Gabriel Scherer]

In the theories you have in mind, how do the fixpoint operators on terms
and types deal with degenerate fixpoints like (fix x . x) and (mu alpha.
alpha)? If your iso-recursive type theory allows the term (fix x. fold x)
but your equi-recursive type theory forbids (fix x . x) or its type, you
have a difference between the two systems. If they are allowed in both
cases, do they reduce in the same way?

On Thu, Nov 15, 2018 at 12:13 PM Marco Patrignani <mp at cs.stanford.edu>
wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list
> ]
>
> 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
>
>
>
>
>