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_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
>
_______________________________________________
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:44 CEST