[Prev][Next][Index][Thread]
A proposed contribution in the types forum
Date: 3 Mar 1989 1338-PST (Friday)
To: meyer@theory.LCS.MIT.EDU
Dear Albert, I'd like to propose the following message to the types
mailing list (J. Meseguer has seen this, and thinks it would be nice
for types). Best wishes from California, where I spend half of the
year at SRC, until july.
Universe models of J. Meseger versus diktoses of T. Ehrhard
I would like to point out a striking similarity (actually inclusion:
diktoses are universe models) between the notions
quoted in the title of this communication. Let me present shortly
these notions, starting with that of J. Meseguer, which is nicely
motivated by syntax related ideas. Let us just mention that universe
models are primarily intended to give meaning to polymorphic
lambda-calculus, while diktoses were designed to give a semantics
to the theory of constructions.
Let me mention also, for interested readers, that the references are
J. Meseguer "Relating Models of Polymorphism" Proc. ACM
POPL'89 Symp., 228-241, 1989.
T. Ehrhard, "A categorical semantics of constructions", Proc. LICS
88, Edinburgh.
J. Meseguer has a nice way of describing a semantic framework
for F (second order Lambda-calculus in Girard's terminology), starting
>from the paradigm of translating polymorphism into dependency
(used, as far as I know, in Edinburgh's LF)
So the story begins with this translation. One introduces in the
calculus of pure first-order dependency (lambdaPI in the terminology
of Meyer-Reinhold) two kinds (french people call them types...): U,
and T which depends on U, say x:U |- T[x] type.
Then the types (french people call them propositions...)
of F translate into terms of type U (one needs two
constants =>:UxU->U and PI:(U->U)->U). The terms M:a translate into
terms of type T[a].
For this translation to be well typed one needs
two equations:
T[=>(a,b)] = T[a]->T[b]
T[PI(\a)] = PI_{Fst}(T[a])
In the last equation, one has, say a: CxU->U, \a:C->(U->U), Fst:CxU->C.
Now take your favorite semantic framework for first order dependent
types, and plug in that additional small theory about U,T,=>,PI and the
two equations, and say that a model of the theory is a model of F.
Specializing to (relatively) locally cartesian closed
categories (LCCC's), this gives Meseguer's universe
models.
T. Ehrhard, in his thesis, the main results of which appeared in the
quoted LICS 88 proceedings, proposed a categorical framework for type dependency,
looser than (relatively) LCCC's, on the top of which he placed
a simple "kit" to interpret Coquand-Huet's theory of constructions.
The very same kind of "kit" appears also in the thesis of T. Streicher
(Univ. of Passau, 1988), where it is grafted on Cartmell's contextual
categories.
This "kit" is "detachable", and can be reimported into the probably
more familiar world of (relatively) LCCCs: and
this is what Ehrhard calls a diktos (actually he has one more condition,
reflection, which is not needed for the purpose of this discussion).
I recall the definition, which
I try to give in a notation compatible with Meseguer's framework, and
I specialize to LCCC'S rather than relatively LCCC'S.
It may be worthwhile to recall that locally cartesian closed categories
are categories with a terminal object s.t. all the slice categories
are CCCS, where the slice category C/A of a categoy C has arrows f:B->A
as objects, and arrows h:f->g as arrows where h;g=f.
Notation: FA will be "for all" and PI will be dependent product,
which in LCCC's is the right adjoint to pullback functor ; pullbacks
are denoted as follows: the result of pulling back g:B->A along f is written
g[f] (substitution!) or even B[f]. I use LATEX conventions for sub and supersripts.
Definition: A diktos is a LCCC with a special arrow T->U, s.t. for any
a:A->U and f:A->B there exists an arrow, called FA_{f}(a):B->U
(impredicative quantification). One
requires i) naturality ii) compatibility with predicative
quantification. In clear:
i) for g:C->B g;(FA_{f}(a))=FA_{f[g]}(g[f];a)
ii) PI_{f}(T[a]) = T[FA_{f}(a)]
Actually these equalities are canonical isomorphisms, but this is
another story (I am trying currently to make a rigorous account of
this coherence problem, which is always thrown under the carpet).
The point of this message is to stress that diktoses are universe
models. You just need to interpret => and PI as
=> = FA_{T[Fst]}(T[Fst];Snd)
(where Fst,Snd are the projections
UxU->U)
PI = FA_{Fst}(App)
(where Fst,App: (U->U)xU->(U->U) are the first
projection and the evaluation maps)
And checking the two equations is then an almost trivial exercise.
What this says is that the definition proposed by J. Meseguer amounts
to ask for two instances of the powerfull FA operator. It is most
likely that once the effort has been made to build some universe model,
it will not cost more to actually see that one has got a diktos, thus
a model of the whole theory of constructions.
And conversely what worries me about the universe models is that there
seem to exist hyperdoctrine models which cannot be viewed easily as
universe models, unless they are put into the powerful presheaf
machinery used by A. Pitts to prove completeness of topos models.
I think of the ideal semantics of Macqueen-Plotkin-Sethi, which can be
formulated rather easily as a hyperdoctrine model, but not
as a universe model, maybe because some work has to be done to understand
ideal semantics of dependent types. By the way the ideal semantics
is not either a model in Meyer-Mitchell's sense, because of the lack of weak
extensionality. So I think it is still useful to have hyperdoctrines.
In response to that criticism, as he indeed already quotes in his
paper, J. Meseguer, argued the following
1. In a hyperdoctrine model you only have NAMES for types, but in general
there is no way of associating to them EXTENSIONS. In this sense, they
are "syntactic" and fail in general to provide a semantic content. This,
by the way, is a point that I have discussed with Lawvere in connection
with polymorphism models and on which we both pretty much agree. I have
also raised the same objection to Seely, without much of an answer.
2. From an expository point of view, I find the notion of a universe very
intuitive and easy to understand without any knowledge of category
theory, whereas the notion of a hyperdoctrine model is, I think, quite
harder to motivate and explain, specially to people with little
acquaintance with category theory. [J. Meseguer]
And I agree, but ideal models are nice..., and universe models are
possibly too strong a notion, since they are so near modelling the
constructions...
Pierre-Louis Curien, LIENS (on leave at SRC till july 89).