- Contemporary messages sorted: [ by date ] [ by thread ] [ by subject ] [ by author ] [ by messages with attachments ]

From: Bernd Brassel <bbr_at_informatik.uni-kiel.de>

Date: Wed, 14 May 2008 15:43:45 +0200

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

Date: Wed, 14 May 2008 15:43:45 +0200

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

*
This archive was generated by hypermail 2.3.0
: Di Sep 29 2020 - 07:15:03 CEST
*