Re: New PAKCS release (Version 1.8.0)

From: Emilio Jesús Gallego Arias <egallego_at_babel.ls.fi.upm.es>
Date: Tue, 10 Apr 2007 19:00:26 +0200

Wolfgang Lux <wlux_at_uni-muenster.de> writes:

> same should be done for partial applications, so a goal like
> (x===const y) =:= False
> should succeed with a disequality constraint x/=const y in the
> constraint store regardless of whether there is another function
> with const's type signature in scope or even present in the linked
> program.

Ok, so we get a constraint store with {x =/= const 2} (Let me replace
y -> 2)

If I recall correctly, const is defined as:

const x y = x

So the traditional meaning is
   \exists X. X =/= \_ -> 2

with X \in a -> b -> a

I'm not opposed to this, but this gets ugly if I say:

  myf = \x -> 2

and then

  x =:= myf

Then, can the system check whether myf =/= const 2 ?

Anyways, all the above depends on how you want to interpret
eta-extensionality.

> Incidentally, the point that you need disequality constraints in
> order to reasonably define (===) for numeric data types (and may
> be for potentially infinite data types as well) makes me think
> that defining (=:=) in terms of (===) is putting the cart in
> front of the horse. I think, it should rather be done the other
> way around:
> x === y | x=:=y = True
> x === y | x=/=y = False

I think that's just an implementation issue. If done properly, both
ways have the same operational meaning.

Regards,

Emilio

_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Mi Apr 11 2007 - 11:57:18 CEST

This archive was generated by hypermail 2.3.0 : Do Jun 20 2024 - 07:15:08 CEST