Search code examples
functional-programmingisabellehol

Type Unification failed for bool * bool ⇒ bool * bool

I wrote a simple function which should perform the function of a halfadder.

fun halfadder :: "bool * bool ⇒ bool * bool"
where
  "halfadder (a,b) = (
     let s = xor a b in
     let cout = and a b in
     (cout,s))"

However, I get the following error:

Type unification failed: No type arity bool :: semiring_bit_operations

Type error in application: incompatible operand type

Operator:  xor :: ??'a ⇒ ??'a ⇒ ??'a
Operand:   a :: bool

Why is it not able to perform a XOR operation on a bool? What is going wrong here?

I have tried using the XOR operator with different data types and it still faces the same error

Solution

  • The type bool in Isabelle/HOL is the type for logical formulas (of the object logic HOL) and so not intended to be used as a type for bit datas. For example, a diagnosis

    term "P ∧ Q"

    gives

    "P ∧ Q"
  :: "bool"

    If you jump to the definition of xor, you find that xor is defined for (or fixed for or being a method of) the class semiring_bit_operations. A possible solution is to define your halfadder inside the context of semiring_bit_operations, e.g.

    context semiring_bit_operations
begin
fun halfadder :: "'a * 'a ⇒ 'a * 'a"
where
  "halfadder (a, b) = (
     let s = xor a b in
     let cout = and a b in
     (cout,s))"
end

    which worked for me.

    However, semiring_bit_operations is not a class for one bits but bit sequences. Thus, it's better to define your own boolean datatype, and and xor (or use some built-in type if any (which I don't know)).

    (Note: I'm a beginner of Isabelle and so it is probably better to wait for more comprehensive answers from specialists.)