Non-strict semantics and partial application

[Ang Soon]

Hello,

I'm implementing a non-strict toy language supporting partial function
application, but I've come to realize I'm confused over what non-
strictness means.

Consider, for example, the K-combinator:

K x y => x

Suppose K is _partially_ applied on bottom; does it evaluate to bottom
right away, or does it evaluate to a unary combinator that will
evaluate to bottom if evaluated? I.e.,

K undefined => ?

Thanks,

Ang

[Ertugrul Söylemez]

Post by Ang Soon
I'm implementing a non-strict toy language supporting partial function
application, but I've come to realize I'm confused over what non-
strictness means.
K x y => x
Suppose K is _partially_ applied on bottom; does it evaluate to bottom
right away, or does it evaluate to a unary combinator that will
evaluate to bottom if evaluated? I.e.,
K undefined => ?

It shouldn't evaluate to bottom, because then it would be a strict
language. If you ever ask for the result of 'K undefined', for example
when printing it, then it needs to be evaluated.


Greets,
Ertugrul

[George Neuner]

On Tue, 29 Jun 2010 03:45:05 -0700 (PDT), Ang Soon

Post by Ang Soon
I'm implementing a non-strict toy language supporting partial function
application, but I've come to realize I'm confused over what non-
strictness means.

Well, "strictness" means that an argument's value is required by the
computation ... so "non-strictness" means the value isn't required.

Post by Ang Soon
K x y => x
Suppose K is _partially_ applied on bottom; does it evaluate to bottom
right away, or does it evaluate to a unary combinator that will
evaluate to bottom if evaluated? I.e.,
K undefined => ?

Partial application is non-strict ... the function can't be evaluated
until all the required arguments are bound. The result of partial
application of a function to some of its arguments is a new function
of the remaining arguments.

So:
K x [x := _bottom_] => \y.( K x y [x := _bottom_])

i.e. the result is a function in search of an argument.


Since K itself is non-strict, the argument x is really a symbol
denoting the computation that results in _bottom_. Since K does not
evaluate x, the result is not _bottom_ but x.

K x y [x := _bottom_] => x.


Partial application of K can be a bit confusing because K simply
returns the first argument, so it would seem that the second argument
is unnecessary and

K x y = K x

But K is defined to take 2 arguments, so partial application to one of
them results in a function of the other.

Hope this helps.
George

[Ang Soon]

Post by George Neuner
On Tue, 29 Jun 2010 03:45:05 -0700 (PDT), Ang Soon

Post by Ang Soon
I'm implementing a non-strict toy language supporting partial function
application, but I've come to realize I'm confused over what non-
strictness means.

Well, "strictness" means that an argument's value is required by the
computation ... so "non-strictness" means the value isn't required.

Post by Ang Soon
K x y => x
Suppose K is _partially_ applied on bottom; does it evaluate to bottom
right away, or does it evaluate to a unary combinator that will
evaluate to bottom if evaluated? I.e.,
K undefined => ?

Partial application is non-strict ... the function can't be evaluated
until all the required arguments are bound.  The result of partial
application of a function to some of its arguments is a new function
of the remaining arguments.
   K x [x := _bottom_] => \y.( K x y [x := _bottom_])
i.e. the result is a function in search of an argument.
Since K itself is non-strict, the argument x is really a symbol
denoting the computation that results in _bottom_.  Since K does not
evaluate x, the result is not _bottom_ but x.
   K x y [x := _bottom_] => x.
Partial application of K can be a bit confusing because K simply
returns the first argument, so it would seem that the second argument
is unnecessary and
   K x y = K x
But K is defined to take 2 arguments, so partial application to one of
them results in a function of the other.
Hope this helps.
George

Thanks, everyone, this set my mind straight. Very helpful,

Cheers, Ang

[Dan Doel]

Post by Ang Soon
K x y => x
Suppose K is _partially_ applied on bottom; does it evaluate to bottom
right away, or does it evaluate to a unary combinator that will
evaluate to bottom if evaluated? I.e.,
K undefined => ?

Simon Peyton-Jones (I believe) came up with "weak head normal form" to
describe the sort of terms that non-strict graph reduction yields. The rules
go something like:

A term is in weak head normal form if it is:

1) A lambda expression
2) An under-applied built-in function.

In a combinator calculus, we don't have the former, and so only have to
worry about redexes for the latter. So

K x

is already in weak head normal form, regardless of what x is. Similarly:

S f and S g h

are in whnf, and don't compute, regardless of f, g and h. But:

K x y

reduces to x, and may continue from there. In particular:

K (K x y)

is in weak head normal form, and doesn't reduce to K x.

In a language with lambda:

\x -> e

is in whnf regardless of e, and so similarly:

\x -> (\y -> y) x

does not reduce further.

If you imagine that 'undefined' describes any expression that will reduce
without end, then the answer to your question is that, no, 'K undefined' is
not undefined, because it does not reduce at all.

-- Dan