Types & Strictness (forwarded)

Date:     Thu, 16 Mar 89 12:23:18 GMT

                     ---- TYPES & STRICTNESS ----
                             Gavin Wraith
                              15 Mar 89

Am I musing through my hat on the following ?

The functional programming community seem divided into two camps;
the major camp being proponents of normal order evaluation, a
minority arguing for applicative order. Everybody agrees that the
latter is more efficient, but the former is necessary for easy
manipulation of infinite data-objects.

Data-objects come in two sizes: small and large. Small data-objects
may as well be treated strictly. Why bother to delay updating the
components of the object, even if they will never be accessed, if there
are only a few of them? The updating might be quicker than forming the
closures necessary to do the delay.

Infinite data-objects arise as values of recursive product types.
To be precise about what I mean, recall that finite lists are
values of the recursive sum type

sum list(a) =
    nil : unit -> list,
    cons : a*list -> list ;

and that infinite lists are values of the recursive product type

product stream(a) =
    hd : stream -> a,
    tl : stream -> stream ;

and these two should not be confused. Lists in my sense are always
finite and streams are always infinite. You can define a third type

product seq(a) =
    start : seq -> opt(a),
    next  : seq -> opt(seq) ;

where

sum opt(a) =
    stop : unit -> opt,
    go_on : a -> opt ;

whose values can be construed as either lists or streams via

def list_to_seq by
start (list_to_seq nil) = stop
next  (list_to_seq nil) = stop
start (list_to_seq (cons (a,x))) = go_on a
next  (list_to_seq (cons (a,x))) = go_on (list_to_seq x);

def stream_to_seq by
start (stream_to_seq x) = go_on (hd x)
next  (stream_to_seq x) = go_on (stream_to_seq (tl x));

Note the type of take : NAT->stream(a)->list(a) defined by

def take by
take zero x = nil
take (succ n) x = cons(hd x,take n (tl x));

Now it may be that programmers would simply find it inconvenient to
be this nit-picking about distinctions between types, when a little
fudge with an exception here or there, or a domain theoretic semantics
with bottom elements allows you to avoid the distinctions. However,
>from the mathematical point of view I find it much clearer to retain
a sharp distinction.
I suggest that the only recursive values one ever wants are either
functions or values of recursive products (like stream(a), but I can
give you plenty of other examples). Would it not be feasible to
have data-objects treated strictly unless they were of the latter kind?
After all, you could always translate a finite object into a
potentially infinite one (e.g using an analog of list_to_seq)
when you wanted to handle it lazily, and then chop off a finite
portion (with an analog of take) afterwards.

I would be interested to hear from anyone who has comments, or who
can set down rigorously what I am groping for (if there is anything
worth groping for). I am trying to suggest that a categorical
approach to types should reveal strictness information.

Gavin Wraith
=========================================================================

                           RESPONSE by Andy Pitts

Translating your example type definitions into a language with unit
type, binary product type (X*Y), binary sum type (X+Y), initial recursive
types (muX.a), and final recursive types (nuX.a) we get

  list(a) = muX.unit+(a*X)

stream(a) = nuX.a*X

   seq(a) = nuX.(unit+a)*(unit+X)

(? So seq(a) = nuX.unit+a+X+(a*X), where `=' means  isomorphic ...?)

The last one looks odd. What about the "lazy list" type most often
mentioned by functional people---i.e. the type of potentially infinite
lists of elements from a? In ML that's

datatype   'a llist = Nil | Cons of 'a * (unit -> 'a llist)

If we extend the type expression language to include explicit
computation types X~ (= "type of computations of type X"), isn't the
meaning of this exactly described by

llist(a) = muX.unit+(a*(X~))

(ML type (unit->X) simulates X~, with evaluation of a computation e:X~
to a value (if any) corresponding to function evaluation of e:unit->X
at the unique value ():unit.)

I am quite enthusiastic about the usefulness of explicit computation
types in a metalanguage for denotational semantics (with just initial
recursive types---but initial with respect to a notion of
approximation between types rather that with respect to all
functions). See Plotkin's notes on "partial domain theory", Constable
& Smith's article in LICS88 and Moggi's really nice (for us category
buffs) article in LICS89.

Andy Pitts