[TYPES] System F omega with (equi-)recursive types

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Dear types forum members,

I have been looking for publications studying the properties (type
safety, decidability of type checking, type checking algorithm) of
System F omega combined with (equi-)recursive types but have,
unfortunately, been quite unsuccessful. I am interested in an extension
of F omega where the X in (mu X. T) ranges over proper types of kind *.

I would very much appreciate any pointers into the literature.

Thank you and best regards,

Florian

--

-- 
Florian Lorenzen

Technische Universität Berlin
Fakultät IV - Elektrotechnik und Informatik
Übersetzerbau und Programmiersprachen

Sekr. TEL12-2, Ernst-Reuter-Platz 7, D-10587 Berlin

Tel.:   +49 (30) 314-24618
E-Mail: florian.lorenzen@...
WWW:    http://www.user.tu-berlin.de/florenz

Re: [TYPES] System F omega with (equi-)recursive types

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Hello,

On Mon, Jun 06, 2011 at 06:33:00PM +0200, Florian Lorenzen wrote:
> I have been looking for publications studying the properties (type
> safety, decidability of type checking, type checking algorithm) of
> System F omega combined with (equi-)recursive types but have,
> unfortunately, been quite unsuccessful. I am interested in an extension
> of F omega where the X in (mu X. T) ranges over proper types of kind *.

First, do you know about the papers that concern System F with equi-recursive
types? There is a paper by Neal Glew and one by Nadji Gauthier and I on
efficiently deciding type equality in the presence of \forall and \mu
quantifiers. You can find references to earlier work in there (e.g. work by
Colazzo and Ghelli). Once you know how to check type equality, the rest
(proof of type soundness, type-checking algorithm) is just as in System F;
the presence of recursive types has essentially no impact.

You say that you are interested in System F_omega, but you restrict the \mu
quantifier to variables of kind *. It seems to me that the resulting system
remains fairly simple, because beta-reduction and the unfolding of \mu's
cannot interact: unfolding a \mu cannot cause a beta-redex to appear. Thus,
you should be able to first bring every type to a normal form, as in Ssytem
F_omega, then compare types for equality, as in System F with recursive types.

If you allow \mu at every kind, things become more interesting. There is an
old paper by Marvin Solomon at POPL 1978 where it is showed that in the
presence of parameterized, recursive types definitions (that is, in System
F_omega with \mu at every kind), deciding whether two types are equal is

Re: [TYPES] System F omega with (equi-)recursive types

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

For termination, you may have a look at:

Strong Normalization and Equi-(co)inductive Types 
<http://www2.tcs.ifi.lmu.de/%7Eabel/tlca07.pdf> Andreas Abel
/Typed Lambda Calculi and Application, TLCA'07.

Best regards, Frederic.
/
Le 07/06/2011 00:07, Florian Lorenzen a écrit :
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
>
>
> Dear types forum members,
>
> I have been looking for publications studying the properties (type
> safety, decidability of type checking, type checking algorithm) of
> System F omega combined with (equi-)recursive types but have,
> unfortunately, been quite unsuccessful. I am interested in an extension
> of F omega where the X in (mu X. T) ranges over proper types of kind *.
>
> I would very much appreciate any pointers into the literature.
>
> Thank you and best regards,
>
> Florian
>