equality of partial applications

From: Sebastian Fischer <sebf_at_informatik.uni-kiel.de>
Date: Sun, 17 Jun 2012 20:23:22 +0200

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 Mon Jun 11 2012 - 12:28:14 CEST

This archive was generated by hypermail 2.3.0 : Mon Nov 18 2019 - 07:15:08 CET