Re: New PAKCS release (Version 1.8.0)

From: Wolfgang Lux <wlux_at_uni-muenster.de>
Date: Mon, 02 Apr 2007 09:18:12 +0200

Bernd Brassel wrote:

> However, the concept of extensible data types is in conflict with many
> approaches discussed recently:
>
> a) introducing a function (===) equivalent to a flexible version of
> (==)
> which would allow to express (=:=).
> x =:= y | x===y = success
> b) equivalence between free variables and generator functions,
> along the
> lines of
>
> unknown::Nat
> unknown = S unknown
> unknown = Z
>
> c) some forms of negation constraints for (=:=)
>
> All of the above concepts would allow to write a function like test
> and
> isF above.

I see the problem. But then I would say that the above approaches are
suspicious. It would be a pity if these approaches would rule out the
possibility of adding an equivalent of Objective Caml's polymorphic
variants (which basically are extensible algebraic data types) to
Curry.

That said, I think the situation is not that bad. The point is that
an implementation must not consider partial applications like an
inductively defined data type, but rather more like the numeric types.
For instance, it would be unreasonable to expect that the goal
   (x===0) =:= False
is going to bind x non-deterministically to any integer value except
zero. I would rather assume that the above goal would succeed with a
disequality constraint x/=0 being added to the constraint store. The
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.

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

Regards
Wolfgang


_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Wed Apr 11 2007 - 11:56:34 CEST

This archive was generated by hypermail 2.3.0 : Mon Nov 11 2019 - 07:15:07 CET