Hi Andy, this is an interesting issue. Actually, the behavior of PAKCS was different until I detected a problem with normalizing the arguments of partial applications when type classes had been added (where dictionary arguments contained partial applications). Note that the partial application ((1+1)+) can be rewritten as \x -> (1+1) + x but a lambda term will never be normalized in its body (otherwise you might run into termination problems). It is a feature of PAKCS that you can visualize the normal form of a functional value. In other systems, like KiCS2, you'll never see them so that this question does not occur. Best regards, Michael On 5/28/19 7:00 PM, Andy Jost wrote:

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 expression has no normal form because the first occurrence of + cannot be eliminated.  Yet PAKCS seems to treat it as if it was a value.  This makes a certain 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 partial 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#Prelude.Int 1))

Call: id (_impl#+#Prelude.Num#Prelude.Int (1 _impl#+#Prelude.Num#Prelude.Int 1))

Exit: id (_impl#+#Prelude.Num#Prelude.Int (1 _impl#+#Prelude.Num#Prelude.Int 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#Prelude.Int 1)) (HNF: _impl#+#Prelude.Num#Prelude.Int (1 _impl#+#Prelude.Num#Prelude.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 reasons to NOT reduce an expression such as ((1+1)+) to (2+)?  I can imagine that attaining correct semantics might require this delay if the subexpression is non-deterministic but I’m not entirely convinced. Certainly, it is not obvious to me.

 

And is there some theoretical basis upon which I can understand these seeming quirks?

 

-Andy

_______________________________________________ curry mailing list -- curry@lists.rwth-aachen.de To unsubscribe send an email to curry-leave@lists.rwth-aachen.de https://lists.rwth-aachen.de/postorius/lists/curry.lists.rwth-aachen.de