Tesla Coils & Corpses report: programming language design

[Daira Hopwood]

On 19/12/14 22:54, Daira Hopwood wrote:
> On 18/12/14 23:19, Matthias Görgens wrote:
>> [Tesla Coils and Corpses notes]:
>>> As far as we can see the vast majority of things that people write are trivially
>>> terminating, or they have an infinite loop based on I/O.
>>
>> You might want to look up co-recursion and codata, a way to deal with I/O based
>> infinite loops, and still keep some notion of totality and (co-) termination.
>>
>> See eg http://blog.sigfpe.com/2007/07/data-and-codata.html?m=1
> 
> I am skeptical of the need for codata and corecursion as explicit concepts,
> especially in strict languages.
> 
> In a language that is strict by default, like Noether, laziness can be encoded
> at the library level using explicit delays and forces.
> 
> For simplicity let's ignore the need for memoization, since that doesn't affect
> termination behaviour. (In practice, there would be a single-assignment slot
> associated with a delay to hold any already-computed value.)
> 
> With that simplification, we can define a lazy value to be just a terminating
> function

I should have said "deterministic terminating function".

> from the unit value '!' to some other type:
> 
>   lazy[t] = ! --> t
> 
> such as a stream:
> 
>   stream[a] ! = Nil | Cons a stream[a]
> 
> (This is equivalent to 'stream[a] = ! --> (Nil | Cons a stream[a])'. Each
> forcing reveals one more element in the stream, or reveals that it is now
> empty.)

On reflection I'm not quite happy with this encoding of explicit laziness.

The issue is that t is not a subtype of ! --> t. Ideally, we want forcing a
non-lazy value to be the identity function, because that allows us to write
code that accepts both lazy and non-lazy values, without requiring explicit
suspensions of the latter just to make the types work out.

(This is consistent with other effects in Noether: code modifications that
eliminate an effect do not require any superfluous syntactic changes. I believe
this is a very important property to ensure that the effect system does not
appear to be "getting in the way".)

It's fairly easy to add a t <: lazy[t] subtyping rule if we treat laziness
as a built-in concept recognized by the type system. But it would be more
flexible to generalize the idea of a suspension so that arbitrary
--possibly user-defined-- effects can introduce different kinds of
suspension. If we use the notation t~e for t annotated with an extra
effect e, then t <: t~lazy would be a consequence of the effect subtyping
rule, t~e <: t~f whenever e has a subset of the effects of f.

This isn't premature generalization because we have other use cases --
for example we would like:

  t <: t~far   (a local reference can be used in place of a far/remote one)
  t <: t~alias (a unique reference can be used in place of an aliasable one)

and so on.

Note that "shallow" implicit coercion from t to lazy[t] is not sufficient.
For example,

  list[a] = Nil | Cons a list[a]

must also be a subtype of stream[a] for any a.

This shows that the subtyping genuinely increases expressive power, because
writing this coercion manually would not be only a local transformation (and
would require traversing strict data structures to coerce them to lazy,
defeating the purpose).

However it also places the constraint on the implementation that the
representations of list[a] and stream[a] must be compatible. (In particular,
the tail of each cons cell has to be the same size in both representations,
and the implementation of ! has to be able to recognize values that are not
suspensions.) This is actually not a huge problem: most implementations of
lazy functional languages work by replacing suspensions with their forced
results.

Note that the effect-based encoding differs from the function encoding also
in whether it is possible to nest suspensions (of a given kind). The function
encoding would allow a value of type:

  ! --> ! --> t

which would not be fully forced by a single application to !. There seems
no good reason to allow nesting of suspensions of the same kind, and it could
be a source of confusing type errors for beginners.

In any case, adding t <: lazy[t] subtyping doesn't affect the conclusion that
corecursion and codata do not need to be explicitly supported; the termination
analysis is the same as if the function-based encoding had been used. Also,
this works for all kinds of suspensions that need to be explicitly forced,
which supports the argument for generalized suspensions.

-- 
Daira Hopwood ⚥

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 490 bytes
Desc: OpenPGP digital signature
URL: <http://tahoe-lafs.org/pipermail/tahoe-dev/attachments/20141222/36c37eb8/attachment.pgp>