CODEWITHSUNDEEP
genericstypesisabelleunification
TKler
TKler

Reputation: 135

Isabelle: generic datatypes and equivalence

I'm just starting making my type generic in Isabelle now i get funny error messages once i start using parenthesis.

theory Scratch
imports Main
begin
no_notation plus (infixl "+" 65)

datatype typeA = aa
datatype typeB = bb
datatype ('a, 'b) genericType = cc | 
                                plus 'a 'b (infixr "+" 35)

lemma test1 : "x + y ≡ x + y"
by auto
lemma test2 : "x + y + z ≡ x + y + z"
by auto
lemma test3 : "x + (y + z) ≡ x + y + z"
by auto
lemma test4 : "(x + y) + z ≡ x + y + z"
lemma test5 : "(aa + aa) + aa ≡ aa + aa + aa"
lemma test6 : "(cc + cc) + cc ≡ cc + cc + cc"
lemma test7 : "(cc + aa) + cc ≡ cc + aa + cc"
lemma test8 : "(aa + cc) + cc ≡ cc + aa + cc"

Everything is fine with test1-3, but test 4 and 5 result in this error: 

Type unification failed: Occurs check!

Type error in application: incompatible operand type

Operator:  op ≡ ((x + y) + z) :: ((??'a, ??'b) genericType, ??'c) genericType ⇒ prop
Operand:   x + y + z :: (??'a, (??'b, ??'c) genericType) genericType

and respectivly:

Type unification failed: Clash of types "typeA" and "(_, _) genericType"

Type error in application: incompatible operand type

Operator:  op ≡ ((aa + aa) + aa) :: ((typeA, typeA) genericType, typeA) genericType ⇒ prop
Operand:   aa + aa + aa :: (typeA, (typeA, typeA) genericType) genericType

test6 and weirdly test7/8 are fine again. Any more replacement of "cc" with "aa" leads to the same problem though.

PS: can i somehow specifiy the types 'a and 'b?

Upvotes: 1

Views: 263

Answers (1)

Manuel Eberl
Manuel Eberl

Reputation: 8268

Two types in Isabelle are only equal when they really are syntactically equal. An equation where the left-hand side and the right-hand side have different types is not well-typed and will lead to an error message.

You defined + to be right-associative, so x + y + z is just an abbreviation for x + (y + z). The lemmas test1 to test3 are therefore trivially true, since the two sides of the equation are syntactically equal terms.

In test4 and test5, the left-hand sides have type ((_,_) genericType, _) genericType. The right-hand sides, on the other hand, have type (_, (_,_) genericType) genericType.

To illustrate it a bit better, I will write + for genericType in infix: the left-hand sides have type (_ + _) + _; the right-hand sides have _ + (_ + _). These two types are not syntactically equal and therefore different types. They are obviously isomorphic, but still different.

The fact that test6 to test8 are type-correct has to do with polymorphism: cc is polymorphic with schematic type variables 'a and 'b that can be instantiated to anything, and, importantly, if cc occurs in a term several times, the type variables can be instantiated to different types in every occurrence. This is not possible with variables like x, y, and z from the earlier examples.

Note, however, that while test6 to test8 can be type-checked, they are quite obviously false, as QuickCheck will tell you.

As for specifying the type variables: You can annotate terms with types, e.g. x + y :: (typeA, typeB) genericType or (x :: typeA) + (y :: typeB).

Upvotes: 1

Related Questions