Dear all,
the Curry report specifies constraint equality for data terms and
logic variables (in Appendix D.3) but some Curry systems also support
constraint equality of partial applications. For example, both MCC and
PAKCS allow the following comparisons:
Prelude> (+1) =:= (+1)
Success
Prelude> (+1) =:= (1+)
No solution
I consider this feature a bug because it destroys many equational laws
which are useful for program development:
Prelude> id =:= map id
No solution
More severe might be the observation that it allows to define a type
cast as follows:
ignore :: _ -> a -> a
ignore _ x = x
unwrap :: (a -> a) -> _
unwrap y | y =:= ignore x = x
where x free
cast :: a -> b
cast = unwrap . ignore
In PAKCS we can now write an expression that nondeterministically
returns an integer or a boolean:
pakcs> if True?False then cast False else 0
Result: False
More solutions? [Y(es)/n(o)/a(ll)]
Result: 0
Is this a known bug of PAKCS?
MCC is more restrictive and suspends in the branch that uses 'cast':
cyi> if True?False then cast False else 0
Suspended
More solutions? [Y(es)/n(o)/a(ll)]
0
What is the rule that makes MCC suspend in the second example
comparing partial applications but not in the first? Does this rule
ensure type safety in general?
Best regards,
Sebastian
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Mo Jun 11 2012 - 12:28:14 CEST