Subtraction(x, y) : y-ty
	where x : x-ty
		and y : y-ty
		and (x-ty == Int() else error $[Type mismatch: expected Int got [x-ty] in Math Operation] on x)
		and (y-ty == Int() else error $[Type mismatch: expected Int got [y-ty] in Math Operation] on y)

Generates

create-type-task(|ctx) :
    Subtraction(x, y) -> <task-create-id(|ctx,[eq1152])> y-ty
    where 
      x-ty := <type-task(|ctx)> x;
      y-ty := <type-task(|ctx); task-create-id(|ctx, [x-ty])> y;
      eq1151 := <type-match(|ctx, Int()); task-create-id(|ctx, [y-ty])> x-ty;
      <task-create-error-on-failure(|ctx, eq1151, ["Type mismatch: expected Int got ", x-ty, " in Math Operation"])> x;
      eq1152 := <type-match(|ctx, Int()); task-create-id(|ctx, [eq1151])> y-ty;
      <task-create-error-on-failure(|ctx, eq1152, ["Type mismatch: expected Int got ", y-ty, " in Math Operation"])> y

This means that "a" - 4 will give two errors

• Type mismatch: expected Int got String in Math Operation
  • Type mismatch: expected Int got Int in Math Operation

The second error is there because eq1152 depends on eq1151.

Note that in the case of "a" - "b" one would actually want two errors.

Since we defined that and generates a dependency between the left expression and the right expression I am not really sure how we should approach this new situation.

Submitted by Daco Harkes on 19 March 2014 at 13:24

I’m also encountering this issue.

The task dependency chain that results from the above code is:

y-ty -> x-ty
eq1151 -> y-ty
eq1152 -> eq1151

As you see, the parentheses are not taken into account. Leaving out the parentheses would result in the same dependencies.

To solve this, I think an ‘and’-task must be introduced (similar to how there is an ‘or’-task task-create-choice). Then the dependency chain would become:

eq1151 -> x-ty
eq1152 -> y-ty
and1 -> [eq1151, eq1152]

Since task-create-error-on-failure succeeds when its dependency fails, I think this would result in the correct behavior.

Proposed solution: dependencies stay within brackets

Suggestion to fix this: do not depend on things outside brackets.

Code without brackets, triggering wrong errors:

Subtraction(x, y) : y-ty
  where x : x-ty
	and y : y-ty
	and x-ty == Int() else error $[Type mismatch: expected Int got [x-ty] in Math Operation] on x
	and y-ty == Int() else error $[Type mismatch: expected Int got [y-ty] in Math Operation] on y

Code with brackets, triggering correct errors:

Subtraction(x, y) : y-ty
  where x : x-ty
	and y : y-ty
	(and x-ty == Int() else error $[Type mismatch: expected Int got [x-ty] in Math Operation] on x)
	(and y-ty == Int() else error $[Type mismatch: expected Int got [y-ty] in Math Operation] on y)

Of course the rules inside the brackets would still depend on all the names they use, but not on all the rules in before.

Other syntactic or non-syntactic suggestions for proper task-dependencies?

Parentheses should only be used for syntactic disambiguation.

A proper solution is better dependency analysis.

What would that better dependency analysis look like?
Currently an and always lets the right side depend on the left.
Dropping these dependencies is also not a solution, then the and will fail.

This is an error-message only issue, a type rule just computes a single type which should fail if any and fails.
So different dependencies are required for the actual rule result and the error messages.

I guess letting error messages only depend on the thing right before the else would be too restrictive (it solves most of the use cases though, because if there are multiple failure conditions you usually want to give specific error messages for each).
And it would mean there would be separate task-dependencies and message-dependencies.

I guess that the following should give the error messages that we’d expect:

create-type-task(|ctx) :
Subtraction(x, y) -> <task-create-id(|ctx,[eq1151, eq1152])> y-ty
where
x-ty := <type-task(|ctx)> x;
y-ty := <type-task(|ctx); task-create-id(|ctx, [x-ty])> y;
eq1151 := <type-match(|ctx, Int()); task-create-id(|ctx, [])> x-ty;
<task-create-error-on-failure(|ctx, eq1151, ["Type mismatch: expected Int got “, x-ty, " in Math Operation”])> x;
eq1152 := <type-match(|ctx, Int()); task-create-id(|ctx, [])> y-ty;
<task-create-error-on-failure(|ctx, eq1152, ["Type mismatch: expected Int got “, y-ty, " in Math Operation”])> y

Yes.

Lets see what the patterns for different more complex rules will be

Addition(x, y) : y-ty
where x : x-ty
	and y : y-ty
	and (x-ty == Int() or x-ty == String()) else error  $[Type mismatch: expected Int or String got [x-ty] in Addition] on x
	and x-ty == y-ty else error $[Type mismatch: expected [x-ty] got [y-ty] in Addition] on y

translates to

  create-type-task(|ctx) :
    Addition(x, y) -> <task-create-id(|ctx,[eq4589])> y-ty
    where 
      x-ty := <type-task(|ctx)> x;
      y-ty := <type-task(|ctx); task-create-id(|ctx, [x-ty])> y;
      eq4587 := <type-match(|ctx, Int()); task-create-id(|ctx, [y-ty])> x-ty;
      eq4588 := <type-match(|ctx, String()); task-create-id(|ctx, [y-ty])> x-ty;
      or2204 := <type-is(|ctx)> <task-create-choice(|ctx)> [eq4587, eq4588];
      <task-create-error-on-failure(|ctx, or2204, ["Type mismatch: expected Int or String got ", x-ty, " in Addition"])> x;
      eq4589 := <type-match(|ctx, y-ty); task-create-id(|ctx, [or2204])> x-ty;
      <task-create-error-on-failure(|ctx, eq4589, ["Type mismatch: expected ", x-ty, " got ", y-ty, " in Addition"])> y

but not same solution:
(removing the dependencies in or2204 would break the behaviour)

  create-type-task(|ctx) :
    Addition(x, y) -> <task-create-id(|ctx,[or2204, eq4589])> y-ty
    where 
      x-ty := <type-task(|ctx)> x;
      y-ty := <type-task(|ctx); task-create-id(|ctx, [x-ty])> y;
      eq4587 := <type-match(|ctx, Int()); task-create-id(|ctx, [y-ty])> x-ty;
      eq4588 := <type-match(|ctx, String()); task-create-id(|ctx, [y-ty])> x-ty;
      or2204 := <type-is(|ctx)> <task-create-choice(|ctx)> [eq4587, eq4588];
      <task-create-error-on-failure(|ctx, or2204, ["Type mismatch: expected Int or String got ", x-ty, " in Addition"])> x;
      eq4589 := <type-match(|ctx, y-ty); task-create-id(|ctx, [])> x-ty;
      <task-create-error-on-failure(|ctx, eq4589, ["Type mismatch: expected ", x-ty, " got ", y-ty, " in Addition"])> y

I guess the pattern is:

• don’t pass dependencies over error tasks
• add the dependencies that would have been passed over error tasks to the top level task

A task should depend on all tasks that create input for it (basically task variables it depends on)

The final task in the rhs should depend on the tips of each dependency branch.

By accident stumbled on a work around, define two separate rules:

  Attribute(a, a-ty, a-mu, Derivation(e, derivationType)) :-
  where e : e-ty
    and e-ty == a-ty else error 
      $[Type mismatch: expected [a-ty] got [e-ty] in Derivation] on e
      
  Attribute(a, a-ty, a-mu, Derivation(e, derivationType)) :-
  where e has multiplicity e-mu
    and (
            a-mu == ZeroOrOne() and e-mu == One()
         or a-mu == e-mu
        )
    else error 
      $[Multiplicity mismatch: expected [a-mu] got [e-mu] in Derivation] on e

For rules with a type result it would be something like:

Subtraction(x, y) : y-ty
  where x : x-ty
    and y : y-ty
    and x-ty == Int()
    and y-ty == Int()

Subtraction(x, y) :-
  where x-ty == Int() else error $[Type mismatch: expected Int got [x-ty] in Math Operation] on x

Subtraction(x, y) :-
  where y-ty == Int() else error $[Type mismatch: expected Int got [y-ty] in Math Operation] on y

I’m not sure if the type-rule will still work then though.

Interesting finding, @Daco. This might be a compilation scheme.

How did the original rule look like for the first example?

In the second example, the last two rules miss the calcuation for x-ty and y-ty, but those can easily be added. It does not even duplicate the calculation because the task is the same, but has a small overhead in the collection.

This rule

  Multiplication(x, y)
+  Division(x, y)
+  Modulo(x, y)
+  Subtraction(x, y) : y-ty
  where  x  : x-ty
    and  y  : y-ty
    and  x-ty == Int() else error $[Type mismatch: expected Int got [x-ty] in Math Operation] on x
    and  y-ty == Int() else error $[Type mismatch: expected Int got [y-ty] in Math Operation] on y

Should have the behaviour of

  Multiplication(x, y)
+ Division(x, y)
+ Modulo(x, y)
+ Subtraction(x, y) : y-ty
  where  x  : x-ty
    and  y  : y-ty
    and  x-ty == Int()
    and  y-ty == Int()
    
  Multiplication(x, y)
+ Division(x, y)
+ Modulo(x, y)
+ Subtraction(x, y) :-
  where  x  : x-ty
    and  x-ty == Int() else error $[Type mismatch: expected Int got [x-ty] in Math Operation] on x
    
  Multiplication(x, y)
+ Division(x, y)
+ Modulo(x, y)
+ Subtraction(x, y) :-
  where  y  : y-ty
    and  y-ty == Int() else error $[Type mismatch: expected Int got [y-ty] in Math Operation] on y

Which indeed removes all error messages of the first rule and gives all the error message rules only the calculations/dependencies it really needs.