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.
We don’t have anything on this, I think, but there is mention of “intrinsic” and “à la Church” at coercion. From Type refinement and monoidal closed bifibrations:
One of the difficulties in giving a clear mathematical definition of the “topic” of type theory is that the word “type” is actually used with two very different intuitive meanings and technical purposes in mind:
- Like the syntactician’s parts of speech, as a way of defining the grammar of well-formed expressions.
- Like the semanticist’s predicates, as a way of identifying subsets of expressions with certain desirable properties.
These two different views of types are often associated respectively with Alonzo Church and Haskell Curry (hence “types à la Church” and “types à la Curry”), while the late John Reynolds referred to these as the intrinsic and the extrinsic interpretations of types [11]. In the intrinsic view, all expressions carry a type, and there is no need (or even sense) to consider the meaning of “untyped” expressions; while in the extrinsic view, every expression carries an independent meaning, and typing judgments serve to assert some property of that meaning.
[11] is John C. Reynolds. The Meaning of Types: from Intrinsic to Extrinsic Semantics. BRICS Report RS-00-32, Aarhus University, December 2000. pdf
There are two very different ways of giving denotational semantics to a programming language (or other formal language) with a nontrivial type system. In an intrinsic semantics, only phrases that satisfy typing judgements have meanings. Indeed, meanings are assigned to the typing judgements, rather than to the phrases themselves, so that a phrase that satisfies several judgements will have several meanings.
In contrast, in an extrinsic semantics, the meaning of each phrase is the same as it would be in a untyped language, regardless of its typing properties. In this view, a typing judgement is an assertion that the meaning of a phrase possesses some property.
The terms “intrinsic” and “extrinsic” are recent coinages by the author [1, Chapter 15], but the concepts are much older. The intrinsic view is associated with Alonzo Church, and has been called “ontological” by Leivant [2]. The extrinsic view is associated with Haskell Curry, and has been called “semantical” by Leivant.
[1] John C. Reynolds. Theories of Programming Languages. Cambridge University Press, Cambridge, England, 1998. [2] Daniel Leivant. Typing and computational properties of lambda expressions. Theoretical Computer Science, 44(1):51–68, 1986.
Anyone have a preferred name for this distinction?
Intrinsic/extrinsic isn’t bad.
Ok, so I’ve started something at intrinsic and extrinsic views of typing.
And I started type refinement.
In the (nonextended version of) A Fibrational Framework for Substructural and Modal Logics, there’s mention of Melliès and Zeilberger’s work:
Bifibrations have also been used recently to model refinement types and logical relations…Superficially, this seems to be a different use of the same semantic structure, because the base and domain categories of the bifibration play a different role…It would be interesting to investigate deeper connections and combine the two notions.
Noam was speaking on this work at Kent yesterday, and it was very good to meet him. It does surely seem that the common use of bifibrations is salient.
Yes, these two projects are much more closely related than I realized at first. When we last discussed their “Bifibrational reconstruction” paper, I was still thinking only of fibrations in an “indexing” sense, with cartesian lifts being “fundamental” and opcartesian lifts being “indexed coproducts”. But in LSR we’re using bifibrations in a very similar way as they are, with cartesian and opcartesian lifts being treated very dually, corresponding roughly to negative and positive type formers (“U-types” and “F-types” in adjoint-logic parlance). I think that their monoidal bifibrations are very close to the semantics of the still-nascent LSR 3-theory of “classical simple type theory” – like the extant LSR paper for “intuitionistic simple type theory” but allowing multiple consequents as well. (To be precise, right now I think that the most general thing we want is a monoidal bifibration over a compact closed cartesian bicategory.)
I don’t really know exactly what a “refinement type” is, but intuitively it seems to me that LSR can be thought of as a sort of “refinement typing”, and I think Dan has even used that word in referring to it. That is, the type theory “upstairs” is really just ordinary “cartesian” type theory, but “refined” by associating modal information to everything that controls what sort of derivations are permissible.
Intriguing. It would be good to resume the discussion with Noam.
I don’t really know exactly what a “refinement type” is…
There’s certainly more to say at type refinement. Should we extract ideas from this cs.stackexchange answer?
One motivation for the extrinsic point of view seems to be that it makes better sense of subtypes. So if I say things about a red apple, I may mean that they apply to the apple itself. In ’This red apple is tasty’, the ’tasty’ is a predicate applied to apples or foodstuffs, rather than to red apples.
So what’s the difference between a subtype, a dependent sum of a dependent type that is necessarily a proposition for each element of the base type, and a dependent type that happens to be a subsingleton for each element of the base?
Perhaps as an example of the three: Married man; Man and warrant of his marriage; and, Man and his spouse. (Assuming we’re in a monogamous society.)
Presumably the extrinsic type theorist is prepared to distinguish the first from the second, since in ’The married man is tall’ the height only applies to the man, not his marital status. As for the third, we’d certainly have to signal the projection to speak just of the man.
The man and his spouse are tall.
I guess if it’s just a question of a bifibration $\mathcal{D} \to \mathcal{M}$, you can have the extremes, $\mathcal{M} = \mathbf{1}$ and $\mathcal{D} = \mathcal{M}$, and then you’re not going to speak of refinement. If $\mathcal{M}$ just has as objects $t$ and $v$ as in Pfenning-Davies, the ’refining’ seems mostly about adding to the $t$ fibre, whereas if $\mathcal{M}$ concerns all sets and $\mathcal{D}$ predicates on those sets, it’s easier to see $\mathcal{M}$ as being refined.
Hi David and Mike,
Maybe I can say a couple of things.
I agree that there is a close connection between the two projects (our work on type refinement systems and the LSR approach). It might help to know that the idea of building a fine-grained, “fibrational proof theory” (where the base category encodes the allowable operations on the context) was actually one of our original motivations when we started out, and the connection to refinement typing only came later. We talked a little bit about these proof-theoretical motivations in the “Isbell duality” paper, in particular the idea of interpreting logical formulas as fibered over context types, and inference rules as fibered over context operations. (For example, the ${\otimes}R$ rule of linear logic is fibered over the operation of context concatenation.) So what we call “context types” (which are “refined” by formulas in substructural logics) are very analogous to what LSR call “modes”.
A reason the analogy to refinement typing was originally very useful to me was that it made clear the importance of “working in the total category” over “working in the fibers”. Under the interpretation of a functor as a type refinement system, vertical morphisms correspond to subtyping derivations, which are just the special case of typing the identity. In some situations (namely for a fibration/opfibration), it is possible to reduce typing to subtyping, but somehow this is less natural from a type-theoretic perspective. Another useful example from computer science is Hoare logic, which can be modelled as a type refinement system over a one-object category of “commands”. In some cases it is possible to reduce reasoning in Hoare logic to reasoning in ordinary predicate logic by computing weakest preconditions (= pullbacks/right-cartesian liftings) or strongest postconditions (= pushforwards/left-cartesian liftings), but these may not always exist depending on the language of predicates and commands.
And from a formal perspective, alluding to what Mike said, one of the things that working with a type refinement system as a functor rather than as a fibration lets you do is treat left-cartesian and right-cartesian morphisms on equal footing. An example of this is the very useful fact that in an adjunction of refinement systems, the left adjoint preserves left-cartesian morphisms and the right adjoint preserve right-cartesian morphisms.
David wrote:
I guess if it’s just a question of a bifibration $\mathcal{D}\to\mathcal{M}$, you can have the extremes, $\mathcal{M}=1$ and $\mathcal{D}=\mathcal{M}$, and then you’re not going to speak of refinement.
But you can! These are actually examples that we use in the “Isbell duality” paper. The idea is that a category can be seen as a degenerate kind of “refinement system” in two different canonical ways, and this is actually useful sometimes for thinking of refinement systems as generalizations of categories (in the same sense as displayed categories).
I understand that the terminology of type refinement may not be helpful for everyone. I like the slide from Paul-André’s recent talk at Bonn where he said that a functor $p : \mathcal{E} \to \mathcal{B}$ can be seen in two complementary ways: either as a category $\mathcal{E}$ with “infrastructure” $\mathcal{B}$, or as a category $\mathcal{B}$ with “superstructure” $\mathcal{E}$. In either case, we refer to the objects in $\mathcal{E}$ as “refinements” of the objects in $\mathcal{B}$, although in the first case it may be more natural to think of the objects in $\mathcal{B}$ as “shadows” of the objects in $\mathcal{E}$.
re David #8:
One motivation for the extrinsic point of view seems to be that it makes better sense of subtypes. So if I say things about a red apple, I may mean that they apply to the apple itself. In ’This red apple is tasty’, the ’tasty’ is a predicate applied to apples or foodstuffs, rather than to red apples.
Yes, to me that sounds very analogous to the motivation for the original (non-categorical) work on type refinement, which was to have types capturing more precise properties of programs but without changing the semantics of those programs. In pure dependent type theory the possibility of taking such an interpretation is not always clear, because as we modify the type of a program expression to make it more precise, we also have to modify the code of that expression. (On the other hand, dependent type theory is expressive enough that working within a fragment, you can try to maintain the invariant that programs with more precise types are erasable to programs with simpler types: for example, that’s the motivation for Conor McBride’s work on “ornaments”.)
I understand that the terminology of type refinement may not be helpful for everyone.
It’s probably the usual sort of situation: saying that A is like B can only help people understand B if they already understand A. For me, the analogy is probably more likely to be helpful in understanding what “type refinement” means than the other way around.
Noam, re #10, do you know whether the slides of Paul-André’s talk at Bonn will be made available?
Do any interesting lifting problems arise against such refinement bifibrations, $p : \mathcal{E} \to \mathcal{B}$?
Noam, re #10, do you know whether the slides of Paul-André’s talk at Bonn will be made available?
I don’t know, but will try asking…
Do any interesting lifting problems arise against such refinement bifibrations, $p : \mathcal{E} \to \mathcal{B}$?
Indeed. You can ask about the lifting of a monad or endofunctor on $\mathcal{B}$ to a monad or endofunctor on $\mathcal{E}$, and there are some interesting general constructions, see for example this paper by Shin-ya Katsumata, and this paper by Atkey, Johann, and Ghani.
Returning to this conversation, the video of Paul-André’s talk is available, but unfortunately in a way that’s difficult to see what he’s writing on the blackboard.
I was thinking, John Baez used to make a great deal about the analogy between hom sets and inner products, e.g., in Higher-Dimensional Algebra II: 2-Hilbert Spaces, explaining the similarity between adjoint operators and adjoint functors. With this bifibration set-up above of a total 2-category over a 2-category of modes, it seems like we’re seeing something similar to parallel transport of vectors. So a path (or arrow) in the 2-category of modes $f:A \to B$ allows transport of elements in the fibres in both directions, $F_f$ sending the fibre over $A$ to that over $B$, and $U_f$ doing the opposite. Then $(F_f X, Y)_B \equiv (X, U_f Y)_A$ indicates the preservation of the ’inner product’.
By the way, Mike, can we expect any time soon the next instalment of the LSR project? Is that to be on dependent type (2-)theories, or perhaps the ’classical simple type theory’ in #6?
I think the next installment will be on dependent type theories. We’re working on it, but the details are fiddly, and none of us have a lot of time right now, so I don’t have an ETA yet.
1 to 16 of 16