Typeclasses (via meta arguments)

(Page under construction)

Meta-F* introduced a new way of doing implicit argument resolution to F*, which we used to implement typeclases. We describe the user view of typeclasses first, and then go into details about how they work.

Quick Intro and Cheatsheet

Declaring a class:

class deq a = {
  eq    : a -> a -> bool;
  eq_ok : (x : a) -> (y : a) -> Lemma (eq x y <==> x == y)
}

Concrete instances:

instance deq_int  : deq int  = {eq = (fun x y -> x = y); eq_ok = (fun _ _ -> ())}
instance deq_bool : deq bool = {eq = (fun x y -> x = y); eq_ok = (fun _ _ -> ())}
(* both proofs left to SMT, they look the same since both are eqtypes *)

type abc = | A | B | C
let eq_abc x y = match x, y with
                 | A, A | B, B | C, C -> true
                 | _ -> false

let eq_abc_ok (x y : abc) : Lemma (eq_abc x y <==> x == y) = ()

(* no need to give a name *)
instance _ : deq abc = { eq = eq_abc; eq_ok = eq_abc_ok }

A parametric instance

Typeclasses

There two new keywords: class and instance. To declare a class, which must be defined as record types, we simply use class instead of type:

class inhabited a = { witness : a }
class deq a = {
  eq : a -> a -> Tot bool;
  eq_ok : x:a -> y:a -> Lemma (__fname__eq x y <==> x == y) (* __fname__ due to #1184, should remove *)
}

(If you need to have typeclass resolution for something that is not a record, that's possible, read the next section.)

From here onwards, the types inhabited and deq are defined and can be used as usual. Beyond that, we get the methods witness, eq, and eq_ok, which are properly overloaded. Now we can write:

let eqList (#a:Type) (_ : deq a) (l1 l2 : list a) : bool =

How it's made