Arith type class requiring more than just a base type

[weaversa]

Why is Arith e not sufficient? This causes problems...

mmult : {a, b, c, e} (fin (a+b+c), Arith e) => [a][b]e -> [b][c]e -> [a][c]e
mmult x y = [ sum (transpose [ col * row | col <- transpose y ]) | row <- x ]

sum xs = sums!0
  where sums = [zero] # [ x + s | x <- xs | s <- sums ]

The following works, though Arith e isn't even required, but Arith ([b]e) and Arith ([c]e) are!

mmult : {a, b, c, e} (fin (a+b+c), Arith ([b]e), Arith ([c]e)) => [a][b]e -> [b][c]e -> [a][c]e
mmult x y = [ sum (transpose [ col * row | col <- transpose y ]) | row <- x ]

sum xs = sums!0
  where sums = [zero] # [ x + s | x <- xs | s <- sums ]

[brianhuffman]

Here is a minimal example that gives a similar type error:

sum' : {b, c, e} (fin b, fin c, Arith e) => [b][c]e -> [c]e
sum' y = sum y

sum xs = sums!0
  where sums = [zero] # [ x + s | x <- xs | s <- sums ]

And an even more minimal one:

neg' : {n, a} (fin n, Arith a) => [n]a -> [n]a
neg' xs = negate xs

[yav]

The behavior of Arith on sequences depends on the type of the elements of the sequence. For example, if the elements are of type Bit then (+) works one way, and if it is something else, then it works in a different way. The constraint is not being discharged because Cryptol does not know if the lements (i.e., e) will be Bit or something else.

Now, you could argue that since we have an Arith e constraint, and we know that there is no instance for Arith Bit, then we should be able to conclude that e can't possibly be Bit. At present we don't do any such fancy negative information reasoning, and I am not sure if it would be a good idea to do it, or how hard it might it be to implement.

[brianhuffman]

No negative information reasoning is necessary here. We just need to be able to derive Arith ([n]e) from Arith e, which should be trivial. What's the problem?

[brianhuffman]

From the perspective of improving/simplifying constraints on inferred types, I understand why Arith ([n]e) can't be reduced to Arith e. But when checking a user-supplied type signature, it should always be possible to derive Arith ([n]e) from Arith e.

[yav]

The current set of instances are like this:

 instance (fin n) => Arith ([n]Bit) where ...
 instance (fin n, Arith e, a /= Bit) => Arith ([n]e) where ...

Note that we don't have a rule that says Arith e => Arith ([n] e), at least not directly. Now since Arith is essentially a closed class, it is indeed the case that Arith e => a /=Bit and the rule you suggest is valid, but we don't have it. By the way, this would not be a valid inference if we did decide to add Arith Bit.

Also, currently the solver works backward, form the goal to the assumptions, and tries to simplify the goal to known assumptions. Now, of course we could try to do some forward reasoning too (i.e., start from the assumptions and try to reach a goal), but I am not sure how to guide it. When it is just a single step reasoning (as it is in this case), the derivation is obvious, but I am not sure how to guide it beyond that.

I anticipate that this is doable, if we are sure that we never want to add Arith Bit, but just requires some thinking.

[brianhuffman]

Wow, that a /= Bit thing is weird. Anyway, I think you meant to type:

instance (Arith a, a /= Bit) => Arith ([n]a) where ...

I.e. e and a should be the same variable, and fin n should not be necessary (otherwise we would not have Arith [inf][8], for example).

[weaversa]

After a long discussion with @brianhuffman, we decided Arith Bit just can't be.

The reasoning is that arithmetic operators work over arbitrary structures of sequences of bits. For example, + works on sequences of bits:

Cryptol> 5 + 1 == 6

and sequences of sequences of bits:

Cryptol> [1, 0, 1] + [0, 0, 1] == [1, 0, 2]

Allowing statements like True + False == True would be problematic because it creates, in a sense, another base type for the iteration of + over structures of sequences of bits (Bit itself). For example, if Arith Bit was possible, then one may expect that the + operation would iterate over sequences of bits pairwise, that is:

Cryptol> [True, False, True] + [False, False, True] == [True, False, False] 
which can also be written as
Cryptol> 0b101 + 0b001 == 0b100
or as
Cryptol> 5 + 1 == 4

[robdockins]

Would it break anything to pretend like we have the following overlapping instances, and just prefer the more specific [n]Bit instance when it applies?

instance (Arith a) => Arith ([n]a)
instance Arith [n]Bit

[yav]

I don't think we can do much about this for the time being, so I'll close it. If one day a good idea comes up, maybe we can revisit this issue.