Hi Sebastian,
> 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
You are right that these equivalences do not hold. However, what you are expecting here is extensional equality, which is impossible to support in Curry. So what would be the alternatives? Without modifying Curry's type system, the only alternative would be reporting a runtime error when you attempt unifying two partial applications. With type classes we could prevent equality constraints between partial applications by making (=:=) a method of a type class; however that introduces its own bunch of problems (recall my 2008 talk at the workshop in Bad Honnef [1]) and hence MCC's type classes branch does not follow that route.
> 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?
It should be known :-) I mentioned it in my 2007 talk in Bad Honnef [2], (see footnote 1 on p.2 of the paper). It inspired Bernd to a few more variations on this topic in this thread: [3].
> 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?
MCC uses a (decent?, dirty?) hack to cope with the type unsoundness present in unifications between two partial applications and between two existentially quantified data constructors, which show the same problem: It uses (a sort of) runtime type checking. Since data constructors and partial applications carry enough type information in the runtime to distinguish, say, the integer constant 0 from the data constructor False whereas unbound variables have not enough information attached to them in the runtime (in fact they are untyped), equality constraints between terms whose roots are partial applications or existentially quantified constructors are restricted to ground terms. This is also mentioned in Sect. 8.1.3 of MCC's User's Guide. Hence, in your example it is the application (cast False) that suspends the evaluation.
Regards
Wolfgang
[1]
http://danae.uni-muenster.de/~lux/pubs/BadHonnef08.html
[2]
http://danae.uni-muenster.de/~lux/pubs/BadHonnef07.html
[3]
http://www.informatik.uni-kiel.de/~curry/listarchive/0705.html
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Mi Jun 20 2012 - 17:18:17 CEST