[curry] "Normal form" of a partial application

From: Andy Jost <Andrew.Jost_at_synopsys.com>
Date: Tue, 28 May 2019 17:00:16 +0000

I'm trying to understand the following output of PAKCS:

test> ((1+1)+)
_impl#+#Prelude.Num#Prelude.Int (1 _impl#+#Prelude.Num#Prelude.Int 1)
test> :t (+) (1+1)
(+) (1+1) :: Num a => a -> a

It surprises me that the subexpression 1+1 is not reduced. The full expres=
sion has no normal form because the first occurrence of + cannot be elimina=
ted. Yet PAKCS seems to treat it as if it was a value. This makes a certa=
in practical sense in the context of the REPL, but if this is like a value =
then why is the subexpression not reduced?

If I go one step further and apply $!! to force normalization of the partia=
l application, I see that $!! ignores the subexpression 1+1 (trace shown):

test> id $!! ((1+1)+)
Call: id $!! (_impl#+#Prelude.Num#Prelude.Int (1 _impl#+#Prelude.Num#Prelud=
e.Int 1))
Call: id (_impl#+#Prelude.Num#Prelude.Int (1 _impl#+#Prelude.Num#Prelude.In=
t 1))
Exit: id (_impl#+#Prelude.Num#Prelude.Int (1 _impl#+#Prelude.Num#Prelude.In=
t 1)) (HNF: _impl#+#Prelude.Num#Prelude.Int (1 _impl#+#Prelude.Num#Prelude.=
Int 1))
Exit: id $!! (_impl#+#Prelude.Num#Prelude.Int (1 _impl#+#Prelude.Num#Prelud=
e.Int 1)) (HNF: _impl#+#Prelude.Num#Prelude.Int (1 _impl#+#Prelude.Num#Prel=
ude.Int 1))
_impl#+#Prelude.Num#Prelude.Int (1 _impl#+#Prelude.Num#Prelude.Int 1)

This seems to imply that (1+1)+ is a normal form, which it clearly is not.

Is this perhaps some corner that is not well defined, or are there good rea=
sons to NOT reduce an expression such as ((1+1)+) to (2+)? I can imagine t=
hat attaining correct semantics might require this delay if the subexpressi=
on is non-deterministic but I'm not entirely convinced. Certainly, it is no=
t obvious to me.

And is there some theoretical basis upon which I can understand these seemi=
ng quirks?

-Andy



_______________________________________________
curry mailing list -- curry_at_lists.rwth-aachen.de
To unsubscribe send an email to curry-leave_at_lists.rwth-aachen.de
https://lists.rwth-aachen.de/postorius/lists/curry.lists.rwth-aachen.de
Received on Mi Mai 29 2019 - 18:48:34 CEST

This archive was generated by hypermail 2.3.0 : Do Feb 01 2024 - 07:15:13 CET