Path: utzoo!attcan!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!sdd.hp.com!samsung!uunet!mcsun!ukc!strath-cs!cs.glasgow.ac.uk!jl
From: jl@cs.glasgow.ac.uk (John Launchbury)
Newsgroups: comp.lang.functional
Subject: Re: Intermediate Codes for Functional Languages
Message-ID: <7251@vanuata.cs.glasgow.ac.uk>
Date: 18 Dec 90 10:33:43 GMT
References: <3054@skye.cs.ed.ac.uk> <7185@vanuata.cs.glasgow.ac.uk> <1975@m1.cs.man.ac.uk> <5455@rex.cs.tulane.edu>
Organization: Computing Sci, Glasgow Univ, Scotland
Lines: 59

fs@rex.cs.tulane.edu (Frank Silbermann) writes:

>But how can one speak of strict or lazy constructors?
>Consider for example, the ordered pair constructor,
>which uses elements X1 and X2 of domains D1 and D2,
>to create the element <X1,X2> of domain D1xD2.
>The standard selector functions will choose
>the appropriate piece of <X1,X2> regardless
>of whether the other side happens to be the bottom.

>Of course, the language designer may choose to deny the programmer
>direct access to the standard selector functions,
>and instead provide selector functions which,
>before selecting an element, verify that both sides
>are strictly above bottom.  In any case,
>the elements <X1,bot>, <bot,X2> and <bot,bot> are
>distinct elements of D1xD2, regardless of whether
>any particular language lets the programmer make use of this fact.

>So, when we speak of strict constructors, are we not _really_
>describing a property of the _selector_ functions, and not the constructor?
>Or, is there another version of domain theory I am not aware of?

No, no other version of domain theory. It's just the method of
modelling the implementation by domain theory that you don't seem
to be fully aware of. First of all, sequential machine implementations
are inherently strict. In order to achieve laziness, implementations
make use of closures - pieces of code/graph which represent a
potential computation. Closures of values of a type A may be modelled
by values of the type (Lift A) - all the elements of A plus a new bottom.
The implementation will be strict in this new bottom, but not in
the bottom of A (not yet evaluated).

A constructor (a sum injection) may be strict or lazy: the latter is
achieved by making the constructor point to a closure, the former
by making it point to the value (if the process of producing the value
does not terminate, then neither will the construction of the sum).
Domain theoretically, the machine uses strict sum (smash sum) in both
cases, but in the lazy case it is the smash sum of lifted values. By
the standard isomorphism this is the same as separated sum.

Product formation is similar, but there are distinctions. Consider
the construction of a closure for a pair. What actually happens
(in the G-machine, TIM etc.) is that a pair cell is constructed
with a closure to each value. The construction of the pair is
strict in that if the construction of either closure failed to
terminate successfully (e.g. out of heap) then so would the
construction of the pair. Thus pair construction is strict product,
but it is the product of closures of values. This is isomorphic to
a closure of a non-strict product. So long as it is impossible to
get a recursive value using just products, e.g.
	x = (1,x)
then this is a correct implementation (note that the above definition
of x is ruled out by the common HM type system.)

Finally, it is worth noting that exactly the same trick is used to
obtain lazy functions. This uses the isomorphism
	A -> B  ===  (Lift A) => B
where => is the space of strict functions.