Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
So I have a vague thought/complaint, which is that I’ve been describing Nuprl-style systems as “extrinsic”, but from the quotes on this page, I’m confused. That may be all my fault: I might’ve been using “intrinsic” and “extrinsic” wrong. But already in the quotes of Reynolds, and of Melliès and Zeilberger, it seems like there are actually three different distinctions branded as the intrinsic/extrinsic distinction:
I would say these are:
Also note that if a term has a unique type, it presumably has at most one meaning, even with polymorphic semantics.
Maybe I’m just being too fussy. I sure thought Nuprl was extrinsic, and (2) and (3) seem to support that, but (1) does not. That is, Nuprl has polymorphic, semantic typing, and the polymorphism is nontrivial since a term typically has multiple types.
Maybe I’m misinterpreting (1) by thinking of the wrong notion of meaning? Certainly every Nuprl term has operational semantics independently of typing judgments. Is that all that counts?
I think this subtlety of what the intrinsic/extrinsic distinction is really about might have to do with the unfortunate situation that the “Functors are Type Refinement Systems” approach doesn’t seem to cover Nuprl-style type systems. The immediate problem is that Nuprl-style refinement (subquotient) generally forgets meaningless distinctions (implementation details), and so the functor would not respect equality of morphisms. But why didn’t Melliès and Zeilberger address that? Maybe I’m not supposed to think about Nuprl in terms of refinement/extrinsic typing? Similar systems have traditionally been called “polymorphic”.
Thoughts, anyone?
Just to note: we needed to set up this thread, but there was earlier discussion at Extrinsic/intrinsic Curry/Church distinctions.
Thanks for that link.
I asked:
the “Functors are Type Refinement Systems” approach doesn’t seem to cover Nuprl-style type systems … the functor would not respect equality of morphisms. But why didn’t Melliès and Zeilberger address that?
From this old comment, it looks like the reason might just be that type refinement wasn’t the original motivation of their functors.
It’s hard for me to imagine an monomorphic categorical semantics, since categories are fairly relentlessly typed. So I expect the intended meaning of (1) is operational.
That makes sense. On the other hand, the categorical semanticists I’ve seen seem to prefer unique typing, so that they can pretend they’re still interpreting terms. What if there’s not unique typing; are they really OK with polymorphism? The versions of MLTT with unique typing have also been called “monomorphic”, so I associated category theory with a lack of polymorphism, and so your comment surprised me.
Anyway, another possibility for interpreting untyped terms is domain theory. But I suppose it wouldn’t make a difference, if you’re doing it right.
So I suppose the thing that makes Nuprl feel extrinsic is how it internalizes reasoning about its monomorphic operational semantics, in addition to its polymorphic type semantics.
To be clear, I have no idea why you chose the words “polymorphic” and “monomorphic” here, I was just copying you. In general, to interpret a term in a category you have to know its type, so you are interpreting judgments rather than terms. But that has nothing to do, in my mind, with whether that term could also have another type, which I would still regard as somewhat bizarre (if we’re talking about fully elaborated terms).
If terms have unique types, and you only interpret well-typed terms, then there exists a unique type, so it doesn’t matter whether you interpret the term or the typing judgment. Of course, the context needs to be taken into account, but you know about that. (The quotes didn’t say anything about interpreting derivations, which is good, since it’s a technicality, but I’m wondering if there’s an ambiguity here.)
This is related to my confusion about the quotes: if a system is intrinsic in the sense of unique typing, then it doesn’t matter whether it’s intrinsic in the sense of interpreting judgments. So I wonder if Reynolds was assuming a system without unique typing, and comparing the (consequently different) ways of interpreting. But Melliès and Zeilberger seem to be talking about different styles of system, not different styles of interpretation.
1 to 8 of 8