Tesla Coils & Corpses report: programming language design

[Daira Hopwood]

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 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.)

So, a stream of the Fibonacci numbers would be:

  fibs : stream[nat]

  fibac : nat --> nat --> stream[nat]
  fibac m n ! = Cons (m+n) (fibac n (m+n))
  fibs = fibac 0 1

(I could have defined this as an unfold rather than using accumulator
parameters, but that would probably have obscured the point.)

In the corecursion/codata approach, we would consider 'fibac' above to be
corecursive. However, with explicit laziness, we don't need support for any
concepts of corecursion or codata in the language in order to handle this.
The stream fibs is represented as a terminating function, so when we apply
that function, we know that we will get a Cons containing the next element
of the stream (or Nil -- in more idiomatic Noether we'd exclude the latter
possibility). The function representing the "tail" of the stream is not
called yet (notice that 'fibac' is only partially applied in its own
definition), and so there is no possibility of nontermination. If you want,
you can think of the stream as "codata", but why introduce another concept
for something that is just an ordinary function?

It is also possible to represent mutually dependent streams or other
non-well-founded structures with this encoding, but that is ordinary
recursion, not corecursion.


I haven't discussed how this interacts with I/O. Well, in Noether there is
no I/O other than message passing. This uses an event-loop model, where each
event loop turn should terminate. An object can have nonterminating behaviour
across turns, but that has no interaction with termination checking for
particular functions, since cross-turn behaviour is never a single execution
of a function.

-- 
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/20141219/ce751293/attachment.pgp>