[Prev][Next][Index][Thread]

L-domains


Dear Polymorphic Colleagues!
   This is my first contribution to the "types" mailing list, so a
quick introduction first.  I was a student of Martin Hyland (in
Pure Maths) in Cambridge and completed my PhD, entitled

    Recursive Domains,  Indexed Category Theory and Polymorphism

in October 1986.  The main objective of this was the construction of
models of polymorphism (dependent types and Type:Type) in all then
existing categories of domains.  Wherever I could I worked with
continuous rather than algebraic domains, and had to develop a lot of
difficult ordinary domain theory in the process.  I concluded by
constructing a domain of "names" of domains with the property that any
dependent type A[x] had a dependent name n_A(x) such that T[n_A(x)] is
isomorphic to A[x].

   I am now interested in Berry-Girard domain theory and announce
the following (very recent) results of mine.  An "L-domain" is a
cpo in which every principal lower set is a continuous lattice
(the term, which I think should be replaced, is due to Achim Jung, who
has shown that if a cpo has algebraic function space then it is
either bifinite (SFP) or an L-domain).  I argue that "stable" should
mean all connected meets (codirected meets as well as pullbacks).
I can prove:

  (1)  The category of L-domains and stable maps is the category of
algebras for a monad defined over locally connected spaces/locales
or domains (not sets), the corresponding algebraic operations being
connected meets which distribute over directed joins.  cf Day [1975]
who did the same for continuous lattices.

  (2)  The 2-category of L-domains, stable maps and the Berry order
is cartesian closed.  In the course of the proof we have to commute
(not distribute) codirected meets and directed joins, which is the
classic error in Analysis;  we are saved from this calamity by the
Berry order and connectedness.  In fact I have a model of dependent
type polymorphism and am working on Type:Type.

  Observe that besides working with continuous rather than algebraic
domains I have exposed two red herrings in the presentation of
Berry-Girard domain theory (dI-domains, for instance), namely
Girard's peculiar notion of finite, and finite distributivity
(bounded binary meets over bounded binary joins).  I believe that
these domains, with either Scott-continuous maps and the pointwise
order, or with stable maps and the Berry order, are highly respectable
mathematical objects (more so than any other domains to date apart
>from continuous lattices and LFP categories, and certainly much more
so than SFP or boundedly complete domains) and well worthy of
further study.

  Paul Taylor,
  Dept. of Computing,  Imperial College, London SW7 2BZ, UK.
  +44 1 589 5111 x 4980
  pt@doc.ic.ac.uk