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