-
Notifications
You must be signed in to change notification settings - Fork 232
Typeclasses (via meta arguments)
Guido Martínez edited this page Aug 31, 2018
·
4 revisions
(Page in construction)
Meta-F* introduced a new way of doing implicit argument resolution to F*, which we used to implement to typeclases. We describe the user view of typeclasses first, and then go into details about how they work.
Declaring a class:
class deq a = {
eq : a -> a -> bool
eq_ok : (x y : a) -> Lemma (eq x y <==> x == y)
}
Concrete instances:
instance deq_int : deq int = { eq x y = (fun x y -> x = y); eq_ok = fun _ _ -> () }
instance deq_bool : deq bool = { eq x y = (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) = () // GG! check if this works
(* no need to give a name *)
instance _ : deq abc = { eq = eq_abc; eq_ok = eq_abc_ok }
A parametric instance
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 =