🚀 go-pugleaf

In article <6853@rex.cs.tulane.edu> fs@caesar.cs.tulane.edu (Frank Silbermann)
writes:
>By the way, does the _formal_ theory of typed lambda calculus accept
>constructor-based primitive functions defined via rewrite-rules?
>For example, in the lambda-notation of denotational semantics,
>one can _force_ any primitive function `f: A->B' to be strict
>simply by defining f(BOT_A) = BOT_B.

It's not that simple.  In general you can't define f(BOT_A).  In a fully lazy
system, its value is determined by the values at other points.  If don't want
to be fully lazy, which is what you're asking for, you can make it less
determined.  You can never make it more determined.  Really this is a semantic
argument, rather than something provided in your type system.

I've posted about this subject before, so i won't repeat what i said then.
Bottom is the least determined value, and it must be consistent with other
values which are more determined.  Basically, i'd say you shouldn't think of
bottom as `fails to terminate', but rather as `status unknown'.

In fact you can detect some cases of failure to terminate, and give them new
values in your type system.  Then if you know that some expression fails to
terminate, it's not bottom.  Of course you can never hope to catch all cases.

>One can even use this method
>to define a strict version of function application.

I would say that strictness is a property of specific primitive combinators,
rather than something you can specify in your type system.  You can use strict
primitive combinators to force evaluation of some expression, even if you
don't use its value.

Suppose we define a combinator with HOLD x y = x, but we say that it's strict
in y.  In other words, it computes x and y in some order or in parallel, and
when both values are available it returns the first.

There are many ways to simulate this, depending on what primitives you have
available.  For example, if x and y are numbers you could define it as HOLD x
y = 0*x+y.  This assumes that the multiplication primtive is strict in both
arguments.  If it's too smart, this won't work.  So let's just assume HOLD is
a primitive.

This combinator makes a lot more sense when you consider it temporally.  It
`holds up' the value x until y is ready.  This provides a way to synchronize
two values, which is useful if we want to write them out to disk together or
something like that.  The idea is that we only want to write them both out if
they're both ready, otherwise we don't want to write anything.  You can see
the similarity to database transactions.

If we extend this to include side-effects (and switch the parameters), we get
normal sequential execution.  This combinator would be exactly the same as the
comma operator in C or the semicolon `operator' in Pascal.  If you want to
execute a C program with combinators, this is exactly what you do.

But then you can change the semantics to be more lazy, by removing the
strictness.  This gives you dead code elimination and common subexpression
elimination, the usual C compiler stuff.  The interesting thing is that this
makes a `new' C where more things terminate.  For example, the following
function returns 0:

	int foo()
	{
	  while (1);
	  return 0;
	}
--
Joe Keane, supercombinator hacker