Hello FunLog people,
last week we had our annual German workshop about programming languages
and I learned (among other interesting things) a really interesting
example from Wolfgang Lux. He published the example already in 2007 so
maybe many of you know it already, cf.
http://danae.uni-muenster.de/~lux/pubs/BadHonnef07.html.
But anyway I find it interesting enough to discuss on this list.
Suppose you have an innocent function "ignore", which I write with
Toy-syntax in mind, since the example also works there:
ignore :: A -> B -> B
ignore _ Y = Y
Now we can write a function co like this:
co x | ignore x =:= ignore y = y where y free
Or with a Toy-Style:
co X = Z <== (ignore X == ignore Z)
where for Curry we add the definitions:
x <== c | c = x
Z = x where x free
(==) = (=:=)
(And for the MCC we add:
import Prelude hiding ((==))
at the beginning)
What is the type of this function "co"?
Because "ignore" is so very polymorphic, it ends up to be
co :: A -> B
in either case. And here is a second version of co:
co2 :: A -> B
co2 X = gnore (ignore x)
gnore :: (A -> A) -> B
gnore (ignore x) = x
Both versions work fine in Toy and in PAKCS, though the second version
works for different reasons. In Toy "gnore" uses an HO-Pattern, whereas
in PAKCS it is a function pattern. Both have quite a different
operational behavior - at least for most other examples.
Wolfgang's MCC does not allow the second version but it does allow the
first one, although it suspends during evaluation of, e.g., (co 42).
KiCS does allow neither, you get a type error for any version. This is,
however, a pure coincidence because of having a typed target language
(Haskell) which does not allow to write a terminating type cast without
unsafe features and the type error message is not that easy to comprehend.
In my point of view the lesson is clear: there should not be
unification, free variables nor any kind of narrowing for type A -> B.
With Wolfgang's proposal to add type classes like "Narrow" or
"Unifiable" to the definition of the Curry language, we could omit this
problem and all unsafe features would be in Unsafe again.
For function patterns like in PAKCS giving up patterns of functional
type would not be problematic. But HO-Patterns seem to be much closer to
the essence of the problem.
Have a nice type casting!
Bernd
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Mi Mai 14 2008 - 15:50:59 CEST