Continuations, parametricity, and polymorphism · learning: questions

Are you all requiring function extensionality (not just eta) for both -> and forall in your definition of model for system F? I usually don't but some of these older papers do

Mike Shulman (Jul 03 2025 at 19:01):

Ryan Wisnesky (Jul 03 2025 at 19:50):

Section 3 of Tannen Coquand ('Extensional Models for Polymorphism', https://repository.upenn.edu/server/api/core/bitstreams/4eed61a9-05c6-453e-be1e-58b5f5f47bbd/content) gives a (the?) closed term model of system F, shows that it is not extensional, and shows how you can quotient it to get extensionality (section 4). (That it satisfies betais stated earlier on page 11.) So it seems like the closed term model may be parametric but not extensional, if that's even possible? Anyway, is the Tannen Coquand model equivalent to what people understand as the system F term model? FWIW I think both this thread and the HRR conclusion paragraph use "true in the term model" accidentally instead of "true in all models/provable from beta/eta alone" in many places

Mike Shulman (Jul 03 2025 at 20:04):

Mike Shulman (Jul 03 2025 at 20:08):

Oh, do you mean the axioms on p12 of TC, that functions are determined by their action on "elements"? That doesn't even make sense for a category theoretic model where types don't have "elements".

Mike Shulman (Jul 03 2025 at 20:10):

You could interpret elements as global elements i.e. maps from the terminal object, which in the term model are closed terms, but I certainly wouldn't expect functions in the term model to be determined by their action on closed terms.

Ryan Wisnesky (Jul 03 2025 at 20:11):

The paper writes the condition semantically, but you can just as easily add proof rules to the system F calculus (from x:T |- f x = g x for fresh var x infer |- f = g), which is usually what I've seen

Mike Shulman (Jul 03 2025 at 20:14):

Ryan Wisnesky (Jul 03 2025 at 20:14):

I do not believe funext and eta are equivalent here, or even in dependent type theories, although eta is a special case of funext

Mike Shulman (Jul 03 2025 at 20:14):

Those should always be the same. That's part of the point of the term model, that it satisfies only the provable equations and hence gives you completeness of the semantics.

Mike Shulman (Jul 03 2025 at 20:15):

(As long as

=

means definitional equality, and in a non-dependent type theory there's nothing else for it to mean.)

Ryan Wisnesky (Jul 03 2025 at 20:22):

hm, I grabbed the phrasing from Coq: Lemma functional_extensionality {A B} (f g : A -> B) :
(forall x, f x = g x) -> f = g. What did I do wrong? (it's a lemma b/c uses the dependent ext axiom)

Ryan Wisnesky (Jul 03 2025 at 20:31):

also: the term model should satisfy a lot more equations than just what is provable in the rules for system F. (The Tannen Coquand paper talks about this a bit). For example, the term model of O:nat and S:nat->nat and + proves x+y=y+x for variable x, whereas an arbitrary model does not. (at least if we're talking in Set, following Baader and Nipkow.). I thought this was the reason initial model semantics was "good" - you get all these extra properties not found in arbitrary models.

Mike Shulman (Jul 03 2025 at 20:36):

Mike Shulman (Jul 03 2025 at 20:38):

Not in any term model I'm familiar with. What is your definition of "term model"? I have always understood the term model to consist by definition of the terms modulo definitional equality.

Mike Shulman (Jul 03 2025 at 20:40):

They don't call it a "model" because they want to save that word for something that satisfies their additional semantic extensionality property, which of course the term model doesn't. But their section 3 is really the "term model".

Ryan Wisnesky (Jul 03 2025 at 20:49):

Ryan Wisnesky (Jul 03 2025 at 20:51):

example 3.5.9 shows there are equations that hold in the term algebra that don't hold in arbitrary algebras

Ryan Wisnesky (Jul 03 2025 at 20:55):

Mike Shulman (Jul 03 2025 at 20:59):

Ryan Wisnesky (Jul 03 2025 at 20:59):

Mike Shulman (Jul 03 2025 at 21:00):

In a theory with function-types, you can get away with using only closed terms because an open term can be abstracted over its free variables to yield a closed term.

Ryan Wisnesky (Jul 03 2025 at 21:01):

certainly they claim in the conclusion that their model "C" is made entirely of closed terms

Mike Shulman (Jul 03 2025 at 21:01):

But for instance the observation you quoted about

f(x,y)\approx f(y,x)

is not true in a term model with open terms, if

x

and

y

are free variables.

Ryan Wisnesky (Jul 03 2025 at 21:03):

sure, but I don't see how TC section 3 has free variables or open terms anywhere in its definition. This is why I think the term model for system F should have all kinds of equations true in it that aren't implied by the theory of F. The interpretation of a sequent that has variables in context uses the "environment" rather than an open term (a trick from closed term models of simply typed lambda calculus). I'd also be surprised they'd call it the "closed term/closed type construction" if it used open terms.

Ryan Wisnesky (Jul 03 2025 at 21:04):

I will agree that a model of system F with open terms as carrier will prove a lot less things than one with closed terms as carrier, according to my intuition

Mike Shulman (Jul 03 2025 at 22:56):

Okay, let's back up. Really explaining this in depth is going to require a broader view.

Ryan Wisnesky (Jul 03 2025 at 22:56):

I'm going to write to Prof Tannen. I think he might be able to settle some questions (eg is there an equation true in his term model of system F that doesn't follow from beta/eta) faster than us trying to work through his definitions

Mike Shulman (Jul 03 2025 at 22:57):

(The answer to that specific question is that it depends on what you mean by "equation" and "true", which I'll get to in a bit.)

Ryan Wisnesky (Jul 03 2025 at 22:57):

I do want to keep pressing on the (a?) closed term model of system F (instead of the open model), however, because to me that is what formalizes "idealized haskell w/o recursion"; it's what I have in my head when I write a big step operational semantics (the target is the closed term model)

Mike Shulman (Jul 03 2025 at 22:58):

Every theory is written in a "doctrine" that specifies the allowable judgment forms. You can extend a theory to a more expressive doctrine, and we often blur the distinction between a theory and its extension, but formally they are different and it's sometimes important to distinguish.

Mike Shulman (Jul 03 2025 at 22:59):

In particular, the term model of a theory is built out of the judgment forms that are derivable in its syntax. But what those are depends also on the doctrine, and thus the term model for a theory is different depending on what doctrine you write it in.

Mike Shulman (Jul 03 2025 at 23:00):

Theories like STLC and System F are written in doctrines whose judgment forms include contexts of variables, such as

x:A, y:B \vdash t:C

. Thus, their term models are built out of judgments of that sort, which are of course open terms.

Mike Shulman (Jul 03 2025 at 23:01):

The doctrine of STLC, with only "term variables", can be called "simple type theory", while the doctrine of System F, which also has type variables, could be called "polymorphic type theory".

Ryan Wisnesky (Jul 03 2025 at 23:02):

well sure, the closed term model of TC interprets judgements with variables in context, but the carrier for their interpretation is not open terms

Mike Shulman (Jul 03 2025 at 23:02):

Mike Shulman (Jul 03 2025 at 23:04):

The term model of a simple type theory is most directly viewed as some kind of multicategory, whose objects are the types and whose multi-morphisms such as

(A,B) \to C

are terms

x:A ,y:B \vdash t:C

. However, it's common to view it instead as an ordinary category whose objects are contexts (lists of types), and whose morphisms are substitutions (lists of terms).

If the theory has product types, this is equivalent to a category whose objects are single types and whose morphisms are terms in a singleton context such as

x:A \vdash t:C

. And even if the theory doesn't have product types, we can consider that category for simplicity.

Mike Shulman (Jul 03 2025 at 23:06):

If the theory has function types, then there is a bijection between open terms such as

x:A, y:B \vdash t:C

and closed terms of type

A\to B\to C

. Thus, in this case we could equivalently build the term model using only closed terms. This is what TC do in section 3, modulo some rearranging of their presentation to become a category, and ignoring the relation

\vDash

which I haven't gotten to yet.

Mike Shulman (Jul 03 2025 at 23:08):

In particular, the equality between terms in the section 3 model is the equivalence relation that they call

G_\omega

, which is defined to be the definitional equality of syntax. Thus, their term model qua category, like every term model, validates all and only the statements in the doctrine that are derivable in the theory.

Mike Shulman (Jul 03 2025 at 23:08):

Mike Shulman (Jul 03 2025 at 23:09):

In general it is true that a term model can satisfy additional statements that are not in its doctrine.

Ryan Wisnesky (Jul 03 2025 at 23:11):

in Baader-Nipkow example 3.5.9, the extra equations it satisfies are not part of the doctrine of the original equational theory?

Mike Shulman (Jul 03 2025 at 23:12):

Ryan Wisnesky (Jul 03 2025 at 23:13):

Ok, I'll need to pause to consider that. I've never really used doctrines before, and Baader/Nipkow don't talk about that point at all

Mike Shulman (Jul 03 2025 at 23:13):

If we formulate a simple algebraic theory in a doctrine without contexts, there is just one judgment

t\, \mathrm{term}

, with rules such as

Mike Shulman (Jul 03 2025 at 23:14):

Ryan Wisnesky (Jul 03 2025 at 23:14):

Mike Shulman (Jul 03 2025 at 23:15):

Then the term model in this doctrine is the set of all ("closed") terms such as

f(a,f(f(b,a),b)

built only from the constants

a,b,f

and no "variables".

Ryan Wisnesky (Jul 03 2025 at 23:15):

Mike Shulman (Jul 03 2025 at 23:16):

A statement like "for all

x

and

y

we have

f(x,y)=f(y,x)

" is not in this doctrine, and so it can hold in the term model even though it isn't "derivable from the theory".

Mike Shulman (Jul 03 2025 at 23:16):

However, we can also extend this theory to the doctrine of a simple type theory with judgments in context like

x:A, y:A \vdash f(x,y):A

and

\vdash a:A

, where

A

is the unique type. In this case, the term model will be the (multi)category freely generated by a semigroup object containing two elements that commute with each other. Of course such a semigroup need not be abelian, and therefore the two morphisms

(A,A)\to A

determined by the terms

x:A, y:A \vdash f(x,y):A

and

x:A, y:A \vdash f(y,x):A

are not the same, and so this term model does not satisfy the equation

x:A, y:A \vdash f(x,y)=f(y,x)

, which is in its doctrine.

Ryan Wisnesky (Jul 03 2025 at 23:18):

right, I'm still following. But for example 3.5.9, why isn't that equation that is only true in the term model not in the original doctrine (which had variables in context in its initial set of equations)

Mike Shulman (Jul 03 2025 at 23:18):

It will satisfy a statement like "for all closed terms

\vdash s:A

and

\vdash t:A

we have

\vdash f(s,t) = f(t,s)

", but this is not in its doctrine, since simple type theory does not include a way to quantify over closed terms.

Ryan Wisnesky (Jul 03 2025 at 23:21):

(also, I understand why function extensionality as I wrote it doesn't fit with system's F equational logic (it just follows from eta), albeit not b/c of a hyper doctrine reason. I'd never tried writing fun-ext outside of coq before)

Mike Shulman (Jul 03 2025 at 23:24):

Yes, good point. If we want to capture that whole example in a doctrine without contexts, we would have to include associativity in the doctrine itself rather than in the theory. So it would be in the doctrine of semigroups, and the theory in that doctrine would be the theory of two commuting elements, and so the term model would be the free semigroup generated by two commuting elements. (This is just like how associativity for morphism composition in a category, i.e. substitution of terms, is included in the doctrine of simple type theory, but not expressible in any theory in that doctrine.)

Mike Shulman (Jul 03 2025 at 23:25):

So, to conclude, the TC relation

\vDash

is a way of expressing statements about closed terms, which is not in the doctrine of simple type theory, and so the term model can satisfy statements of that form that are not derivable from the theory.

Ryan Wisnesky (Jul 03 2025 at 23:26):

ooh, heh, I get it now... I think. the "doctrine" defines what freeness is relative to. In which case, example 3.5.9 is "different" when you view it as the three axiom equational theory over the empty theory (as I do), or as a single ground equation over two (universally quantified) equations... right?

Mike Shulman (Jul 03 2025 at 23:30):

I wrote a longish blog post about doctrines, and more general "

n

-theories", here.

Ryan Wisnesky (Jul 03 2025 at 23:32):

ok, that explains (some of) the confusion with term models. For me (and I'd imagine TC), we just assume every statement in first order logic about the model is fair game to distinguish the models

Ryan Wisnesky (Jul 03 2025 at 23:33):

incidentally, CQL may provide a good example of "stacking" doctrines, its "instances" are theories in the doctrine of its schema which is a theory in the doctrine of its "typeside", if I understand correctly. Implementation-wise these are just theories that extend each other, but there are very specific rules about what kind of equations can be written where in this stack.

Mike Shulman (Jul 03 2025 at 23:34):

The confusion is that the TC syntax for

\vDash

looks the same as the syntax for definitional equality in the doctrine. It would be better if instead of

\vDash x:A, y:B ; M = N

they wrote something like

(\vdash x:A), (\vdash y:B) \vDash (\vdash M = N)

Mike Shulman (Jul 03 2025 at 23:35):

Yes, a doctrine is a 2-theory, which is a 2-theory in some 2-doctrine (= 3-theory), and so on.

Ryan Wisnesky (Jul 03 2025 at 23:37):

I think im still going to write to prof. tannen asking about properties true in his closed term model that don't follow from beta/eta, but then we can check them to see if they fall into the expected doctrine or not. does that sound like a good next step?

Mike Shulman (Jul 03 2025 at 23:38):

Ryan Wisnesky (Jul 03 2025 at 23:39):

I want to know if HRR's Q = S is true in the closed TC model, even if that question is ill-posed doctrinally. It's true in the closed TC model after they collapse it, because collapse creates a PER model

Mike Shulman (Jul 03 2025 at 23:41):

Ryan Wisnesky (Jul 03 2025 at 23:41):

no one has made that claim, it's a claim I need to figure out to check my understanding

Mike Shulman (Jul 03 2025 at 23:41):

Ryan Wisnesky (Jul 03 2025 at 23:42):

I think they say collapse results in a PER somewhere, I'll go find the reference

Mike Shulman (Jul 03 2025 at 23:43):

I want to not be too blithe about it, because there could be multiple meanings of what "being a PER model" is, and it doesn't seem to me that simply quotienting the term model could create the kind of "PER model" that makes Q=S.

Ryan Wisnesky (Jul 03 2025 at 23:43):

lemma 4.3 says something is a PER, although maybe not the kind of PER HRR talk about

Ryan Wisnesky (Jul 03 2025 at 23:44):

Mike Shulman (Jul 03 2025 at 23:46):

Okay. Pre-collapse we know that it is not true in the ordinary sense as a statement about the term model qua category, because of the HRR counterexample. But I guess there may be a way to interpret it as a different statement involving

\vDash

, which might be true.

Ryan Wisnesky (Jul 03 2025 at 23:47):

my hunch is all these properties that are ruled out doctrinally actually do conspire to equate Q=S in the specific closed term model of TC, and HRR meant open term model or "all models"

Mike Shulman (Jul 03 2025 at 23:49):

I'm not sure what you mean by hyper-doctrinally. I haven't been talking about any hyperdoctrines.

Ryan Wisnesky (Jul 03 2025 at 23:50):

Mike Shulman (Jul 03 2025 at 23:50):

I also don't know what you mean by distinguishing the closed term model and open term model. As I said, I think there is no difference between them in a theory with function types; what makes the difference is what's in the doctrine.

Mike Shulman (Jul 03 2025 at 23:51):

Oh, I see. It's very confusing that a "hyperdoctrine" is totally unrelated to a "doctrine" in this sense.

Ryan Wisnesky (Jul 03 2025 at 23:52):

I'll find the reference - I think it was hasegawa - who was talking about the differences between the open and closed term models of system F

Ryan Wisnesky (Jul 03 2025 at 23:53):

Ryan Wisnesky (Jul 04 2025 at 00:00):

while we're revisiting very basic assumptions, I always thought the logical relations lemma was proved by induction on closed terms or types, so it surprises me when a closed term model isn't parametric. but as this thread makes clear, I'm full of erroneous assumptions if someone wants to correct this one too

Mike Shulman (Jul 04 2025 at 01:18):

I can't get to that paper either, so I don't know what this putative closed term model might mean. But I do know that it's nearly impossible to prove anything by induction only over closed terms: when you get to the case for

\lambda x. M

, you don't have an inductive hypothesis since

M

isn't a closed term any more. The logical relations lemma that I know is proved by induction (i.e. by the universal property) on the ordinary (open) term model. (And, remember that that's only external parametricity.)

Mike Shulman (Jul 04 2025 at 01:18):

Ryan Wisnesky (Jul 04 2025 at 01:26):

Mike Shulman (Jul 04 2025 at 01:32):

Well, I can't make heads or tails of Hasegawa's introduction, and nowhere in the paper do I see a definition of what he means by a model of open terms. His model of "closed terms" (which he calls just an "interpretation") looks to me like it is equivalent to I would call the ordinary term model, by the trick that I mentioned of abstracting open terms to make them closed.

Mike Shulman (Jul 04 2025 at 01:34):

Ohh... maybe by "open terms" he means a model in which the "elements" of a type are the union of the terms of that type in all contexts? Or, put more categorically, in which the morphisms

t:(A,B)\to C

are terms of the form

\Gamma_t, x:A, y:B \vdash t:C

for some additional context

\Gamma_t

, which could be different for different morphisms

t

Mike Shulman (Jul 04 2025 at 01:35):

I've seen people do things like that for untyped lambda-calculus, so maybe people do it for typed lambda-calculus too. It certainly wouldn't be the initial model, but it might be useful for some things.

Ryan Wisnesky (Jul 04 2025 at 01:39):

if the trick of an interpreting a term in context via its corresponding closed lambda term really set up an equivalence of models, why would the closed one fail to be extensional but the open would not? my intuition is that these closed models must be doing something differently than just using the equivalent lambda term or there wouldn't be all these papers by well-known authors about how to turn the closed model extensional... but we might be approaching the point where it's easiest to ask the authors

Mike Shulman (Jul 04 2025 at 02:08):

It's an equivalence between what TC and Hasegawa call the "closed term model" and what I call "the term model" which involves terms in context that only use the variables from that context. I don't think the latter is what Hasegawa means by an "open term model" -- I think he means what I suggested above, where the terms can also involve additional free variables that aren't in the context. That model can be "extensional" for trivial reasons because you can always apply two functions

f,g:A\to B

to a free variable

x:A

and then if

f\,x = g\,x

it must be that

f=g

by eta.

Madeleine Birchfield (Jul 04 2025 at 02:22):

I renamed this discussion because it has veered far from the original topic of comparing synthetic algebraic geometry to continuations. This deviation happened at the beginning of the discussion once it became clear that the SQC axiom wasn't all that similar to the axioms that types are isomorphic to its continuations.

Ryan Wisnesky (Jul 04 2025 at 02:27):

I found and attached the paper hasegawa cites when he says "the open model is used to prove completeness". section 3 uses an argument like you just made, but I can't settle your question from reading it quite yet.
second-order-semantics.pdf

Ryan Wisnesky (Jul 06 2025 at 00:10):

Screenshot 2025-07-05 at 4.39.55 PM.png
Screenshot 2025-07-05 at 4.40.33 PM.png
I'm still trying to square the fact that the term model of the simply typed lambda calculus is sound and complete for the equational theory of the STLC (I've gone through this proof many times), but that you can, according to Baader/Nipkow/Mitchell and many others, still end up with a "term model" of an equational theory that has more equations true in it than specified (and that this fact is used in algebraic specification, for example, you can choose from 'initial model' and 'final model' semantics, with entire papers about the differences). doctrines may help formalize what's going on, but I'm getting more confused rather than less. I've included some images from Baader/Nipkow that indicate whatever is going on is related to having infinitely many variables, and also an image of Mitchell talking about how "no junk, no confusion" in the initial model refers to ground terms (not open terms). I'll keep thinking, but if anyone can explain this difference, please chime in. the difference is even weirder in my mind when I consider the point-free form of the STLC, since that has no variables and so should be amendable to analysis from universal algebra.
Screenshot 2025-07-05 at 5.03.03 PM.png
Screenshot 2025-07-05 at 5.02.56 PM.png

Ryan Wisnesky (Jul 06 2025 at 00:21):

I think the remark in 3.5.8 means that b/c example 3.5.9 uses quantified equations, its ground term model may satisfy quantified equations that are not provable from the original equational theory (as the example shows), and that this is a general phenomenon - ground models of quantified equations will have many more (quantified) consequences than models with variables. which is the "usual situation" where I grew up - ground term models of theories with variables. but I get why this situation isn't fully satisfactory for all times, and why you'd want variables in your term model.

Mike Shulman (Jul 06 2025 at 00:25):

Yes, we already discussed that -- BN's initial algebras are in a doctrine without contexts, while the "identities" they consider are in a nonempty context.

Ryan Wisnesky (Jul 06 2025 at 00:27):

never having used doctrines before, I have to work all this out in BN/mitchell terms, and I'm being very careful anticipating writing this up, thanks for sticking with me

Mike Shulman (Jul 06 2025 at 00:27):

The thing about cardinality of variables is an extension of that: if instead of the initial algebra (

X=\emptyset

) you consider the free algebra on a set of generators

X

, then any equation in a context of length

\le |X|

can be instantiated using distinct generators for the variables, and since it's free on the generators it won't satisfy any such equations that don't follow from the theory even with contexts.

Ryan Wisnesky (Jul 06 2025 at 00:29):

this new set of messages is about how the term model of the STLC manages to avoid this phenomenon, b/c I thought you could encode the point-free version of STLC equationally

Mike Shulman (Jul 06 2025 at 00:30):

Ryan Wisnesky (Jul 06 2025 at 00:30):

Mike Shulman (Jul 06 2025 at 00:30):

Ryan Wisnesky (Jul 06 2025 at 00:30):

Mike Shulman (Jul 06 2025 at 00:31):

Mike Shulman (Jul 06 2025 at 00:32):

Ryan Wisnesky (Jul 06 2025 at 00:32):

Screenshot 2025-07-05 at 5.32.10 PM.png
this is for a BCCC and some other stuff, but it's the language with "curry" and "eval" etc - the original "categorical machine language", actually

Mike Shulman (Jul 06 2025 at 00:33):

What I'd need to see to understand that is the typing judgments, not the raw terms.

Ryan Wisnesky (Jul 06 2025 at 00:33):

Ryan Wisnesky (Jul 06 2025 at 00:34):

Ryan Wisnesky (Jul 06 2025 at 00:36):

so specifically, assuming these "equations" are actually equations the sense of Baader Nipkow, I'm trying to compare its ground term model against the usual one for STLC that is sound/complete for beta/eta only

Mike Shulman (Jul 06 2025 at 00:41):

Mike Shulman (Jul 06 2025 at 00:43):

The analogue of the BN observation about "extra equations" would apply here to equations of the form

x:\alpha\to\beta, y:\gamma\to\delta \vdash M=N

in a context where you've assumed a couple of morphisms in the free CCC, which is not a statement in the variable-free doctrine of this theory.

Ryan Wisnesky (Jul 06 2025 at 00:43):

the ground term model of the equations suffers from the phenomenon that it will have quantified equations true in it that don't follow from the equations (according to BN 3.5.8 remark). But the free CC is sound/complete for the equations. that's the contradiction I don't understand

Mike Shulman (Jul 06 2025 at 00:44):

If you pass that back to ordinary STLC with variables, you would get something like

x : (a:\alpha \vdash t:\beta), y : (c:\gamma \vdash s:\delta) \vdash M=N

, which is also not in the doctrine of STLC since it quantifies not over internal variables but over judgments.

Mike Shulman (Jul 06 2025 at 00:44):

Ryan Wisnesky (Jul 06 2025 at 00:44):

Ryan Wisnesky (Jul 06 2025 at 00:45):

Ryan Wisnesky (Jul 06 2025 at 00:47):

what happens if we just roll with it. like, are there "extra equations" that hold in the ground term model but not in the usual model? I see how "extra equations" they can be consider ill-formed, but for other purposes, they are still well-formed. like, they seem to have determine truth-values (being true or false in each model)? I ask because to my understanding of "haskellers", for blog post purposes these extra equations may be part of "Haskell's term model"

Ryan Wisnesky (Jul 06 2025 at 00:55):

hm, I also don't understand why "passing back" does anything at all - the original equation with x and y seems like it is already an equation of ordinary STLC, but that may be because of lack of knowledge of doctrines. in fact, conflating the two may be another common mistake to write about

Mike Shulman (Jul 06 2025 at 01:59):

I don't know what you mean by distinguishing a "ground term model" from a "usual model". Each theory in a given doctrine has a definite specific term model.

Ryan Wisnesky (Jul 06 2025 at 02:03):

By "the usual model", I mean the free CCC as defined in sec 7/8 of https://www.cl.cam.ac.uk/teaching/1617/L108/catl-notes.pdf . By "the ground term model", I mean the ground term model of the "lambeck" form of STLC (with curry, eval, etc) from wikipedia

Ryan Wisnesky (Jul 06 2025 at 02:05):

I'd like to find an example of an "extra equation" that holds in the ground term model that does not hold in the usual model, which I claim is possible since "quantification over judgements" is still well-defined, if not internalized in the stlc

Mike Shulman (Jul 06 2025 at 02:11):

Mike Shulman (Jul 06 2025 at 02:13):

Each of them satisfies internally exactly the equations in their doctrine that are derivable from the theory, and each of them can satisfy additional equations that are not in the doctrine. The difference is that one of them has an "internal" notion of "variable" while the other is formulated without such, but there is still a bijection between the "internal" equations on both sides and also a bijection between the "external" equations on both sides.

Ryan Wisnesky (Jul 06 2025 at 02:17):

if "each of them can satisfy additional equations that are not in the doctrine", then what is an example equation, not in the doctrine, that one satisfies that the other doesn't (that's my previous question), or must they satisfy the same set of equations not in the doctrine?

John Baez (Jul 06 2025 at 02:36):

This sounds a bit off because doctrines aren't mainly a technical device one "uses" in a problem like this - e.g., people have argued for many years about the correct definition of doctrine, but that doesn't stop anyone from talking about doctrines, because they mainly serve as a way of thinking that keeps one from getting confused. In this particular case Mike seems to keeps using them to say roughly "the stuff you do when you do logic with contexts is different from the stuff you do in logic without contexts, so just because something is initial when you're working without contexts, doesn't mean some similar-looking thing is gonna be initial when you're working with contexts". See, I said that without saying "doctrines", but Mike said it faster by saying the word "doctrines".

I don't understand what you guys are talking about, except for the part about how you gotta be careful which doctrine you're working in. It's a very general point, like how you can't say an object is initial until you've made up your mind what category it's an object in.

Ryan Wisnesky (Jul 06 2025 at 02:46):

I think we're making progress, if testing Mike's patience. At present, there's two models of the simply typed lambda calculus we're trying to compare, one defined as the ground term model (in Baader Nipkow sense) of the "lambeck equations" as defined in wikipedia, the other being the free cartesian closed category as usual. These are so similar that teasing them apart (if they can be teased apart at all) may require what we've been calling "extra equations", which as I understand it can be formalized using doctrines

Mike Shulman (Jul 06 2025 at 02:46):

They must satisfy the same set of equations not in the doctrine because they are the same object.

Ryan Wisnesky (Jul 06 2025 at 02:46):

heh, that would explain why I can't come up with an example myself and had to ask...

John Baez (Jul 06 2025 at 02:50):

So you see, "teasing them apart" is mainly about teasing apart the two doctrines. So you gotta listen when people talk about doctrines, even if they never say exactly what a doctrine is in full generality (since nobody knows, although maybe Mike does).

Ryan Wisnesky (Jul 06 2025 at 02:50):

I take the absence of an example here to mean that although a ground term model (in the BN sense) may satisfy extra equations, it doesn't have to, or any that it does are already true in the free CCC (which is I think is the case here, any "extra theorems" in the ground term model are true in the free CCC, following from the free CCCs initiality)

John Baez (Jul 06 2025 at 02:51):

Is there a guy named Lambeck in addition to the famous guy named Lambek, or is this some joke about Lambek and Beck?

Ryan Wisnesky (Jul 06 2025 at 02:52):

John Baez (Jul 06 2025 at 02:52):

Ryan Wisnesky (Jul 06 2025 at 02:56):

fwiw, it sounds like much of the field of "algebraic specification", where you study the "extra equations" that arise in the ground term model of an equational theory, can be explained in doctrinal terms. there may be two blog posts here, one on folklore about system F and one about how doctrines relate to old school algebraic specification

Ryan Wisnesky (Jul 06 2025 at 03:30):

bearing with me as I apply all of what happened today to the original questions about system F, I now conclude 1) Reynolds parametricity implies Q~Cont(Q) , and 2) the term model of system F is not reynolds-parametric (any "extra equations" from today can't "conspire to make it so", as was my original concern). I'd still like to find citations/proofs for these though. anyway, I have no further questions for now and will go back to writing.

Mike Shulman (Jul 06 2025 at 04:17):

I agree if instead of "parametric" you say internally parametric. I maintain the term model is externally parametric by the usual argument.

Ryan Wisnesky (Jul 06 2025 at 04:22):

hm, I mean parametric in the sense of the HRR conclusion. I think they must have meant "internal" too, in which case they are saying its a failure of the externally parametric term model to be internally parametric, which squares with what we saw earlier with bridge discreteness etc. When put that way it doesn't seem surprising to me anymore

Ryan Wisnesky (Jul 06 2025 at 05:26):

checking my understanding again: the plotkin-abadi identity extension lemma implies equality of two variables (rather than closed terms); therefore, the plotkin-abadi logic is axiomatizing internal parametricity. Nevermind: this was confirmed earlier in the thread

Ryan Wisnesky (Jul 06 2025 at 07:33):

Ok, I've summarized my conclusions from this thread into the following list; some entries are sanity checks and some go against folklore, but all should be correct. the blog post will refer to many or most of these propositions. I don't have any more questions, and appreciate everyone's patience.

1) external parametricity does not imply q ~ cont q (evan,mike)

2) internal parametricity implies q ~ cont q (evan,mike)

3) internal parametricity implies c ~ cont c for every closed type c  (b/c closed types are bridge discrete) (evan,mike)

4) internal parametricity doesnt imply a ~ cont a for variable a (internal parametricity of forall a, forall r, ((a->r)->r) does not help (mike); need bridge discreteness for a variable) (evan,mike)

5) system F term model is external but not internal parametric (HRR)

6) models of reynolds-abadi logic are internally parametric (mike)

7) external parametricity implies forall x, x -> x has one inhabitant (need reference)

8) the term model for system F is sound and complete for beta and eta (mike), same as with STLC (course notes)

9) "extra equations" (in the sense of BN) in the ground term model of the Lambek equational theory from wikipedia are meta-theoretic (not theoretic) statements about the free CCC that follow from initiality

10) extensional PER models are internally parametric (not 100% sure about this one / need reference)

11) in the early 90s many authors required models of system F to be extensional, a property they always expressed semantically (and different than eta) (tannen)

12) in the early 90s many authors distinguished between "open" and "closed" term models of system F for extensionality reasons, but "open" and "closed" may have unusual meanings in these papers (mike)

13) not all polymorphic functions in system F define natural transformations on definable functors (since not all type constructors are functorial, e.g. X |-> X->X) (reddy)

14) all polymorphic functions between (definable) functors are natural transformations in an internally parametric model, but not an externally parametric model (b/c q not iso to Cont q; need reference)

15) initial algebras and final coalgebras for positive defineable functors exist in an internally parametric model of system F (wadler)

16) eta implies a kind of function extensionality in system F (mike, mitchell)

17) in system F, both internal and external parametricity are meta-theoretic properties

18) internal parametricity (conclusions hold in all contexts) implies external parametricity (conclusions hold in empty contexts) for system F

Mike Shulman (Jul 06 2025 at 16:15):

Madeleine Birchfield (Jul 06 2025 at 22:14):

Mike Shulman (Jul 06 2025 at 22:57):

(3) certainly depends on what theory we're talking about. It's not true in internally parametric dependent type theory, for instance, because universes are closed and not bridge-discrete. Evan showed essentially that all closed types in the first universe are bridge-discrete, which would imply that in a simple predicative type theory without universes all closed types are bridge-discrete; but his proof doesn't treat an impredicative universe or

\forall

, so it's not clear to me at the moment whether all closed types in System F are bridge-discrete.

(14) This depends on (3) (since automatic naturality for transfomations Reader->Id implies a ~ cont a), so it also varies with the theory, is false (or at least probably not true) for dependent type theory, and is unclear to me whether it's true for System F.

(17) I'm not sure what you mean by this for internal parametricity. Normally I think of internal parametricity as a built-in part of a theory, not a metatheoretic statement about it, hence the "internal".

Ryan Wisnesky (Jul 07 2025 at 02:04):

Mike Shulman (Jul 07 2025 at 02:07):

Ryan Wisnesky (Jul 07 2025 at 02:09):

re: 3) I meant system F, so it's good to note your uncertainty. I'm not sure if bridge discreteness follows from internal parametricity as formulated by Reynolds abadi (or anyone else), and regard 3) as key to settling.

Ryan Wisnesky (Jul 07 2025 at 02:09):

Ryan Wisnesky (Jul 07 2025 at 02:10):

Ryan Wisnesky (Jul 07 2025 at 02:13):

re: 16, I'm used to distinguishing eta from function extensionality due to working in Coq so much. I've never seen fun-ext follow from eta. So I was surprised to learn that (x |- f x = g x -> |- f = g) follows from eta in System F, even though it's due to issues with having a type of propositions, etc. Mitchell gives the same argument about this that you did earlier.

Ryan Wisnesky (Jul 07 2025 at 02:21):

for 17) I'm using "internal and external in the sense of 18). But I agree there's another meaning of internal and external meaning that internally you can have a Prop stating that e.g. function extensionality is true which is distinct from it being true externally. I tried to use "definable" instead of "internal" in this bullet list to avoid ambiguity in this specific sense. What I meant by the question was that it seems like people need to build a logic on top of system F (a la plotkin abadi), rather than say add a bunch of 'free theorems' to system F, to capture parametricity. I was trying to confirm you have to do more than just add (infinitely many) equations to the theory of system F to capture internal parametricity.

Mike Shulman (Jul 07 2025 at 05:57):

As I said before, if = means definitional equality, then that rule is not funext. It is not even a "kind" of funext, unless you want to call eta itself "a kind of funext", because this rule is equivalent to eta.

Mike Shulman (Jul 07 2025 at 05:58):

Mike Shulman (Jul 07 2025 at 06:00):

I'm not even sure what you mean by "parametricity" in (17-18). What I mean by "external parametricity" is that there's a translation on syntax transforming every closed type

A

to a relation on its closed terms, defined in the usual way, such that every closed term is related to itself. What I mean by "internal parametricity" is that the syntax contains an operation mapping every type to a relation on itself, defined in the usual way, such that every term is related to itself.

Nathanael Arkor (Jul 07 2025 at 14:32):

I've not been following this discussion so closely, but it seems like Abadi, Cardelli, and Curien's work on Formal Parametric Polymorphism may be related, as they give a calculus extending System F in which certain parametricity results are provable internally.

Mike Shulman (Jul 07 2025 at 16:30):

Thanks. That looks similar to the Plotkin-Abadi logic we've been discussing; in fact I'm not sure what the difference is. They cite the Plotkin-Abadi paper in the last sentence but it's not clear to me what they're saying about it.

I think I would classify both of them as a way to add "internal parametricity" to System F. (Full internal parametricity requires a dependent type theory.) But I could be misunderstanding something about one or both.

Ryan Wisnesky (Jul 07 2025 at 17:55):

I got the internal/external parametricity distinction (applies in all contexts vs applies in empty context) from here: https://ncatlab.org/nlab/show/parametric+dependent+type+theory . Without a type of propositions, I'm not even sure how system F could "internalize" (mike's sense) parametricity (besides an axiom schema of 'free theorems').

Ryan Wisnesky (Jul 07 2025 at 17:58):

internal vs external in the sense of that ncatlab page seemed relevant, since a ~ CPS a when a is a variable has different properties than c ~ CPS c when c is a closed term

Mike Shulman (Jul 07 2025 at 18:16):

The distinction is correct, but the "thing" that applies in contexts or not is not the conclusions, but the parametricity operator that takes types to relations and terms to witnesses of relations.

Also that nLab page is only about forms of parametricity that are inside the theory:

In particular, as it says, it uses "external parametricity" for "explicit external parametricity", which is different from the meta-theoretic external parametricity of Reynolds:

Basically all constructive type theories satisfy meta-theoretic external parametricity. But I don't know what "meta-theoretic internal parametricity" would even mean.

Explicit parametricity is indeed harder to make sense of in a non-dependent type theory, but I thought that's what the Plotkin-Abadi and Abadi-Cardelli-Curien logics were trying to do.

Ryan Wisnesky (Jul 07 2025 at 18:21):

I figured "meta-theoretic internal parametricity" meant a parametricity result that also applies to open terms. at least, that's how I used internal/external in the list of items. if that's not a germane distinction for system F, I'll need to re-think the list

Mike Shulman (Jul 07 2025 at 18:25):

If you can point to a paper that does something you would describe as "meta-theoretic internal parametricity", I'd be interested. Otherwise, let's not use that phrase.

Note that ordinary meta-theoretic external parametricity does do something with open terms, as it essentially must in order to give a proof by induction over syntax in a theory with variable binding. Namely, it shows that open terms map related values for their free variables to related outputs, just like abstracted functions.

Ryan Wisnesky (Jul 07 2025 at 18:30):

In my ignorance I'd point at that automated free theorem generator website from a week ago as something that distinguishes closed vs open terms in a parametricity result : it could generate a free theorem for "forall a, forall x, (a->x)->x", but not for "forall x, (a->x)->x" with a left a type variable. could just be a limitation of the tooling however, or a meaningless distinction (which I suppose it must be)

Ryan Wisnesky (Jul 07 2025 at 18:33):

to make progress, I need to figure out what to replace "internal" and "external" with in each item of the list... so that's what I'll be doing next

Mike Shulman (Jul 07 2025 at 18:40):

Ryan Wisnesky (Jul 07 2025 at 18:45):

fair enough, then in that case the question is, do the distinctions (exclusively) explain any of the phenomena on that list, like I erroneously thought they did, and if they don't, what does... so that's what I'll be thinking through, item by item

Mike Shulman (Jul 07 2025 at 18:45):

But if you apply meta-theoretic external parametricity to an open type, you get an open type that depends on relations corresponding to the free variables. Which is basically the same as if you abstracted over the free variables with forall, applied the "closed term" translation, and then peeled off the corresponding abstractions. So in that sense, the "open terms" translation that's part of external parametricity carries no new information, so it makes sense that the free theorem generator doesn't deal with it. I was just making the point that in order for the induction to go through, the open terms have to be dealt with at some point.

Ryan Wisnesky (Jul 07 2025 at 18:46):

side note: I don't always get indications that you're typing, mike. must be a weird intermittent glitch. I didn't mean to interrupt

Mike Shulman (Jul 07 2025 at 18:48):

Mike Shulman (Jul 07 2025 at 18:51):

I don't know if you're as wrong as you seem to think. Most of the places on that list where you distinguished external and internal parametricity seemed correct to me with the meaning of "internal parametricity" that I'm most familiar with, namely explicit internal parametricity in a dependent type theory.

Mike Shulman (Jul 07 2025 at 18:53):

I think the main thing that I don't understand yet is how the Plotkin-Abadi and Abadi-Cardelli-Curien theories are related to each other and to explicitly internally parametric dependent type theory. In particular, to what extent does my intuition for the latter carry over to them.

Mike Shulman (Jul 07 2025 at 18:53):

I think a good answer to this question should resolve most of the open issues on your list.

Ryan Wisnesky (Jul 07 2025 at 18:56):

that's good to know - and I use Coq a lot more than system F - but I am also fixated on answering these for system F to get at "haskell" folklore for blogging reasons. that being said, I'm thinking of starting with a blog post that just compares the folklore that "the term model of STLC is sound/complete for beta/eta" with folklore that "equational specifications (lists, trees, etc) are studied by their inductive theories", because I think the subtleties of doctrine involved here are often under-stated even in textbooks that use both frameworks (such as Mitchell's)

Mike Shulman (Jul 07 2025 at 19:03):

Josselin Poiret (Jul 08 2025 at 09:01):

Madeleine Birchfield (Jul 08 2025 at 13:54):

What's an example of a dependent type theory with a primitive that breaks Reynolds external parametricity?

Josselin Poiret (Jul 08 2025 at 14:14):

Josselin Poiret (Jul 08 2025 at 14:15):

Josselin Poiret (Jul 08 2025 at 14:21):

i'd love to go back to the original question though, as there's definitely a flavor of getting first order information back out of higher order in SQC: an example is being able to derive ((x = 0) → ⊥) → x invertible

Josselin Poiret (Jul 08 2025 at 14:25):

morally a proof of (x = 0) → ⊥ has to go through some proof that (0 = 1), but in that case you do know that 1 = x*i in the current stage

Mike Shulman (Jul 08 2025 at 15:19):

Hmm, interesting. I'm used to thinking of constructivity as the condition ensuring that a theory has a good initial algebra semantics with a gluing construction, which generally implies parametricity as well as canonicity and (with some extra work) normalization. Typecase doesn't really fit well into my mental models. How do you prove canonicity and normalization for a theory with typecase?

Mike Shulman (Jul 08 2025 at 15:19):

Josselin Poiret (Jul 08 2025 at 15:48):

When you're doing a normalization model for a type theory, you have 2 choices for the interpretation of the universe (and that of the type judgments): positive or negative. The negative version is what you have in mind: a record of abstract relations that verify the minimal interface wrt. neutrals and normal forms. The positive version instead asserts that you already know all types, here are all the codes, and when you need the relation on terms you have a decoding function.

Josselin Poiret (Jul 08 2025 at 15:49):

so the negative model lets you prove parametricity results because you can feed it external relations, but the positive model supports typecase

Mike Shulman (Jul 08 2025 at 16:18):

Interesting. So is typecase the "only" constructive alternative to parametricity then? Can you cite some references that prove canonicity/normalization with typecase?

Josselin Poiret (Jul 08 2025 at 16:30):

I don't think there's a way to formalize this sentence, but intuitively I don't know of any other way to formalize types: it's either of an inductive type of codes or a negative record

Josselin Poiret (Jul 08 2025 at 16:31):

not that i know of (but i haven't looked into it too hard) but it seems pretty straightforward to add to any formalization that uses the positive interpretation

Mike Shulman (Jul 08 2025 at 16:34):

Mike Shulman (Jul 08 2025 at 16:36):

It's interesting that there are multiple ways to construct a universe semantically. That isn't the case for any other type constructors that I know of, because they all have a universal property and hence are uniquely determined up to isomorphism. I guess these two approaches correspond basically to choosing a "handedness" of universal property to give to the universe semantically. And if you try to incarnate those universal properties syntactically, then on the one hand you get typecase, and I guess on the other hand you get... univalence?

Josselin Poiret (Jul 08 2025 at 16:51):

All formalizations of logical relation arguments for dependent type theory that I know use it: LogRel-Coq is an example ofc (or LogRel-MLTT if Agda is more your cup of tea)

Josselin Poiret (Jul 08 2025 at 16:52):

Mike Shulman (Jul 08 2025 at 16:59):

Internal parametricity is certainly inspired by a negative view of the universe, but it isn't a universal property. Univalence is basically a universal property, it says that the universe is a classifying space.

Josselin Poiret (Jul 08 2025 at 17:00):

Mike Shulman (Jul 08 2025 at 17:04):

Umm... hang on. Maybe I'm misreading that code, but it looks to me like just the usual inductive definition of logical relations over types. That's different from interpreting the universe as an inductive type in the model.

Maybe I don't know the right words to say syntactically to make this point. Categorically, the way these arguments work is that you have a syntactic category which is initial among categories with some structure. You consider some canonical map out of it, like the global sections functor if you're proving canonicity, and then you take the comma category over that functor to make a "glued" category living over the syntactic category, whose objects are "types equipped with a logical relation" or something. You prove that the glued category has the same structure as the syntactic category, and then you observe that since the syntactic category is initial, there's a section of the projection down to it from the glued category, where the section assigns to each type its logical relation.

It looks to me like what you pointed to is talking about the definition of the section. This is always inductive over types (i.e. objects of the syntactic category) because the syntactic category is always initial, never terminal. But I thought we were talking about defining the "universe object" in the glued category, whether it has a positive or a negative universal property as an object of that category.

Notification Bot (Jul 08 2025 at 17:41):

Josselin Poiret (Jul 09 2025 at 09:07):

so in that Agda code (and also the Rocq one) there's a bit of indirection, but if you look at the reducibility predicate at the universe, it uses the type reducibility predicate of the lower level (the definition here is quantified over a so-called LogRelKit of lower levels), which is itself obtained by the definition I linked to before

Josselin Poiret (Jul 09 2025 at 09:09):

also, this is not the definition of the section: the section is usually called the "fundamental theorem" and is in fact defined in Fundamental

Josselin Poiret (Jul 09 2025 at 09:16):

i'm a bit more used to the categorical gluing argument à la STC for dependent type theories, and in that formalism you're basically considering two different definitions for the dependent presheaf over

ρ^*(Ty)

where

ρ

is what Jon calls a figure shape

Josselin Poiret (Jul 09 2025 at 09:16):

(and where

Ty

is the presheaf over the syntactic category of contexts of syntactic types)

Josselin Poiret (Jul 09 2025 at 09:17):

Josselin Poiret (Jul 09 2025 at 13:25):

wrt. SQC, it's the axiom that internally to the zariski topos, the canonical map

A → (\mathrm{Hom}_{fp}(A,R) → R)

is invertible for

A

a finitely presented

R

-algebra

Mike Shulman (Jul 09 2025 at 16:42):

Mike Shulman (Jul 09 2025 at 16:43):

Hmm, isn't _⊩¹U the reducibility predicate on the universe? I thought _⊩¹U_∷U/_ would be the proof that all terms in the universe are reducible. Am I reading that code wrong?

Ignat Insarov (Jul 10 2025 at 16:25):

What is the minimal background or summary needed to understand this conversation? I want to understand if parametric functions have free theorems attached or not. I tried reading articles of John Reynolds and Philip Wadler, but I was not able to follow them all the way. Now it seems they were wrong?

I can see that a term of type

∀ x. (x → x) → (x → x)

does not denote a natural transformation because the type

∀x. (x → x)

does not denote a functor. That about sums up what I understood from scrolling through this conversation. I want to understand more but I am dazzled by the expanse of techniques deployed.

If anyone is writing an explanation of this issue, I can be a good representative of general audience and help make it accessible!

Ryan Wisnesky (Jul 10 2025 at 16:37):

the place I'm stuck is finding a complete proof that Reynolds parametricity for system f does or does not imply c ~ CPS c for all closed types c.

Mike Shulman (Jul 10 2025 at 16:38):

Mike Shulman (Jul 10 2025 at 16:39):

I don't think they were wrong. I think our conclusion is more that some people (particularly in the Haskell community) have interpreted their results to say more than they actually do.

Ignat Insarov (Jul 10 2025 at 16:40):

Mike Shulman (Jul 10 2025 at 16:41):

Josselin Poiret (Jul 10 2025 at 19:47):

no, you're reading it right! when i say the reducibility predicate at the universe, I mean the predicate for terms of type the universe (i.e. each realized type decodes to a reducibility predicate for its terms).

Josselin Poiret (Jul 10 2025 at 19:48):

Josselin Poiret (Jul 10 2025 at 19:50):

so for a term t : U to be realized, you need Γ ⊩ t which refers to type realizability at the lower level, which is itself inductive

Mike Shulman (Jul 10 2025 at 22:02):

But then this is not actually an example of "two different ways to interpret the universe". The definition of _⊩¹U is the relevant one, and that's what gives the parametricity interpretation. I thought you were saying that _⊩¹U could also be defined inductively, and that's what I was asking for an example of.

Ryan Wisnesky (Jul 11 2025 at 05:11):

how does this sound for stack overflow? anything I should add or remove? "I am trying to find a proof (or dis-proof) that a Reynolds parametric model of system F is such that for every closed type c, the type c is bijective with the type forall x, (c->x)->x (known as the type of continuations for c). Hyland, Robinson, and Rosolini, in the conclusion of "Algebraic Types in PER Models" (https://www.dpmms.cam.ac.uk/~jmeh1/Research/Pub81-90/hrr90.pdf), give an example c for which this isomorphism fails: (forall x, x->x) -> (forall x, x->x) and conclude "parametricity fails in the system F term model". However, Bartosz Milewski gives a "free theorems" argument (which I've verified in Coq) that this isomorphism must hold (https://bartoszmilewski.com/2015/09/01/the-yoneda-lemma/). So myself and other applied category theorists would like community input to settle these two questions: in system F, does Reynolds parametricity imply every closed type is bijective with its type of continuations? And is the system F term model Reynolds parametric"?

John Baez (Jul 11 2025 at 05:30):

Maybe by "non-proof" you mean "disproof"? It's very easy to find non-proofs, i.e. strings of symbols that aren't proofs.

Josselin Poiret (Jul 11 2025 at 08:44):

How does the realizability of the universe give you the parametricity interpretation? It's rather what realizers of terms at type U that you can feed to polymorphic functions that matter, no?

Josselin Poiret (Jul 11 2025 at 09:06):

I don't remember if it's been said before, but wrt. the Q example of HRR, if you suppose that all inhabitants of

P = Π X, X → X

are already parametric, then in the model

Josselin Poiret (Jul 11 2025 at 09:07):

of course it's not a βη-equivalence, but extensionally, if you only probe them by definable functions, they are equal

Josselin Poiret (Jul 11 2025 at 09:08):

it's something quite similar to Escardó's seemingly impossible functional programs, which work only when you feed them definable predicates

Josselin Poiret (Jul 11 2025 at 09:13):

can you be more explicit about what exactly you've proven? just that web page isn't enough for me to infer it

Madeleine Birchfield (Jul 11 2025 at 12:20):

Do you have any references / papers that talk about dependent type theory with typecase?

Josselin Poiret (Jul 11 2025 at 14:01):

"The next 700 syntactical models of type theory" by Boulier et al. mentions typecase

Mike Shulman (Jul 11 2025 at 16:38):

Typeᵖ X Y = X → Y → Type
Πᴾ X Y f₀ f₁ = (x₀ x₁ : X) (x₂ : Xᵖ x₀ x₁) → Yᵖ (f₀ x₀) (f₁ x₁)

tells you that, for instance, the parametricity translation of (X : Type) → X → X is

((X : Type) → X → X)ᵖ F G =
  (X₀ X₁ : Type) (X₂ : X₀ → X₁ → Type) (x₀ : X₀) (x₁ : X₁) → X₂ (F x₀) (G x₁)

Therefore, for any (closed) F : (X : Type) → X → X, its translation Fᵖ tells you that F must preserve all relations, from which you get its free theorem.

Mike Shulman (Jul 11 2025 at 16:42):

Where Typeᵖ X Y = X → Y → Type is, I believe, what _⊩¹U says (maybe in the unary case).

Mike Shulman (Jul 11 2025 at 16:45):

Is there a precise definition of the phrase "Reynolds parametric model of system F"?

Mike Shulman (Jul 11 2025 at 16:53):

If so, maybe link to it. If not, maybe clarify that there isn't (yet) one, but that you mean some class of models including PER models that satisfy parametricity "internally" in some sense.

Mike Shulman (Jul 11 2025 at 16:56):

Also I think I wouldn't cite Milewski, since we know what's wrong with his argument. Instead I would say that HRR show that even for their own

Q

, the isomorphism does hold in their PER model. So the question is whether there are any "even worse" closed types for which the isomorphism even fails in internally parametric / PER models, or whether one can show that it works there for all closed types.

Ryan Wisnesky (Jul 11 2025 at 23:19):

remind me what went wrong with Milewski's argument? His argument had convinced me that c ~ CPS c for closed c in a parametric model (or at least a model with the 'free theorem' for the Reader and Id functors), from which I concluded the term model is not (fully) parametric. Am I mis-interpreting his argument or the Coq that formalized his argument?

Ryan Wisnesky (Jul 11 2025 at 23:21):

I think I'd use the Adadi-Plotkin paper to define Reynolds parametricity, but am open to suggestions

Mike Shulman (Jul 11 2025 at 23:39):

The isomorphism c ~ CPS c depends on knowing that all transformations

\forall x. (c\to x) \to x

are natural, which in turn requires c to be bridge-discrete to prove it from parametricity (even internal parametricity). IIRC the Coq formalization just assumed that all transformations

\forall x. (c\to x) \to x

are natural.

Mike Shulman (Jul 11 2025 at 23:48):

So the real question is whether "internal parametricity" of some kind for system F implies that all types are bridge-discrete.

Mike Shulman (Jul 11 2025 at 23:48):

Evan proved that all types in the first universe of internally parametric predicative dependent type theory are bridge-discrete, but that doesn't consider the impredicative

\forall

Ryan Wisnesky (Jul 12 2025 at 00:00):

both the coq code and the milewski post assume that any function of type "forall a, F a -> G a", where F and G are internal functors (in this case F=Reader and G=Id), is a natural transformation, this is true. In milewski's case I think he tries to establish this from the Yoneda lemma, and I just assumed it as a "free theorem" in the sense of wadler (and therefore implied by parametricity alone to my way of thinking). But both arguments seem to bypass bridge discreteness (although maybe they shouldn't), which is confusing me. (for sanity I'm going to stick to working in system F and interpreting milewski in system F). image is milewski's "axiom"
Screenshot 2025-07-11 at 5.09.10 PM.png

Mike Shulman (Jul 12 2025 at 00:10):

He states it using forall but that's because he's previously asserted that all transformations are natural.

Mike Shulman (Jul 12 2025 at 00:11):

Mike Shulman (Jul 12 2025 at 00:12):

Mike Shulman (Jul 12 2025 at 00:13):

But I think we worked out before that this just isn't true. There is a free theorem for the type

\forall x. (F x \to G x)

, for any functors

F

and

G

, but it isn't by definition naturality, and to extract naturality from it you need the identity extension lemma for

F

and

G

Mike Shulman (Jul 12 2025 at 00:14):

And the identity extension lemma for

R_a(x) = (a\to x)

requires

a

to be bridge-discrete.

Ryan Wisnesky (Jul 12 2025 at 00:17):

ok. I think that is a good summary of the failure of folklore: naturality does not follow from parametricity in general , so "theorems for free" is not the same as "Reynolds parametricity". Indeed, Wadler might even be conflating these concepts in his "free theorems" paper !?

Ryan Wisnesky (Jul 12 2025 at 00:23):

anyway, I think the blog post will probably need to give the free theorem and show how it isn't the same as naturality, and walk through how bridge discreteness implies identity extension implies naturality, but i think I'm unblocked on writing even without the stack overflow post now: naturality simply does not follow from parametricity. Which is actually a bit surprising because I've seen it claimed at a high level that parametricity generalizes naturality from functions to relations

Ryan Wisnesky (Jul 12 2025 at 01:25):

the plotkin abadi identity extension lemma refers to all types, not just bridge discrete ones (but has no proof). does this mean their logic is actually capturing a notion of parametricity that might always imply naturality? (side note: I saw a remark that identity extension is what separates a parametric model from one that is simply defined using a logical relation, and wonder if that distinction has been showing up here: a parametric model is one where identity extension holds for all types, whereas a logical relation defined model only has that property for bridge discrete types, or something along those lines). Image is of remark from https://par.nsf.gov/servlets/purl/10338496
Screenshot 2025-07-11 at 6.26.58 PM.png

Mike Shulman (Jul 12 2025 at 02:01):

Mike Shulman (Jul 12 2025 at 02:02):

I think I would just call them different forms of parametricity, though. "Internal parametricity" is pretty well-established as a name for a class of dependent type theories, and we decided that those don't satisfy universal identity extension or bridge-discreteness.

Mike Shulman (Jul 12 2025 at 02:03):

Maybe this is "strong parametricity" or "impredicative parametricity" or something.

Ryan Wisnesky (Jul 12 2025 at 05:36):

ok, great; then to conclude, in that case I'd say the HRR conclusion comment is noticing that the term model fails to be "strong parametric", even though it does satisfy weaker forms of parametricity (such as polymorphic identity having one inhabitant), giving q ~ cont q as the witness, and this thread quantifies the difference between the two situations using the "bridge discreteness" of a type

Mike Shulman (Jul 12 2025 at 08:07):

That sounds good, but I'm not ready to conclude until I see a proof of the identity extension lemma.

Ryan Wisnesky (Jul 12 2025 at 08:26):

a proof of the identity extension lemma for which models/logics are you referring to?

Mike Shulman (Jul 12 2025 at 08:33):

At https://cs.stackexchange.com/a/136373/185120 András Kovács claimed that "For System F, identity extension can be proven for types-in-contexts", but wasn't able to produce a reference when I asked.

Ryan Wisnesky (Jul 12 2025 at 08:38):

the plot thickens; identity extension for system F would in my mind contradict HRR's claim that q is not iso to cont q in the term model. my current thinking is no such proof should exist

Ryan Wisnesky (Jul 12 2025 at 08:58):

Mike Shulman (Jul 12 2025 at 15:49):

Could it be a definitional vs contextual thing? E.g. maybe the form of IEL that holds only shows that every element of CPS q behaves like an element of q when applied to all possible closed term inputs, and the exotic HRR term does that?

Ryan Wisnesky (Jul 12 2025 at 19:19):

I think Josselin made a similar remark yesterday? I suppose I'll write to Neel K as a next step.

Mike Shulman (Jul 12 2025 at 20:58):

Ryan Wisnesky (Jul 13 2025 at 23:40):

Here's what Neel said: "There is no incompatibility between the parametricity of the syntactic model and Hyland's note. Hyland considers the naive PER model, in which every type is interpreted solely as a partial equivalence relation (PER) which is well-known to be weak to prove parametricity results. To prove parametricity results, you need a relationally parametric model, in which every type is interpreted both as a PER, and a relation between PERs.
The place where the parametric model over PERs is documented is in Bainbridge, Freyd, Scedrov and Scott's paper "Functorial Polymorphism". The first half of their paper is a (failed) attempt to interpret parametricity as dinaturality, after which they go ahead and build a syntactic parametric PER model, where types are PERs/relations over Godel codes. Among other results, they prove that their relational model satisfies the identity extension property.
Their proof only relies on the Godel codes forming a partial combinatory algebra, and so you can plug in any PCA -- and lambda terms obviously form one. Recall that a PCA is basically an axiomatization of the algebra of the SKI combinators, and so you can make the lambda calculus into a PCA with the usual definitions S = λf.λg.λx.f x (g x) and K = λx.λy.x.
Once you do this, then it's immediate that the parametric term model satisfies identity extension."

Mike Shulman (Jul 14 2025 at 00:34):

Interesting. So he seems to be saying that in order to get IEL, you can't actually look at the term model in the usual sense, but you have to use a model in relations that builds in some strong parametricity. That makes sense with my intuition.

Mike Shulman (Jul 14 2025 at 00:35):

Did you ask him specifically about Kovács' claim that "For System F, identity extension can be proven for types-in-contexts"? That sounds like it's a statement about the ordinary term model rather than a relation model constructed from it.

Ryan Wisnesky (Jul 14 2025 at 00:40):

yeah, I was not expecting him to start talking about a model using untyped lambda terms in reference to the term model. Here's what I asked: "Myself and some other type theorists / category theorists were hoping you might be able to help settle an apparent open folklore question concerning system F. We’re writing specifically because of your illuminating blog post at https://semantic-domain.blogspot.com/2020/12/church-encodings-are-inductive-types.html .
The conclusion of ‘Algebraic types and PER models' by Hyland et al (https://www.dpmms.cam.ac.uk/~jmeh1/Research/Pub81-90/hrr90.pdf) exhibits a failure of “parametricity” in the system F term model by constructing a closed type c for which c is not bijective with forall x, (c -> x) -> x (the type of continuations for c) in the term model.
At the same time, it seems to be folklore that the system F term model is parametric, with for example Andy Kovacs stating that identity extension should hold in the term model (https://cs.stackexchange.com/questions/136359/rigorous-proof-that-parametric-polymorphism-implies-naturality-using-parametrici/136373#136373). There are many other such claims in the literature, yet Mike Schulman and I can’t find any proofs. In fact, I’m starting to believe the term model does not satisfy identity extension, which would explain Hyland et al’s claim (I think).
So, do you know of a proof or dis-proof that the system F term model satisfies identity extension (however suitably formulated for the term model)?"

Mike Shulman (Jul 14 2025 at 00:46):

Ok, he does seem to be saying that the term model doesn't satisfy identity extension, but it's not completely clear. Maybe you could ask for a clarification, emphasizing that by "term model" you mean the initial model build directly from the syntax of system F?

Ryan Wisnesky (Jul 14 2025 at 14:58):

I asked neel the follow-up: "it seems like here by term model you are talking about a model of system F built from untyped lambda terms, passing through their PCA. But what Mike and I meant by the term model of system F was the initial model built directly from the syntax of system F. I’m not even sure how to state identity extension for the term model in the Mike/Ryan sense, but I’m wondering if you can comment on identity extension in the typed term model of system F, rather than the untyped PCA model. Thanks again!" and he replied with a detailed answer, but again not what I was expecting. My understanding of his response is that the untyped PER model somehow "is also" the term model.
Screenshot 2025-07-14 at 7.53.38 AM.png

Mike Shulman (Jul 14 2025 at 15:21):

That does seem to be what he's implying, but that's clearly false because the (initial) term model is not defined mutually recursively with any relational interpretation. Why don't you add me to the email thread and we can all continue there instead of playing telephone? (-:

Ryan Wisnesky (Jul 14 2025 at 15:27):

Will do, although here's a final thought before doing so: to obtain a set-theoretic model of system F terms, the machinery of logical relations might already be required, for example, to inductively define terms that strongly normalize. So maybe there is a sense in which the system F term model does have to be constructed alongside its relational interpretation.

Mike Shulman (Jul 14 2025 at 16:43):

Every type theory has an initial model built out of syntax. It's not a "set-theoretic" model in the sense of interpreting each type as a set, but it always exists.

Mike Shulman (Jul 14 2025 at 16:44):

Notification Bot (Jul 14 2025 at 20:37):

Josselin Poiret (Jul 15 2025 at 09:54):

What I'm saying is precisely that it does not, that would be the negative interpretation of the universe

Josselin Poiret (Jul 15 2025 at 09:58):

you have two choices, either _⊩¹U consists of metatheoretical relations with some conditions on them that makes them behave as realizability relations, or it is just a universe of codes that then decode to the expected relations. The difference between the two is that the former contain undefinable relations while the second, by construction, only contains definable relations

Mike Shulman (Jul 15 2025 at 15:26):

I guess I just can't make heads or tails of that Agda. Can you write out the definition of _⊩¹U in words? I agree it doesn't look like the negative interpretation, but it doesn't look like a positive inductive definition either.

Ryan Wisnesky (Jul 15 2025 at 23:54):

I'm revisiting an example from tannen coquand. consider the type T := (forall x, x) -> (forall x, x) -> (forall x, x). Then there are two distinct terms in this type T, essentially, "project first component" and "project second component". But in an extensional model where forall x, x is empty, this type T should have only one inhabitant. In tannen coquand they conclude the term model is not extensional. So my question: could the HRR result be similarly (better?) understood as a failure of extensionality than parametricity in the term model?

Mike Shulman (Jul 15 2025 at 23:58):

Ryan Wisnesky (Jul 16 2025 at 00:04):

I've attached tannen coquand's definition, which I understand to be a semantic criteria similar to (forall x, f x = g x) -> f = g for both function types and forall types.
Screenshot 2025-07-15 at 5.02.05 PM.png

Mike Shulman (Jul 16 2025 at 00:13):

Ok, they mean equality of functions is detected by applying them to global elements. I would call that being well-pointed.

Mike Shulman (Jul 16 2025 at 00:13):

Mike Shulman (Jul 16 2025 at 00:14):

Well, can you show that the exotic term would be equal to some standard one in any well-pointed model?

Ryan Wisnesky (Jul 16 2025 at 00:22):

the HRR argument for PER models seems to apply to well pointed ones also, but I figured someone here might already know or have a proof

Mike Shulman (Jul 16 2025 at 17:20):

I want to record in this thread something that I didn't realize explicitly at first, namely that strong parametricity (= external parametricity plus identity extension) implies internal parametricity.

\frac{\vdash A\,\mathsf{type}}{x_0 : A, x_1: A \vdash A^p(x_0,x_1) \,\mathsf{type}}\qquad \frac{\vdash a:A}{\vdash a^p : A^p(a,a)}

but to define these recursively on syntax we have to extend them to open terms by also "degenerating the context", e.g.

\frac{x:A \vdash B(x)\,\mathsf{type}}{x_0:A, x_1:A, x_2:A^p(x_0,x_1), y_0:B(x_0), y_1 : B(x_1) \vdash B^p(x_2,y_0,y_1) \,\mathsf{type}}\\[1em] \frac{x:A \vdash b(x):B(x)}{x_0:A, x_1:A, x_2:A^p(x_0,x_1) \vdash b^p(x_2) : B^p(x_2,b(x_0),b(x_1))}

External parametricity satisfies identity extension if

A^p(x_0,x_1) = \mathsf{Id}_A(x_0,x_1)

, and similarly in the dependent case.

By internal parametricity I mean operations on possibly-open terms that don't degenerate the context, such as

\frac{x:A \vdash B(x)\,\mathsf{type}}{x:A, y_0:B(x), y_1:B(x) \vdash B^p(x,y_0,y_1)\,\mathsf{type}}\\[1em] \frac{x:A \vdash b(x):B(x)}{x:A \vdash b^p(x) : B^p(x,b(x),b(x))}

Now if you already have external parametricity, to get internal parametricity it suffices to add these operations on variables, since then you can obtain (for instance) the internal

b^p(x)

as the external

b^p(x,x,x^p)

. (This is how "observational" parametricity, as in Narya, computes with its internal parametricity operator.)

But identity extension also suffices, since you can also use

\mathsf{refl}_x

instead of

x^p

Madeleine Birchfield (Jul 16 2025 at 23:18):

Mike Shulman (Jul 17 2025 at 01:49):

Josselin Poiret (Jul 17 2025 at 09:42):

So the main definition in there is _⊩¹_, which defines the realizability predicate for types (what Jon calls

\mathrm{tp}_{α}^{⨳}

Note that the ¹ is slightly misleading here, it should be understood as ⁺¹ instead, as it builds the predicate for types at level higher than the given rec in the module telescope. So when l = 0 and rec equals λ (), it actually builds the realizability predicate for small types.

Note that this information does not contain an arbitrary realizability relation for terms at that type, it's entirely decoded from the above. This is in contrast with semantic approaches I know of in the literature, where you additionally ask for a relation on terms that reflects neutrals and reifies to normals, and you use that relation when realizing inhabitants of this semantic type.

Josselin Poiret (Jul 17 2025 at 09:43):

_⊩¹_, the positive interpretation, is thus a subtype of the negative version in the literature. One advantage is that the realizability relation is entirely determined by the syntax.

Stream: learning: questions

Topic: Continuations, parametricity, and polymorphism

Ryan Wisnesky (Jul 03 2025 at 18:46):

Mike Shulman (Jul 03 2025 at 19:01):

Ryan Wisnesky (Jul 03 2025 at 19:50):

Mike Shulman (Jul 03 2025 at 20:04):

Mike Shulman (Jul 03 2025 at 20:08):

Mike Shulman (Jul 03 2025 at 20:10):

Ryan Wisnesky (Jul 03 2025 at 20:11):

Mike Shulman (Jul 03 2025 at 20:14):

Ryan Wisnesky (Jul 03 2025 at 20:14):

Mike Shulman (Jul 03 2025 at 20:14):

Mike Shulman (Jul 03 2025 at 20:15):

Mike Shulman (Jul 03 2025 at 20:15):

Ryan Wisnesky (Jul 03 2025 at 20:22):

Ryan Wisnesky (Jul 03 2025 at 20:31):

Mike Shulman (Jul 03 2025 at 20:36):

Mike Shulman (Jul 03 2025 at 20:38):

Mike Shulman (Jul 03 2025 at 20:40):

Mike Shulman (Jul 03 2025 at 20:40):

Ryan Wisnesky (Jul 03 2025 at 20:49):

Ryan Wisnesky (Jul 03 2025 at 20:51):

Ryan Wisnesky (Jul 03 2025 at 20:55):

Mike Shulman (Jul 03 2025 at 20:59):

Ryan Wisnesky (Jul 03 2025 at 20:59):

Mike Shulman (Jul 03 2025 at 21:00):

Ryan Wisnesky (Jul 03 2025 at 21:01):

Mike Shulman (Jul 03 2025 at 21:01):

Ryan Wisnesky (Jul 03 2025 at 21:03):

Ryan Wisnesky (Jul 03 2025 at 21:04):

Mike Shulman (Jul 03 2025 at 22:56):

Ryan Wisnesky (Jul 03 2025 at 22:56):

Mike Shulman (Jul 03 2025 at 22:57):

Ryan Wisnesky (Jul 03 2025 at 22:57):

Mike Shulman (Jul 03 2025 at 22:58):

Mike Shulman (Jul 03 2025 at 22:59):

Mike Shulman (Jul 03 2025 at 23:00):

Mike Shulman (Jul 03 2025 at 23:01):

Ryan Wisnesky (Jul 03 2025 at 23:02):

Mike Shulman (Jul 03 2025 at 23:02):

Mike Shulman (Jul 03 2025 at 23:04):

Mike Shulman (Jul 03 2025 at 23:06):

Mike Shulman (Jul 03 2025 at 23:08):

Mike Shulman (Jul 03 2025 at 23:08):

Mike Shulman (Jul 03 2025 at 23:09):

Ryan Wisnesky (Jul 03 2025 at 23:11):

Mike Shulman (Jul 03 2025 at 23:12):

Ryan Wisnesky (Jul 03 2025 at 23:13):

Mike Shulman (Jul 03 2025 at 23:13):

Mike Shulman (Jul 03 2025 at 23:14):

Ryan Wisnesky (Jul 03 2025 at 23:14):

Mike Shulman (Jul 03 2025 at 23:15):

Mike Shulman (Jul 03 2025 at 23:15):

Ryan Wisnesky (Jul 03 2025 at 23:15):

Mike Shulman (Jul 03 2025 at 23:16):

Mike Shulman (Jul 03 2025 at 23:16):

Ryan Wisnesky (Jul 03 2025 at 23:18):

Mike Shulman (Jul 03 2025 at 23:18):

Ryan Wisnesky (Jul 03 2025 at 23:21):

Mike Shulman (Jul 03 2025 at 23:24):

Mike Shulman (Jul 03 2025 at 23:25):

Ryan Wisnesky (Jul 03 2025 at 23:26):

Mike Shulman (Jul 03 2025 at 23:30):

Mike Shulman (Jul 03 2025 at 23:30):

Ryan Wisnesky (Jul 03 2025 at 23:32):

Ryan Wisnesky (Jul 03 2025 at 23:33):

Mike Shulman (Jul 03 2025 at 23:34):

Mike Shulman (Jul 03 2025 at 23:35):

Ryan Wisnesky (Jul 03 2025 at 23:37):

Mike Shulman (Jul 03 2025 at 23:38):

Ryan Wisnesky (Jul 03 2025 at 23:39):

Mike Shulman (Jul 03 2025 at 23:41):

Ryan Wisnesky (Jul 03 2025 at 23:41):

Mike Shulman (Jul 03 2025 at 23:41):

Ryan Wisnesky (Jul 03 2025 at 23:42):

Mike Shulman (Jul 03 2025 at 23:43):

Ryan Wisnesky (Jul 03 2025 at 23:43):

Ryan Wisnesky (Jul 03 2025 at 23:44):

Mike Shulman (Jul 03 2025 at 23:46):

Ryan Wisnesky (Jul 03 2025 at 23:47):