[TYPES] Types-list Digest, Vol 155, Issue 3

[Jon Sterling]

Hi, 

I don't have much to add to the conversation except a drive-by clarification:  there is absolutely no sense in which the extensional quotient of closed terms could serve as the initial model of System F (keeping in mind, however, that there's many possible notions of model of System F that we have to contend with if we wish to evaluate a claim of initiality). Being "made of terms" doesn't make something initial. The equational theory of System F could be taken to be the beta-equality theory, or the beta-eta equality theory depending on your perspective or tradition.

Best,
Jon


> On Aug 15, 2025, at 6:59 AM, 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
>> ******************************************
>>