[TYPES] Identity extension for the system F term model

Thu Aug 28 23:15:41 EDT 2025

I retract my statement.
While every parametric model is its own extensional collapse by the minimal
PER family consisting of identities on each type, the *uniform*
("functorial") construction uses the full set of PERs, which can certainly
introduce new identifications.
I do not know whether the extensional collapse of the initial model is
initial among all parametric models.

On a related note, in the "Extensional models for polymorphism" paper,
Breazu-Tannen and Coquand ask whether the extensional quotient of the
closed term model of system F yields the same theory as the "maximal
consistent polymorphic theory" defined by Moggi. [1]

Does anyone know if this is still open?

Thanks,
Andrew

[1]  https://urldefense.com/v3/__https://person.dibris.unige.it/moggi-eugenio/ftp/maxcons__;!!IBzWLUs!Sr-NZLDADgRd7d-DHh-mWfvCKdS-_9xr1Rp9MKFkz6z_mrW9-TpI0Oqyfh4v80QAQZbii-LSPdIaMJ3BNdlJcCVNSG2K0CpPzYwTrQ$ 

On Thu, Aug 28, 2025 at 5:55 PM Andrew Polonsky <andrew.polonsky at gmail.com>
wrote:

> Hasegawa gives such a definition in "Parametricity of extensionally
> collapsed term models of polymorphism and their categorical properties",
> see Def. 3.4 and 3.8(iii).
>
> The fact that the extensional collapse of the overall-initial model is the
> initial parametric model follows from functoriality of the extensional
> quotient construction. I don't know if anyone has verified this explicitly,
> but it seems quite clear from how the construction is described by
> Breazu-Tannen and Coquand in "Extensional models for polymorphism", section
> 4 .
>
> Best,
> Andrew
>
> On Thu, Aug 28, 2025 at 1:21 PM Michael Shulman <shulman at sandiego.edu>
> wrote:
>
>> What is the definition of a "parametric model"?  And can you give a
>> reference for the statement that the "extensional" quotient of the
>> overall-initial model is the initial parametric model?
>>
>> On Wed, Aug 27, 2025 at 9:20 PM Andrew Polonsky <
>> andrew.polonsky at gmail.com> wrote:
>>
>>> [ The Types Forum,
>>> http://lists.seas.upenn.edu/mailman/listinfo/types-list  ]
>>>
>>> Put
>>> Top = \forall X. X -> X
>>> tt = /\X.\x:X.x : Top
>>> T(X) = (X -> Top) -> (Top -> Top)
>>> A1 = A2 = Top
>>> R \subset A1xA2 is =beta(eta)
>>> T(R) identifies \x.x, \xy.y, and \xy.tt.
>>>
>>> While I agree that the term "initial model" is most often applied to a
>>> term
>>> model with a syntactic notion of equality, in discussions of IEL there's
>>> a
>>> general implicature that you are interested in parametric models. And the
>>> initial such model is precisely the extensional quotient of the term
>>> model,
>>> for which IEL holds tautologically.  (More precisely, it holds by the
>>> fundamental theorem of logical relations, the version for open terms that
>>> is verified in the proof of the theorem.)
>>>
>>> Best,
>>> Andrew
>>>
>>>
>>> On Wed, Aug 27, 2025 at 7:59 PM Ryan Wisnesky <wisnesky at gmail.com>
>>> wrote:
>>>
>>> > Thanks everyone for the informative discussion!   Andrew’s
>>> counter-example
>>> > of T(X) = X->X to the IEL in the initial model is just what was asked
>>> for.
>>> >
>>> > If I may ask a follow-up: does anyone have a counter-example for the
>>> IEL
>>> > in the initial model for a type expression that defines a functor?  Or
>>> a
>>> > proof that IEL always holds for definable functors in the initial
>>> model?
>>> > (T(X) = X->X is well-known not to be a functor.).
>>> >
>>> > Thanks again!
>>> > Ryan
>>> >
>>> > > On Aug 14, 2025, at 10:59 PM, Andrew Polonsky <
>>> andrew.polonsky at gmail.com>
>>> > wrote:
>>> > >
>>> > > [ The Types Forum,
>>> > http://lists.seas.upenn.edu/mailman/listinfo/types-list   ]
>>> > >
>>> > > Yes, the initial model of System F satisfies the identity extension
>>> > lemma,
>>> > > assuming that by "initial model" you mean the extensional quotient of
>>> > > closed terms as treated e.g. by Hasegawa [1].
>>> > >
>>> > > The identity relation in this model is the extensional equality
>>> defined
>>> > by
>>> > > induction on type structure with the usual logical relation
>>> conditions.
>>> > > This identifies terms that are not beta(-eta) convertible, like the
>>> two
>>> > > successors on the polymorphic church numerals.
>>> > >
>>> > > Nat = \forall A. (A -> A) -> (A -> A)
>>> > > S, S' : Nat -> Nat
>>> > > S = \nfs.f(nfs)
>>> > > S' = \nfs.nf(fs)
>>> > >
>>> > > If by "initial model" you mean something intensional like a lambda
>>> > algebra
>>> > > with beta conversion, then IEL fails.  We can use the same type as
>>> the
>>> > > counterexample.
>>> > >
>>> > > T(X) = X -> X
>>> > > A1 = A2 = Nat
>>> > > R \subset A1xA2 is =beta
>>> > > T(R) identifies S and S'
>>> > >
>>> > > Best,
>>> > > Andrew
>>> > >
>>> > > P.S. Regarding the other question raised in the Zulip chat you
>>> linked,
>>> > > whether every type A is isomorphic to "forall X. (A -> X) -> X" in
>>> this
>>> > > extensional model, I believe the answer to be "yes" based on
>>> comments by
>>> > > Thierry Coquand in [2], slide 52.
>>> > >
>>> > > [1]
>>> >
>>> https://urldefense.com/v3/__https://doi.org/10.1007/3-540-54415-1_61__;!!IBzWLUs!S8aJh356wvmDdcHzuNn_x-n_pAINEuB9OorQS4vpVVPxzpk6f1Frz6bXU2iKOmWU2eJnfiof4UvCQ7Pz7EY2e8iQYns02p8_gTB7LQ$
>>> > > [2]
>>> >
>>> https://urldefense.com/v3/__https://youtu.be/6Ao9zXwyteY?si=5FdC5t5Mnyajmchz&t=4660__;!!IBzWLUs!S8aJh356wvmDdcHzuNn_x-n_pAINEuB9OorQS4vpVVPxzpk6f1Frz6bXU2iKOmWU2eJnfiof4UvCQ7Pz7EY2e8iQYns02p8az4OKSg$
>>> > >
>>> > >
>>> > > On Tue, Aug 12, 2025 at 12:02 PM <
>>> > types-list-request at lists.seas.upenn.edu>
>>> > > wrote:
>>> > >
>>> > >> Send Types-list mailing list submissions to
>>> > >>        types-list at LISTS.SEAS.UPENN.EDU
>>> > >>
>>> > >> To subscribe or unsubscribe via the World Wide Web, visit
>>> > >>        https://LISTS.SEAS.UPENN.EDU/mailman/listinfo/types-list 
>>> > >> or, via email, send a message with subject or body 'help' to
>>> > >>        types-list-request at LISTS.SEAS.UPENN.EDU
>>> > >>
>>> > >> You can reach the person managing the list at
>>> > >>        types-list-owner at LISTS.SEAS.UPENN.EDU
>>> > >>
>>> > >> When replying, please edit your Subject line so it is more specific
>>> > >> than "Re: Contents of Types-list digest..."
>>> > >>
>>> > >>
>>> > >> Today's Topics:
>>> > >>
>>> > >>   1.  Identity extension for the system F term model (Ryan Wisnesky)
>>> > >>
>>> > >>
>>> > >>
>>> ----------------------------------------------------------------------
>>> > >>
>>> > >> Message: 1
>>> > >> Date: Mon, 11 Aug 2025 21:25:19 -0700
>>> > >> From: Ryan Wisnesky <wisnesky at gmail.com>
>>> > >> To: "types-list at lists.seas.upenn.edu"
>>> > >>        <types-list at LISTS.SEAS.UPENN.EDU>
>>> > >> Subject: [TYPES] Identity extension for the system F term model
>>> > >> Message-ID: <CC3F8356-0B05-4A68-9E87-DD181A587DB4 at gmail.com>
>>> > >> Content-Type: text/plain;       charset=utf-8
>>> > >>
>>> > >> Hi All,
>>> > >>
>>> > >> I'm hoping the folks on this list can settle a question of folklore;
>>> > >> myself and Mike Shulman and others have been discussing it on the
>>> > applied
>>> > >> category theory zulip channel but have yet to reach a conclusion:
>>> > >>
>>> >
>>> https://urldefense.com/v3/__https://categorytheory.zulipchat.com/*narrow/channel/229199-learning.3A-questions/topic/Continuations.2C.20parametricity.2C.20and.20polymorphism/with/528479188__;Iw!!IBzWLUs!Uf89Hb7uWjtbz4qUeFbMCVwfxkuye2lpB27Oi4vChhMV6yMPpA57jl2oZnBt3TaOOYa7UhjQTz16dPMUZoGtGubQesXT$
>>> > >>
>>> > >> The question is whether the initial (term) model of system F (2nd
>>> order
>>> > >> impredicative polymorphic lambda calculus) satisfies the "identity
>>> > >> extension lemma", which is one of the primary lemmas characterizing
>>> > >> (Reynolds) parametric models.  To be clear, this question is about
>>> the
>>> > >> initial (term) model of system of F, its initial model of contexts
>>> and
>>> > >> substitutions.
>>> > >>
>>> > >> There are many places that state the system F term model should obey
>>> > >> identity extension, for example, this remark by Andy Kovacs:
>>> > >>
>>> >
>>> https://urldefense.com/v3/__https://cs.stackexchange.com/questions/136359/rigorous-proof-that-parametric-polymorphism-implies-naturality-using-parametrici/136373*136373__;Iw!!IBzWLUs!Uf89Hb7uWjtbz4qUeFbMCVwfxkuye2lpB27Oi4vChhMV6yMPpA57jl2oZnBt3TaOOYa7UhjQTz16dPMUZoGtGpQSw3Ii$
>>> > >> .
>>> > >>
>>> > >> However, neither myself nor Mike nor anyone on the zulip chat or
>>> anyone
>>> > >> we?ve asked has been able to find a proof (or disproof).
>>> > >>
>>> > >> Anyway, do please let me know if you know of a clear proof or
>>> disproof
>>> > of
>>> > >> the identity extension lemma for the initial (term) model of system
>>> F!
>>> > >>
>>> > >> Thanks,
>>> > >> Ryan Wisnesky
>>> > >>
>>> > >> PS Here's a statement from Mike about the exact definition of this
>>> > >> question:
>>> > >>
>>> > >> Let C be the initial model of system F.  Let R(C) be the relational
>>> > model
>>> > >> built from C, so its objects are objects of C equipped with a binary
>>> > >> relation.  There is a strict projection functor R(C) -> C, and
>>> since C
>>> > is
>>> > >> initial this projection has a section C -> R(C), which is "external
>>> > >> parametricity".  In a theory like System F that has type variables,
>>> a
>>> > >> "model" includes information about types in a context of type
>>> > variables, so
>>> > >> external parametricity sends every type in context to a "relation in
>>> > >> context".  Do the relations-in-context resulting in this way from
>>> types
>>> > of
>>> > >> System F always map identity relations to identity relations?
>>> > >>
>>> > >> ------------------------------
>>> > >>
>>> > >> Subject: Digest Footer
>>> > >>
>>> > >> _______________________________________________
>>> > >> Types-list mailing list
>>> > >> Types-list at LISTS.SEAS.UPENN.EDU
>>> > >> https://LISTS.SEAS.UPENN.EDU/mailman/listinfo/types-list 
>>> > >>
>>> > >>
>>> > >> ------------------------------
>>> > >>
>>> > >> End of Types-list Digest, Vol 155, Issue 3
>>> > >> ******************************************
>>> > >>
>>> >
>>> >
>>>
>>