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.

Syntax of Traits

Trait declarations

Traits are declared using the trait keyword, followed by a record type declaration.

type <record name> <type parameters> :=
    | <type-constructor1> {
        <field1-1> : <type-1-1>;
        <field1-n> : <type-1-n>
    | ...
    | <type-constructor-n> {
        <fieldn-1> : <type-n-1>;
        <fieldn-n> : <type-n-n>

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.

Syntax of instance declarations

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 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:

module usage-example;
  type Nat :=
    | Z
    | S Nat;

  type Show A := mkShow {show : A  String};
  NatToString : Nat -> String
    | Z := "Z"
    | (S n) := "S " ++str NatToString n;

  showNat : Show Nat := mkShow (show := NatToString);

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};

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
  | x := x;

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"]);