Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics comma complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration finite foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthoratmacen
    • CommentTimeApr 3rd 2020

    Fake edit to associate a discussion thread.

    diff, v11, current

    • CommentRowNumber2.
    • CommentAuthoratmacen
    • CommentTimeApr 3rd 2020

    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:

    1. Meaning is assigned to judgments (intrinsic) or terms (extrinsic)
    2. Types are syntactic parts of speech (intrinsic) or semantic predicates (extrinsic)
    3. All expressions carry a type (intrinsic) or not (extrinsic)

    I would say these are:

    1. Polymorphic or monomorphic semantics
    2. Syntactic or semantic typing
    3. Unique typing or not

    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?

    • CommentRowNumber3.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 3rd 2020

    Just to note: we needed to set up this thread, but there was earlier discussion at Extrinsic/intrinsic Curry/Church distinctions.

    • CommentRowNumber4.
    • CommentAuthoratmacen
    • CommentTimeApr 3rd 2020

    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.

    • CommentRowNumber5.
    • CommentAuthorMike Shulman
    • CommentTimeApr 4th 2020

    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.

    • CommentRowNumber6.
    • CommentAuthoratmacen
    • CommentTimeApr 4th 2020

    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.

    • CommentRowNumber7.
    • CommentAuthorMike Shulman
    • CommentTimeApr 5th 2020

    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).

    • CommentRowNumber8.
    • CommentAuthoratmacen
    • CommentTimeApr 5th 2020

    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.