Skip to content


A trait is a special type of record that can be used to define a set of functions that must be implemented for a given type. Traits are declared using the trait keyword.

<record type declaration>

The syntax of a record type declaration is as follows:

type <name> <type-parameters> :=
    <constructor> {
       <field1> : <type1>;
       <fieldn> : <typen>

For example, the following defines a trait Show. Any type A that implements Show must provide a function show that takes an A and returns a String.

type Show A := mkShow {show : A → String};

Instance declarations

An instance of a trait refers to a term of the corresponding record type, which must implement all methods stipulated by the trait.

To declare a given term is an instance of a trait, we use the instance keyword. To define an instance of a trait, we use the trait constructor of the corresponding record type.

<term> : {{<trait>}} := <trait constructor> (
    field1 := <term1>;
    fieldn := <termn>;

For example, we could define three instances of Show for String, Bool, and Nat as follows:

showStringI : Show String := mkShow (show := id);

showBoolI : Show Bool :=
  mkShow (show := λ {x := if x "true" "false"});

showNatI : Show Nat := mkShow (show := natToString);

One more involved example is the following, which defines an instance of Show for the type of lists:

showListI {A} {{Show A}} : Show (List A) :=
    showList {A} : {{Show A}} → List A → String
      | nil := "nil"
      | (h :: t) := h ++str " :: " ++str showList t;
  in mkShow (show := showList);

Using traits

Using the Show trait defined above, we can define a function showNat that takes a Nat and returns a String. One possible implementation is the following:

type Box A := box A;

type T A := mkT {pp : A → A};

ppBox {A} {{T A}} : Box A → Box A
  | (box x) := box (T.pp x);

boxT {A} {{T A}} : T (Box A) := mkT (pp := ppBox);

To prevent looping during instance search, we ensure a structural decrease in the trait parameters of instance types. Therefore, the following is rejected:

type Box A := box A;

type T A := mkT { pp : A → A };

boxT {A} : {{T (Box A)}} → T (Box A) := mkT (λ{x := x});

We check whether each parameter is a strict subterm of some trait parameter in the target. This ordering is included in the finite multiset extension of the subterm ordering, hence terminating.

  • Matching on implicit instances

It is possible to manually provide an instance and to match on implicit instances, as shown below:

f' {A} : {{Show A}} → A → String
  | {{mkShow s}} x := s x;

f'' {A} : {{Show A}} → A → String
  | {{M}} x := {{M}} x;

Finally, using the Show trait and the function printStringLn and IO from the standard library, we could use the instances of Show as follows:

main : IO :=
  printStringLn ( true)
    >> printStringLn (f false)
    >> printStringLn ( 3)
    >> printStringLn ( [true; false])
    >> printStringLn ( [1; 2; 3])
    >> printStringLn (f' [1; 2])
    >> printStringLn (f'' [true; false])
    >> printStringLn ( ["a"; "b"; "c"; "d"]);