[TYPES] Identity extension for the system F term model

Lars Birkedal birkedal at cs.au.dk
Fri Aug 29 02:40:10 EDT 2025 

Dear All,

One definition of a parametric model is that it is a model of Plotkin and Abadi’s logic for
parametricity. We analyzed that using a bit of categorical logic, to allow you to vary what
you mean by ‘relation’,  (and also showed how Robinson and
Rosolini’s completion process gives rise to a parametric model) in this paper:
   Categorical Models of Abadi and Plotkin’s Logic for Parametricity.
   Mathematical Structures in Computer Science, 15:709-772, 2005.
   Lars Birkedal and Rasmus Møgelberg.
   Available at:    https://urldefense.com/v3/__https://cs.au.dk/*birke/papers/catmap.pdf__;fg!!IBzWLUs!RJ6C8YWYnk0dZux3qnspVBEBtCYUD-w61KxyvhrTo8tCBOUp3ohgzv3F78tLe9jyT-tm0AF-xYV6A9qAYyt3iqdo_Su5kA$ 
The paper also includes a discussion of relationship to other suggested notions of
parametric model, and shows that the expected consequence of parametricity
(definability of algebras and coalgebras, e.g.) can be stated and proved precisely
in this setting.

(Following ideas of Plotkin, we also worked out linear-non-linear versions of
polymorphic type theory, which allow you to use parametricity also to define
solutions to mixed-variance type equations. References below (*)]

Best wishes,
Lars

(*)

Lars Birkedal, Rasmus Ejlers Møgelberg, Rasmus Lerchedahl Petersen:
Linear Abadi and Plotkin Logic. Log. Methods Comput. Sci. 2(5) (2006)

Lars Birkedal, Rasmus Ejlers Møgelberg, and Rasmus Lerchedahl Petersen:
Category-theoretic models of Linear Abadi & Plotkin Logic
Theory and Applications in Categories, 20(7):116–151, 2008.

Lars Birkedal, Rasmus Ejlers Møgelberg, Rasmus Lerchedahl Petersen:
Domain-theoretical models of parametric polymorphism.
Theor. Comput. Sci. 388(1-3): 152-172 (2007)

Rasmus Ejlers Møgelberg, Lars Birkedal, Giuseppe Rosolini:
Synthetic domain theory and models of linear Abadi & Plotkin logic.
Ann. Pure Appl. Log. 155(2): 115-133 (2008)


From: Types-list <types-list-bounces at LISTS.SEAS.UPENN.EDU> on behalf of Michael Shulman <shulman at sandiego.edu>
Date: Thursday, 28 August 2025 at 20.35
To: Andrew Polonsky <andrew.polonsky at gmail.com>
Cc: types-list at lists.seas.upenn.edu <types-list at lists.seas.upenn.edu>
Subject: Re: [TYPES] Identity extension for the system F term model
[ The Types Forum, https://urldefense.com/v3/__https://eur01.safelinks.protection.outlook.com/?url=http*3A*2F*2Flists.seas.upenn.edu*2Fmailman*2Flistinfo*2Ftypes-list&data=05*7C02*7Cbirkedal*40cs.au.dk*7Cb627001864384b43adea08dde661b0c1*7C61fd1d36fecb47cab7d7d0df0370a198*7C1*7C0*7C638920029494972111*7CUnknown*7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ*3D*3D*7C0*7C*7C*7C&sdata=sKbsvnZsk6Lho0hUbDLZbda8rBDYgyGHEfEDbzOZNxw*3D&reserved=0__;JSUlJSUlJSUlJSUlJSUlJSUlJSUlJSU!!IBzWLUs!RJ6C8YWYnk0dZux3qnspVBEBtCYUD-w61KxyvhrTo8tCBOUp3ohgzv3F78tLe9jyT-tm0AF-xYV6A9qAYyt3iqdpL6Z4vA$ <http://lists.seas.upenn.edu/mailman/listinfo/types-list > ]

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, https://urldefense.com/v3/__https://eur01.safelinks.protection.outlook.com/?url=http*3A*2F*2Flists.seas.upenn.edu*2Fmailman*2Flistinfo*2Ftypes-list&data=05*7C02*7Cbirkedal*40cs.au.dk*7Cb627001864384b43adea08dde661b0c1*7C61fd1d36fecb47cab7d7d0df0370a198*7C1*7C0*7C638920029494998061*7CUnknown*7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ*3D*3D*7C0*7C*7C*7C&sdata=ZY4VKaeMjMwS4bG5AMqLYcgHC17a097IPyccH7kqVLs*3D&reserved=0__;JSUlJSUlJSUlJSUlJSUlJSUlJSUlJSU!!IBzWLUs!RJ6C8YWYnk0dZux3qnspVBEBtCYUD-w61KxyvhrTo8tCBOUp3ohgzv3F78tLe9jyT-tm0AF-xYV6A9qAYyt3iqcyo9DabA$ <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,
> > https://urldefense.com/v3/__https://eur01.safelinks.protection.outlook.com/?url=http*3A*2F*2Flists.seas.upenn.edu*2Fmailman*2Flistinfo*2Ftypes-list&data=05*7C02*7Cbirkedal*40cs.au.dk*7Cb627001864384b43adea08dde661b0c1*7C61fd1d36fecb47cab7d7d0df0370a198*7C1*7C0*7C638920029495012116*7CUnknown*7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ*3D*3D*7C0*7C*7C*7C&sdata=a31Dub7GlosJlzVZkUS1yGuVTTNO6ndJTo*2BOVmtGm*2BM*3D&reserved=0__;JSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJQ!!IBzWLUs!RJ6C8YWYnk0dZux3qnspVBEBtCYUD-w61KxyvhrTo8tCBOUp3ohgzv3F78tLe9jyT-tm0AF-xYV6A9qAYyt3iqehgfb9Ng$ <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://eur01.safelinks.protection.outlook.com/?url=https*3A*2F*2Furldefense.com*2Fv3*2F__https*3A*2F*2Fdoi.org*2F10.1007*2F3-540-54415-1_61__*3B!!IBzWLUs!S8aJh356wvmDdcHzuNn_x-n_pAINEuB9OorQS4vpVVPxzpk6f1Frz6bXU2iKOmWU2eJnfiof4UvCQ7Pz7EY2e8iQYns02p8_gTB7LQ*24&data=05*7C02*7Cbirkedal*40cs.au.dk*7Cb627001864384b43adea08dde661b0c1*7C61fd1d36fecb47cab7d7d0df0370a198*7C1*7C0*7C638920029495027866*7CUnknown*7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ*3D*3D*7C0*7C*7C*7C&sdata=QTf8*2F4DIbLLd*2B1KizQiPehYbkUgblIzF0smTOv0JP2s*3D&reserved=0__;JSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJQ!!IBzWLUs!RJ6C8YWYnk0dZux3qnspVBEBtCYUD-w61KxyvhrTo8tCBOUp3ohgzv3F78tLe9jyT-tm0AF-xYV6A9qAYyt3iqcySc-46g$ <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://eur01.safelinks.protection.outlook.com/?url=https*3A*2F*2Furldefense.com*2Fv3*2F__https*3A*2F*2Fyoutu.be*2F6Ao9zXwyteY*3Fsi*3D5FdC5t5Mnyajmchz*26t*3D4660__*3B!!IBzWLUs!S8aJh356wvmDdcHzuNn_x-n_pAINEuB9OorQS4vpVVPxzpk6f1Frz6bXU2iKOmWU2eJnfiof4UvCQ7Pz7EY2e8iQYns02p8az4OKSg*24&data=05*7C02*7Cbirkedal*40cs.au.dk*7Cb627001864384b43adea08dde661b0c1*7C61fd1d36fecb47cab7d7d0df0370a198*7C1*7C0*7C638920029495041892*7CUnknown*7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ*3D*3D*7C0*7C*7C*7C&sdata=vm6uBPlAR8D5WQPbkb7HtqcIX0VJ7tkYjy6Oqcy3aBw*3D&reserved=0__;JSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSU!!IBzWLUs!RJ6C8YWYnk0dZux3qnspVBEBtCYUD-w61KxyvhrTo8tCBOUp3ohgzv3F78tLe9jyT-tm0AF-xYV6A9qAYyt3iqcspOWK6A$ <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://urldefense.com/v3/__https://eur01.safelinks.protection.outlook.com/?url=https*3A*2F*2Flists.seas.upenn.edu*2Fmailman*2Flistinfo*2Ftypes-list&data=05*7C02*7Cbirkedal*40cs.au.dk*7Cb627001864384b43adea08dde661b0c1*7C61fd1d36fecb47cab7d7d0df0370a198*7C1*7C0*7C638920029495055356*7CUnknown*7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ*3D*3D*7C0*7C*7C*7C&sdata=YFXaYzAGTV76u0LrEzMeybM*2Bes3qRseVCXGde*2BQgfiI*3D&reserved=0__;JSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJQ!!IBzWLUs!RJ6C8YWYnk0dZux3qnspVBEBtCYUD-w61KxyvhrTo8tCBOUp3ohgzv3F78tLe9jyT-tm0AF-xYV6A9qAYyt3iqcPo80EAg$ <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://eur01.safelinks.protection.outlook.com/?url=https*3A*2F*2Furldefense.com*2Fv3*2F__https*3A*2F*2Fcategorytheory.zulipchat.com*2F*narrow*2Fchannel*2F229199-learning.3A-questions*2Ftopic*2FContinuations.2C.20parametricity.2C.20and.20polymorphism*2Fwith*2F528479188__*3BIw!!IBzWLUs!Uf89Hb7uWjtbz4qUeFbMCVwfxkuye2lpB27Oi4vChhMV6yMPpA57jl2oZnBt3TaOOYa7UhjQTz16dPMUZoGtGubQesXT*24&data=05*7C02*7Cbirkedal*40cs.au.dk*7Cb627001864384b43adea08dde661b0c1*7C61fd1d36fecb47cab7d7d0df0370a198*7C1*7C0*7C638920029495068764*7CUnknown*7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ*3D*3D*7C0*7C*7C*7C&sdata=fyzk7Eo3sEP*2B68pTwiqYLVTVbjPZHM*2F0uYKGcsmYtPY*3D&reserved=0__;JSUlJSUlJSUlKiUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJQ!!IBzWLUs!RJ6C8YWYnk0dZux3qnspVBEBtCYUD-w61KxyvhrTo8tCBOUp3ohgzv3F78tLe9jyT-tm0AF-xYV6A9qAYyt3iqdH6_XKeA$ <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://eur01.safelinks.protection.outlook.com/?url=https*3A*2F*2Furldefense.com*2Fv3*2F__https*3A*2F*2Fcs.stackexchange.com*2Fquestions*2F136359*2Frigorous-proof-that-parametric-polymorphism-implies-naturality-using-parametrici*2F136373*136373__*3BIw!!IBzWLUs!Uf89Hb7uWjtbz4qUeFbMCVwfxkuye2lpB27Oi4vChhMV6yMPpA57jl2oZnBt3TaOOYa7UhjQTz16dPMUZoGtGpQSw3Ii*24&data=05*7C02*7Cbirkedal*40cs.au.dk*7Cb627001864384b43adea08dde661b0c1*7C61fd1d36fecb47cab7d7d0df0370a198*7C1*7C0*7C638920029495082083*7CUnknown*7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ*3D*3D*7C0*7C*7C*7C&sdata=myloZnDEu5BruPjy9iGqsPMN9la5dJFTB4ik6Bj1fRA*3D&reserved=0__;JSUlJSUlJSUlJSUlKiUlJSUlJSUlJSUlJSUlJSUlJSU!!IBzWLUs!RJ6C8YWYnk0dZux3qnspVBEBtCYUD-w61KxyvhrTo8tCBOUp3ohgzv3F78tLe9jyT-tm0AF-xYV6A9qAYyt3iqdu03m9cA$ <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://urldefense.com/v3/__https://eur01.safelinks.protection.outlook.com/?url=https*3A*2F*2Flists.seas.upenn.edu*2Fmailman*2Flistinfo*2Ftypes-list&data=05*7C02*7Cbirkedal*40cs.au.dk*7Cb627001864384b43adea08dde661b0c1*7C61fd1d36fecb47cab7d7d0df0370a198*7C1*7C0*7C638920029495095468*7CUnknown*7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ*3D*3D*7C0*7C*7C*7C&sdata=VY6mocf1F*2FIyL1SxD2Kk0qyG8kUfAzuiA8mM24uzk58*3D&reserved=0__;JSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUl!!IBzWLUs!RJ6C8YWYnk0dZux3qnspVBEBtCYUD-w61KxyvhrTo8tCBOUp3ohgzv3F78tLe9jyT-tm0AF-xYV6A9qAYyt3iqcR517yPg$ <https://lists.seas.upenn.edu/mailman/listinfo/types-list >
> > >>
> > >>
> > >> ------------------------------
> > >>
> > >> End of Types-list Digest, Vol 155, Issue 3
> > >> ******************************************
> > >>
> >
> >
>

More information about the Types-list mailing list