[TYPES] Identity extension for the system F term model

Thu Aug 28 13:49:48 EDT 2025

Also, for anyone who is interested, I believe a very similar functor
violating IEL appears in Hyland, Robinson, and Rosolini "Algebraic Types in
PER Models", as part of an example of a type that is not isomorphic to its
"type of continuations" in the initial model, and hence of a polymorphic
transformation between definable functors that is not natural.  (This
observation was part of what started the whole Zulip conversation trying to
square this with claims that parametricity implies naturality.)  With your

Top = \forall X. X -> X
tt = /\X.\x:X.x : Top

the functor is

T(X) = (Top -> Top) -> X

which I think we can see fails IEL with

A1 = A2 = Top -> Top
R = beta-eta equality

and then T(R) will also identify \x.x and \xy.y and \xy.tt, and also I
think other things like \xy.x(y).

HRR's observation (which they call "well-known", although we have not found
any other references for it) is that the transformation \forall X. T(X) ->
X defined by

/\X. \f.  f(\y. y[X -> Top](\z. tt)(f(\w.w)))

is not natural, because it is not definitionally equal to evaluation at any
element of (Top -> Top), which it would have to be if it were natural by
the Yoneda lemma.

On Thu, Aug 28, 2025 at 10:20 AM 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
>> > >> ******************************************
>> > >>
>> >
>> >
>>
>