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