Paul Taylor | 20 Jan 18:00 1988


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]
(Continue reading)

Albert R. Meyer | 20 Jan 18:02 1988


Date: Wed 20 Jan 88 13:54:45-EST
From: Rishiyur S. Nikhil <NIKHIL@...>
Subject: Miranda available
To: csg@...
Cc: ppg@..., mbr <at> XX.LCS.MIT.EDU

With Andy Boughton's help, I have installed Miranda on Newt.  This
version is the first ``official'' release (we had a pre-release
version before).

It has a fairly non-trivial system organization, including:
- a simple module organization, based on files
- compiled versions of source files, including automatic
  maintenance of consistency. (Compiled code = combinators,
  though I don't know what kind.)
- direct transfer between Miranda and a text editor (you can
  choose your editor, I have set the default to emacs)
- automatic recompilation of edited files
- reading, writing, appending to Unix files, including stdin, stdout,
   stderr, ...
- standalone Miranda programs (yes, you can write a Unix filter
   in Miranda)
- ``literate script'' convention, borrowed from the Oxford language

To run Miranda, say


to newt's Unix shell prompt.
(Continue reading)

Albert R. Meyer | 21 Jan 10:07 1988


From: mcvax!!chlo@...
Date: Wed, 20 Jan 88 14:48:01 GMT
To: meyer@...
Subject: Abramsky's Simulation ordering

Dear Professor Meyer,

You may certainly forward my comments on the distinctions between the 
simulation ordering and Bohm trees to TYPES.

Regards, Luke (Ong)
From: mcvax!!chlo@...
Date: Mon, 11 Jan 88 9:54:14 GMT
To: meyer@...
Subject: Abramsky's Simulation ordering

Dear Prof. Meyer,

With reference to the postscript you attached to Samson Abramsky's
e-mail dated 23 Nov, the ``simulation ordering'' M preord N
is not equivalent to two straight-forward modifications of
Bohm-tree ordering (to handle weak head normal forms) which
I have investigated. They are Longo tree ordering and weak Bohm
tree ordering. 

The former was introduced by Giuseppe Longo in his
'83 APAL paper (entitled ``Set-theoretic Models of Lambda-Calculus:
theories, expansions and isomorphisms''). Longo tree differs from
Bohm tree in that the former maps all strongly unsolvable terms
(Continue reading)

Albert R. Meyer | 25 Jan 22:16 1988


Date: Mon 25 Jan 88 19:34:05-EST
From: Rishiyur S. Nikhil <NIKHIL@...>
Subject: Your comments requested ...
To: csg@...

I have put together a document called ``Id Language Extensions''
outlining the proposed extensions to Id regarding algebraic types,
pattern matching, abstract types and syntax for lists, arrays and lazy
evaluation.  Copies are on the credenza in Susan's office.

Please look them over, and try them out on some of your Id programs, if you
can, and let us know your reactions.  Perhaps we can have a lively discussion
in Friday's group meeting, finalize the proposal and get started on

Thanks.  Nikhil

John Mitchell | 26 Jan 03:25 1988

visiting professorship

Stanford has a visiting professorship which may be
awarded to a qualified applicant wishing to visit
for one or more quarters. (Quarters are approximately
10 weeks.) If anyone reading this list is interested,
please let me know as soon as possible. We will begin
reviewing applications on Feb 1.

John Mitchell

Albert R. Meyer | 26 Jan 19:53 1988

Administrative Email to (Internet): types-request <at>

I'll be turning over email list maintenance to a staff member soon, so it
will be helpful if you henceforth send email on TYPES administrative
business---typically updating addresses---to
rather than me personally.  Thanks.

Regards, Albert
Moderator, types@...