These are all very interesting thoughts, thank you Wolfgang!
Wolfgang Lux wrote:
> 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.
This is of course just a question of the viewpoint. The main point is
though, that there are more possibilities for generic functions on types
which you know all the constructors of. Do you agree with that? This
does not mean of course, that extensible types are a bad concept. As you
rightly said:
> 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.
If we had something like type classes or overloading, we might be able
to nicely separate the concepts and say that some generic functions work
only on "fixed" types, i.e. not extensible or potentially infinite types.
> 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.
Do not be surprised, but this is the very reason why I do not like the
integer type also. Why restrict a functional-logic language in such a
way that so many basic functions like (+),(-),take, drop, splitAt and
anything employing the basic type Int are not usable in a logical way?
I would much prefer a standard Int which is fully narrowable and maybe
provide the primitive type in a library if anyone really needs it. But I
would not care nuch if that primitive type is not in the supposed class
of types for which (=:=) is defined.
> 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.
This is also a nice example that shows how much eta expansion would
change the semantics. And anyway, partial calls have some quality which
makes them very different from other kinds of values. As a very plastic
example, I once hacked Michaels web-pages by sending hand-forged partial
calls to his cgi-scripts. You could make a lot of damage, before he
changed his system to not make use of show/read for partial function
calls...
> 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
All very nice but I think you agree that this demands more of the
implementations of Curry. So why put it into the basic definition of the
language, as long as simpler approaches might work just as well (or better)?
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Mi Apr 11 2007 - 11:56:46 CEST