Re: equality of partial applications

From: Wolfgang Lux <wlux_at_uni-muenster.de>
Date: Mon, 18 Jun 2012 13:31:46 +0200

Sebastian Fischer wrote:

>> However, ruling out unifications between two partial applications means that we would have to rule out unifications between a variable and a partial application too;
>
> Yes, I would prefer to rule out every unification between arguments of
> functional type and only support those unifications that are specified
> in the Curry Report, that is, between data terms and logic variables
> and data terms.
>
> If it is not possible to rule out unification of two logic variables
> of functional type without type information, I think it is fine to let
> them succeed as, in practice, entually such variables will eventually
> get unified with actual functions (which would then fail.)
>
>> But generating a runtime error (or failure) on unifications like x =:= map id when x is a free variable IMHO is a too high price to pay
>
> Can you give an example that demonstrates how high the price is?

Probably the most spectacular failure would be f $!! map id because it uses (=:=). Admittedly, there's not much reason to use that expression directly, but keep in mind that a partial application may occur deeply nested inside the argument of (=:=) or ($!!), which could lead to rather non-obvious failures.

Another case happened to me when writing a simple expression parser with MCC's Parser library (which is essentially the same as the one in PAKCS) before MCC supported equality constraints involving partial applications:
  expression = term t <*> plus_minus op <*> expression e >>> op t e <||> term where op, t, e free
  term = factor f <*> prod_div op <*> term t >>> op f t <||> factor where f, op, t free
  factor = terminal '(' <*> expression e <*> terminal ')' >>> e <||> num where e free

  plus_minus = terminal '+' >>> (+) <||> terminal '-' >>> (-)
  prod_div = terminal '*' >>> (*) <||> terminal '/' >>> div

  num = some digit l >>> numeric_value l where l free
  digit = satisfy (true . isDigit)
This parser would fail because (>>>) uses a unification involving its second argument internally, but this is by no means apparent to the user.

Wolfgang


_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Mi Jun 20 2012 - 17:31:29 CEST

This archive was generated by hypermail 2.3.0 : Do Feb 01 2024 - 07:15:11 CET