Michael Hanus wrote:
> Bernd Brassel wrote:
>> 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.
>
> I think this is a serious argument and I agree with it.
> In particular, it has the consequence that function application
> is no longer rigid in its first argument but should produce
> a run-time error since there would be no way to instantiate
> an unbound variable of functional type.
> I'll have to check whether any of my applications uses
> such kinds of "features". If you know of any important
> application which requires it, please let us know.
You should be aware that this sort of restriction seriously
limits the abilities of using logical style definitions in Curry.
Consider the following innocuous little goal
last [(+), (-), (*)] 7 6
The result of this goal is either 42 or a runtime error depending
on whether last is defined in a purely functional style
last [x] = x
last (_:x:xs) = last (x:xs)
or with a function pattern
last (_ ++ [x]) = x
I would be perfectly happy with that difference if it would show
up in last's type (i.e., by a type class constraint in the type of
the second definition) so that I get a type error in the first
place when attempting to evaluate the sample goal with the second
definition of last.
For the time being, I prefer MCC's current approach, which is to
allow instantiation of logical variables with partial applications
but restrict equality for the arguments of partial applications to
ground terms (this is the explanation why co 42 for
co x | ignore x =:= ignore y = y where y free; ignore x y = y
suspends in MCC). In fact, one could even be a little bit more
general and allow non-ground terms for all arguments whose type
is not polymorphic, but this information is not available at
present in MCC's runtime system.
Regards
Wolfgang
PS: The type soundness problem for HO patterns was addressed in [1],
but apparently this never got implemented in Toy.
[1] Juan Carlos Gonzalez-Moreno, Maria Teresa Hortala-Gonzalez, and
Mario Rodriguez-Artalejo. Polymorphic Types in Functional Logic
Programming.
In: JFLP 2001, special issue 1.
http://danae.uni-muenster.de/lehre/kuchen/JFLP/articles/2001/S01-01/
S01-01.html
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Fr Mai 16 2008 - 12:48:24 CEST