H ?
«
‹
←
→
›
»
Language peer sets for SOL:
United States↑
United States/1985↑
Designed 1985 ↑
1980s languages ↑
Fifth generation↑
Late Cold War↑
SOL(ID:1184/sol003)
Second-Order Lambda calculus
alternate simple view
Country: United States
Designed 1985
Published: 1985
Second-Order Lambda calculus. A typed lambda calculus.
References:
Mitchell J. et al, (1985) Mitchell J. et al, "Abstract Types have Existential Type"
in [POPL 1985] (1985) [ACM SIGACT-SIGPLAN] Conference Record of the 12th ACM Symposium on Principles of Programming Languages, New Orleans, Jan. 1985. (POPL '85)
Resources
-
Review of Mitchell 85 by David Watt The title of this paper suggests a hot new discovery being rushed
out of the laboratory and announced to the world. The reality is
less exciting and says much about publication delays. The paper was
first presented at a symposium in January 1985; it was submitted to
TOPLAS in June 1986 and revised in March 1988. The delay should
have provided an opportunity to polish the paper, but a number of
careless errors have persisted, and the ML examples use syntax that
is years out of date.
The main theme of this paper is that existential types (which derive from
constructive type theory) can be used to ascribe types to implementations
of abstract types. For example, the omnipresent t-stack abstract type has the
signature
:.OC :.HB abstype tstack with
empty: t-stack,
push: t ∧9Tt-stack :2WZ t-stack,
pop: t-stack :2WZ t ∧9Tt-stack:.HT :.OE
and each of its implementations would have the existential type
:.OC :.HB ∃9Ts. s ∧9T(t ∧9Ts :2WZ t)-
∧9T(s :2WZ t ∧).:.HT :.OE
(the authors use `∧ for Cartesian product). Similarly, the
t-queue abstract type might have the signature
:.OC :.HB abstype t-queue with
empty: t-queue
insert: t ∧9Tt-queue:2WZ t-queue
remove: t-queue :2WZ t ∧t-queue,:.HT :.OE
and the corresponding existential type would be
:.OC :.HB ∃Qq. q ∧Q(t∧9Tq :2WZ q)-
∧q :2WZ t ∧9Tq).:.HT :.OE
The above two existential types are equivalent; they are independent
of the operations' names and of their intended semantics.
Since abstract type implementations have types, they are first-class values
and can be passed as parameters and returned as function results. The
authors exploit these capabilities by presenting a tree-search function with
a formal parameter of the above existential type. When the function is
called with a stack implementation as an actual parameter, it performs a
depth-first search. When called with a queue implementation, the function
performs a breadth-first search (actually, right to left). This may not
be useful in practice; the tree-search function is hard to understand.
Another of the authors' examples is what must be the most opaque programming
of the sieve algorithm ever published.
This paper invites comparison with Cardelli and Wegner's 1985 survey
paper on type theory [1]. The latter paper was more timely, more accurate,
and more readable, yet it is not even referenced in this paper.
Search in:
Google
Google scholar
World Cat
Yahoo
Overture
DBLP
Monash bib
NZ
IEEE
ACM portal
CiteSeer
CSB
ncstrl
jstor
Bookfinder
|