Coercion

Sometimes it is convenient to interpret elements of type A as elements of type B and use elements of A in places, where elements of B are expected. For example, natural numbers are also integer numbers, integer numbers are also rational numbers, and so on. There is a mechanism, which allows this by marking a function f from A to B as a coercing function. Once f : A -> B is declared as a coercing function, whenever an expression a : A is used in a place, where type B is expected, a will be automatically replaced with f a : B.

A coercing function can be defined either for a \data or a \class definition. It should be written inside the \where block for this definition and it should begin with \use \coerce instead of \func. For example, Bool can be coerced to Nat as follows:

\data Bool | true | false
  \where
    \use \coerce toNat (b : Bool) : Nat
      | true => 1
      | false => 0

It is possible to coerce a given definition either from or to other definition. A function, which coerces from a given definition, must have this definition as the type of its last parameter. A function, which coerces to a given definition, must have this definition as its result type. For example, Nat can be coerced to Bool as follows:

\data Bool | true | false
  \where
    \use \coerce fromNat (n : Nat) : Bool
      | 0 => false
      | 1 => true
      | suc (suc n) => fromNat n

It is possible to define several coercing functions for a single type.

If some data type or record can be coerced to a function, then elements of this type can be applied to arguments, in which case the coercing function will be inserted.

Fields and constructors

A field or a constructor can be marked with the \coerce keyword like this:

\record R (\coerce A : \Type) (a : A)
\data D | \coerce con1 Nat | con2

Then the marked field or constructor will be used just as coercing functions.