In IceDust an expression has multiple orthogonal properties: type, multiplicity + ordering, calculation strategy, non-zero-ness.
These are encoded in a type-tuple in the current implementation, as expression only have a type:

  [[ Equal(e1, e2) ^ (s) : TTuple(TBoolean(), out_mult, out_ord) ]] :=
    [[ e1 ^ (s) : TTuple(e1_type, e1_mult, e1_ord) ]],
    [[ e2 ^ (s) : TTuple(e2_type, e2_mult, e2_ord) ]],
    out_type is sub.lub of (e1_type,e2_type),
    out_type <test? IsType(), // make sure it evaluates to something
    (out_mult, out_ord) is mulOrd.lub of ((e1_mult,e1_ord),(e2_mult,e2_ord)),
    e1_mult_u is multUpper of e1_mult,
    e1_mult_u == TUOne() | error $[Multiplicity mismatch: expected One or ZeroOrOne got [e1_mult]] @ e1,
    e2_mult_u is multUpper of e2_mult,
    e2_mult_u == TUOne() | error $[Multiplicity mismatch: expected One or ZeroOrOne got [e2_mult]] @ e2.

As the type rules have to deal with all the properties at the same time, they become hard to read.

I suggest we allow other properties as well on expressions.

  [[ Equal(e1, e2) ^ (s) : TBoolean() ]] :=
    [[ e1 ^ (s) : e1_type ]],
    [[ e2 ^ (s) : e2_type) ]],
    out_type is sub.lub of (e1_type,e2_type),
    out_type <test? IsType(). // make sure it evaluates to something

  [[ Equal(e1, e2) ^ (s).mult == (out_mult, out_ord) ]] :=
    [[ e1 ^ (s).mult == (e1_mult, e1_ord) ]],
    [[ e2 ^ (s).mult == (e2_mult, e2_ord) ]],
    (out_mult, out_ord) is mulOrd.lub of ((e1_mult,e1_ord),(e2_mult,e2_ord)),
    e1_mult_u is multUpper of e1_mult,
    e1_mult_u == TUOne() | error $[Multiplicity mismatch: expected One or ZeroOrOne got [e1_mult]] @ e1,
    e2_mult_u is multUpper of e2_mult,
    e2_mult_u == TUOne() | error $[Multiplicity mismatch: expected One or ZeroOrOne got [e2_mult]] @ e2.

In this example, type and mult+ord are completely orthogonal, but they are not always.

Lets say that we would require the types of the sub expressions in calculating the multiplicity+ordering.

Then we cannot use [[e1^(s):t]] syntax for it, as [[ ]] means collection, and the constraints for the type of the sub-expression would be collected twice.

Submitted by Daco Harkes on 19 January 2017 at 14:56