Typeclasses

Consider writing a program using bounded unsigned integers while being generic in the actual bounded integer type, E.g., a function that sums a list of bounded integers while checking for overflow, applicable to both UInt32 and UInt64. Since F*’s interfaces are not first-class, one can’t easily write a program that abstracts over those interfaces. Typeclasses can help.

Some background reading on typeclasses:

  • Phil Wadler and Stephen Blott introduced the idea in 1989 in a paper titled “How to make ad hoc polymorphism less ad hoc.” Their work, with many extensions over the years, is the basis of Haskell’s typeclasses.

  • A tutorial on typeclasses in the Coq proof assistant is available here.

  • Typeclasses are used heavily in the Lean proof assistant to structure its math library.

Printable

A typeclass associates a set of methods to a tuple of types, corresponding to the operations that can be performed using those types.

For instance, some types may support an operation that enables them to be printed as strings. A typeclass printable (a:Type) represent the class of all types that support a to_string : a -> string operation.

class printable (a:Type) =
{
  to_string : a -> string
}

The keyword class introduces a new typeclass, defined as a record type with each method represented as a field of the record.

To define instances of a typeclass, one uses the instance keyword, as shown below.

instance printable_bool : printable bool =
{
  to_string = Prims.string_of_bool
}

instance printable_int : printable int =
{
  to_string = Prims.string_of_int
}

The notation instance printable_bool : printable bool = e states that the value e is a record value of type printable bool, and just as with a let-binding, the term e is bound to the top-level name printable_bool.

The convenience of typeclasses is that having defined a class, the typeclass method is automatically overloaded for all instances of the class, and the type inference algorithm finds the suitable instance to use. This is the original motivation of typeclasses—to provide a principled approach to operator overloading.

For instance, we can now write printb and printi and use to_string to print both booleans and integers, since we shown that they are instances of the class printable.

let printb (x:bool) = to_string x
let printi (x:int) = to_string x

Instances need not be only for base types. For example, all lists are printable so long as their elements are, and this is captured by what follows.

instance printable_list (#a:Type) (x:printable a) : printable (list a) =
{
  to_string = (fun l -> "[" ^ FStar.String.concat "; " (List.Tot.map to_string l) ^ "]")
}

That is, printable_list constructs a to_string method of type list a -> string by mapping the to_string method of the printable a instance over the list. And now we can use to_string with lists of booleans and integers too.

let printis (l:list int) = to_string l
let printbs (l:list bool) = to_string l

There’s nothing particularly specific about the ground instances printable bool and printable int. It’s possible to write programs that are polymorphic in printable types. For example, here’s a function print_any_list that is explicitly parameterized by a printable a—one can call it by passing in the instance that one wishes to use explicitly:

let print_any_list_explicit #a ( _ : printable a ) (l:list a) = to_string l
let _ = print_any_list_explicit printable_int [1;2;3]

However, we can do better and have the compiler figure out which instance we intend to use by using a bit of special syntax for a typeclass parameter, as shown below.

let print_any_list #a {| _ : printable a |} (l:list a) = to_string l
let _ex1 = print_any_list [[1;2;3]]
let _ex2 = print_any_list #_ #(printable_list printable_int) [[1;2;3]]

The parameter {| _ : printable a |} indicates an implicit argument that, at each call site, is to be computed by the compiler by finding a suitable typeclass instance derivable from the instances in scope. In the first example above, F* figures out that the instance needed is printable_list printable_int : printable (list int). Note, you can always pass the typeclass instance you want explicitly, if you really want to, as the second example _ex2 above shows.

In many cases, the implicit typeclass argument need not be named, in which case one can just omit the name and write:

let print_any_list_alt #a {| printable a |} (l:list a) = to_string l

Under the hood

When defining a class, F* automatically generates generic functions corresponding to the methods of the class. For instance, in the case of printable, F* generates:

let to_string #a {| i : printable a |} (x:a) = i.to_string x

Having this in scope overloads to_string for all instance of the printable class. In the implementation of to_string, we use the instance i (just a record, sometimes called a dictionary in the typeclass literature) and project its to_string field and apply it to x.

Defining an instance p x1..xn : t = e is just like an ordinary let binding let p x1..xn : t = e, however the instance keyword instructs F*’s type inference algorithm to consider using p when trying to instantiate implicit arguments for typeclass instances.

For example, at the call site to_string (x:bool), having unified the implicit type arguments a with bool, what remains is to find an instance of printable bool. F* looks through the current context for all variable bindings in the local scope, and instance declarations in the top-level scope, for a instance of printable bool, taking the first one it is able to construct.

The resolution procedure for to_string [[1;2;3]] is a bit more interesting, since we need to find an instance printable (list int), although no such ground instance exists. However, the typeclass resolution procedure finds the printable_list instance function, whose result type printable (list a) matches the goal printable (list int), provided a = int. The resolution procedure then spawns a sub-goal printable int, which it solves easily and completes the derivation of printable (list int).

This backwards, goal-directed search for typeclass resolution is a kind of logic programming. An interesting implementation detail is that most of the typeclass machinery is defined as a metaprogran in FStar.Tactics.Typeclasses, outside of the core of F*’s compiler. As such, the behavior of typeclass resolution is entirely user-customizable, simply by revising the metaprogram in use. Some details about how this works can be found in a paper on Meta F*.

Exercises

Define instances of printable for string, a & b, option a, and either a b. Check that you can write to_string [Inl (0, 1); Inr (Inl (Some true)); Inr (Inr "hello") ] and have F* infer the typeclass instance needed.

Also write the typeclass instances you need explicitly, just to check that you understand how things work. This is exercise should also convey that typeclasses do not increase the expressive power in any way—whatever is expressible with typeclasses, is also expressible by explicitly passing records that contain the operations needed on specific type parameters. However, expliciting passing this operations can quickly become overwhelming—typeclass inference keeps this complexity in check and makes it possible to build programs in an generic, abstract style without too much pain.

This exercise file provides the definitions you need.

Answer

instance printable_string : printable string =
{
  to_string = fun x -> "\"" ^ x ^ "\""
}

instance printable_pair #a #b {| printable a |} {| printable b |} : printable (a & b) =
{
  to_string = (fun (x, y) -> "(" ^ to_string x ^ ", " ^ to_string y ^ ")")
}

instance printable_option #a {| printable a |} : printable (option a) =
{
  to_string = (function None -> "None" | Some x -> "(Some " ^ to_string x ^ ")")
}

instance printable_either #a #b {| printable a |} {| printable b |} : printable (either a b) =
{
  to_string = (function Inl x -> "(Inl " ^ to_string x ^ ")" | Inr x -> "(Inr " ^ to_string x ^ ")")
}

let _ = to_string [Inl (0, 1); Inr (Inl (Some true)); Inr (Inr "hello") ]

//You can always pass the typeclass instance you want explicitly, if you really want to
//typeclass resolution really saves you from LOT of typing!
let _ = to_string #_
             #(printable_list
                (printable_either #_ #_ #(printable_pair #_ #_ #printable_int #printable_int)
                                        #(printable_either #_ #_ #(printable_option #_ #printable_bool)
                                                                 #(printable_string))))
             [Inl (0, 1); Inr (Inl (Some true)); Inr (Inr "hello")]

Bounded Unsigned Integers

The printable typeclass is fairly standard and can be defined in almost any language that supports typeclasses. We now turn to a typeclass that leverages F*’s dependent types by generalizing the interface of bounded unsigned integers that we developed in a previous chapter.

A type a is in the class bounded_unsigned_int, when it admits:

  • An element bound : a, representing the maximum value

  • A pair of functions from_nat and to_nat that form a bijection between a and natural numbers less than to_nat bound

This is captured by the class below:

class bounded_unsigned_int (a:Type) = {
   bound      : a;
   as_nat     : a -> nat;
   from_nat   : (x:nat { x <= as_nat bound }) -> a;
   [@@@FStar.Tactics.Typeclasses.no_method]
   properties : squash (
     (forall (x:a). as_nat x <= as_nat bound) /\ // the bound is really an upper bound
     (forall (x:a). from_nat (as_nat x) == x) /\ //from_nat/as_nat form a bijection
     (forall (x:nat{ x <= as_nat bound}). as_nat (from_nat x) == x)
   )
}

Note

The attribute FStar.Tactics.Typeclasses.no_method on the properties field instructs F* to not generate a typeclass method for this field. This is useful here, since we don’t really want to overload the name properties as an operator over all instances bound the class. It’s often convenient to simply open FStar.Tactics.Typeclasses when using typeclasses, or to use a module abbreviation like module TC = FStar.Tactics.Typeclasses so that you don’t have to use a fully qualified name for no_method.

For all bounded_unsigned_ints, one can define a generic fits predicate, corresponding to the bounds check condition that we introduced in the UInt32 interface.

let fits #a {| bounded_unsigned_int a |}
            (op: int -> int -> int)
            (x y:a)
  : prop
  = 0 <= op (as_nat x) (as_nat y) /\
    op (as_nat x) (as_nat y) <= as_nat #a bound

Likewise, the predicate related_ops defines when an operation bop on bounded integers is equivalent to an operation iop on mathematical integers.

let related_ops #a {| bounded_unsigned_int a |}
                (iop: int -> int -> int)
                (bop: (x:a -> y:a { fits iop x y } -> a))
  = forall (x y:a).  fits iop x y ==> as_nat (bop x y) = as_nat x `iop` as_nat y

Typeclass Inheritance

Our bounded_unsigned_int a class just showed that a is in a bijection with natural numbers below some bound. Now, we can define a separate class, extending bounded_unsigned_int with the operations we want, like addition, subtraction, etc.

class bounded_unsigned_int_ops (a:Type) = {
   [@@@TC.no_method]
   base       : bounded_unsigned_int a;
   add        : (x:a -> y:a { fits ( + ) x y } -> a);
   sub        : (x:a -> y:a { fits op_Subtraction x y } -> a);
   lt         : (a -> a -> bool);
   [@@@TC.no_method]
   properties : squash (
     related_ops ( + ) add /\
     related_ops op_Subtraction sub /\      
     (forall (x y:a). lt x y <==> as_nat x < as_nat y) /\ // lt is related to <
     (forall (x:a). fits op_Subtraction bound x) //subtracting from the maximum element never triggers underflow
   )
}

The class above makes use of typeclass inheritance. The base field stores an instance of the base class bounded_unsigned_int, while the remaining fields extend it with:

  • add: a bounded addition operation

  • sub: a bounded subtraction operation

  • lt : a comparison function

  • properties, which show that

    • add is related to integer addition +

    • sub is related to integer subtraction -

    • lt is related to <

    • and that sub bound x is always safe

Typeclass inheritance in the form of additional fields like base is completely flexible, e.g., multiple inheritance is permissible (though, as we’ll see below, should be used with care, to prevent surprises).

Treating an instance of a class as an instance of one its base classes is easily coded as instance-generating function. The code below says that an instance from bounded_unsigned_int a can be derived from an instance of d : bounded_unsigned_int_ops a just by projecting its base field.

instance ops_base #a {| d : bounded_unsigned_int_ops a |} 
  : bounded_unsigned_int a
  = d.base

Infix Operators

F* does not allows the fields of a record to be named using infix operator symbols. This will likely change in the future. For now, to use custom operations with infix notation for typeclass methods, one has to define them by hand:

let ( +^ ) #a {| bounded_unsigned_int_ops a |}
           (x : a)
           (y : a { fits ( + ) x y })
  : a
  = add x y

let ( -^ ) #a {| bounded_unsigned_int_ops a |}
           (x : a)
           (y : a { fits op_Subtraction x y })
  : a
  = sub x y

let ( <^ ) #a {| bounded_unsigned_int_ops a |}
           (x : a)
           (y : a)
  : bool
  = lt x y

Derived Instances

We’ve already seen how typeclass inheritance allows a class to induce an instance of its base class(es). However, not all derived instances are due to explicit inheritance—some instances can be computed from others.

For example, here’s a class eq for types that support decidable equality.

class eq (a:Type) = {
  eq_op: a -> a -> bool;

  [@@@TC.no_method]
  properties : squash (
    forall x y. eq_op x y <==> x == y
  )
}

let ( =?= ) #a {| eq a |} (x y: a) = eq_op x y

We’ll write x =?= y for an equality comparison method from this class, to not confuse it with F*’s built-in decidable equality (=) on eqtype.

Now, from an instance of bounded_unsigned_int_ops a we can compute an instance of eq a, since we have <^, a strict comparison operator that we know is equivalent to < on natural numbers. F*, from all the properties we have on bounded_unsigned_int_ops and its base class bounded_unsigned_int, can automatically prove that not (x <^ y) && not (y <^ x) is valid if and only if x == y. This instance of eq now also lets us easily implement a non-strict comparison operation on bounded unsigned ints.

instance bounded_unsigned_int_ops_eq #a {| bounded_unsigned_int_ops a |}
  : eq a
  = {
      eq_op = (fun x y -> not (x <^ y) && not (y <^ x));
      properties = ()
    }

let ( <=^ ) #a {| bounded_unsigned_int_ops a |} (x y : a)
  : bool
  = x <^ y || x =?= y

Ground Instances

We can easily provide ground instances of bounded_unsigned_int_ops for all the F* bounded unsigned int types—we show instances for FStar.UInt32.t and FStar.UInt64.t, where the proof of all the properties needed to construct the instances is automated.

module U32 = FStar.UInt32
module U64 = FStar.UInt64
instance u32_instance_base : bounded_unsigned_int U32.t =
  let open U32 in
  {
    bound    = 0xfffffffful;
    as_nat   = v;
    from_nat = uint_to_t;
    properties = ()
}

instance u32_instance_ops : bounded_unsigned_int_ops U32.t =
  let open U32 in
  {
    base = u32_instance_base;
    add  = (fun x y -> add x y);
    sub  = (fun x y -> sub x y);
    lt   = (fun x y -> lt x y);
    properties = ()
  }


instance u64_instance_base : bounded_unsigned_int U64.t =
  let open U64 in
  {
    bound    = 0xffffffffffffffffuL;
    as_nat   = v;
    from_nat = uint_to_t;
    properties = ()
}

instance u64_instance_ops : bounded_unsigned_int_ops U64.t =
  let open U64 in
  {
    base = u64_instance_base;
    add  = (fun x y -> add x y);
    sub  = (fun x y -> sub x y);
    lt   = (fun x y -> lt x y);
    properties = ()
  }

And one can check that typeclass resolution works well on those ground instances.

let test32 (x:U32.t)
           (y:U32.t)
  = if x <=^ 0xffffffful &&
       y <=^ 0xffffffful
    then Some (x +^ y)
    else None

let test64 (x y:U64.t)
  = if x <=^ 0xfffffffuL &&
       y <=^ 0xfffffffuL
    then Some (x +^ y)
    else None

Finally, as promised at the start, we can write functions that are generic over all bounded unsigned integers, something we couldn’t do with interfaces alone.

module L = FStar.List.Tot
let sum #a {| bounded_unsigned_int_ops a |}
        (l:list a) (acc:a)
  : option a 
  = L.fold_right
     (fun (x:a) (acc:option a) ->
       match acc with
       | None -> None
       | Some y ->
         if x <=^ bound -^ y
         then Some (x +^ y)
         else None)
     l
     (Some acc)

let testsum32 : U32.t = Some?.v (sum [0x01ul; 0x02ul; 0x03ul] 0x00ul)
let testsum64 : U64.t = Some?.v (sum [0x01uL; 0x02uL; 0x03uL] 0x00uL)

F* can prove that the bounds check in sum is sufficient to prove that the addition does not overflow, and further, that the two tests return Some _ without failing due to overflow.

However, the proving that Some? (sum [0x01ul; 0x02ul; 0x03ul] 0x00ul) using the SMT solver alone can be expensive, since it requires repeated unfolding of the recursive function sum–such proofs are often more easily done using F*’s normalizer, as shown below—we saw the assert_norm construct in a previous section.

let testsum32' : U32.t =
  let x =
    sum #U32.t
        [0x01ul; 0x02ul; 0x03ul;
         0x01ul; 0x02ul; 0x03ul;
         0x01ul; 0x02ul; 0x03ul]
        0x00ul
  in
  assert_norm (Some? x /\ as_nat (Some?.v x) == 18);
  Some?.v x

Note

That said, by using dependently typed generic programming (which we saw a bit of earlier), it is possible to write programs that abstract over all machine integer types without using typeclasses. The F* library FStar.Integers shows how that works. Though, the typeclass approach shown here is more broadly applicable and extensible.

Dealing with Diamonds

One may be tempted to factor our bounded_unsigned_int_ops typeclass further, separating out each operation into a separate class. After all, it may be the case that some instances of bounded_unsigned_int types support only addition while others support only subtraction. However, when designing typeclass hierarchies one needs to be careful to not introduce coherence problems that result from various forms of multiple inheritance.

Here’s a typeclass that captures only the subtraction operation, inheriting from a base class.

class subtractable_bounded_unsigned_int (a:Type) = {
   [@@@no_method]
   base   : bounded_unsigned_int a;
   sub    : (x:a -> y:a { fits op_Subtraction x y } -> a);

   [@@@no_method]
   properties : squash (
     related_ops op_Subtraction sub /\
     (forall (x:a). fits op_Subtraction bound x)
   )
}

instance subtractable_base {| d : subtractable_bounded_unsigned_int 'a |} 
  : bounded_unsigned_int 'a 
  = d.base

And here’s another typeclass that provides only the comparison operation, also inheriting from the base class.

class comparable_bounded_unsigned_int (a:Type) = {
   [@@@no_method]
   base   : bounded_unsigned_int a;
   comp   : a -> a -> bool;

   [@@@no_method]
   properties : squash (
     (forall (x y:a).{:pattern comp x y} comp x y <==> as_nat x < as_nat y)
   )
}

instance comparable_base {| d : comparable_bounded_unsigned_int 'a |} 
  : bounded_unsigned_int 'a 
  = d.base

However, now when writing programs that expect both subtractable and comparable integers, we end up with a coherence problem.

The sub operation fails to verify, with F* complaining that it cannot prove fits op_Subtraction bound acc, i.e., this sub may underflow.

[@@expect_failure [19]]
let try_sub #a {| s: subtractable_bounded_unsigned_int a|}
               {| c: comparable_bounded_unsigned_int a |}
            (acc:a)
  = bound `sub` acc

At first, one may be surprised, since the s : subtractable_bounded_unsigned_int a instance tells us that subtracting from the bound is always safe. However, the term bound is an overloaded (nullary) operator and there are two ways to resolve it: s.base.bound or c.base.bound and these two choices are not equivalent. In particular, from s : subtractable_bounded_unsigned_int a, we only know that s.base.bound `sub` acc is safe, not that c.base.bound `sub` acc is safe.

Slicing type typeclass hierarchy too finely can lead to such coherence problems that can be hard to diagnose. It’s better to avoid them by construction, if at all possible. Alternatively, if such problems do arise, one can sometimes add additional preconditions to ensure that the multiple choices are actually equivalent. There are many ways to do this, ranging from indexing typeclasses by their base classes, to adding equality hypotheses—the equality hypothesis below is sufficient.

let try_sub {| s: subtractable_bounded_unsigned_int 'a |}
            {| c: comparable_bounded_unsigned_int 'a |}
            (acc:'a { s.base == c.base } )
  = bound `sub` acc

Overloading Monadic Syntax

We now look at some examples of typeclasses for type functions, in particular, typeclasses for functors and monads.

Note

If you’re not familiar with monads, referring back to A First Model of Computational Effects may help.

In a previous chapter, we introduced syntactic sugar for monadic computations. In particular, F*’s syntax supports the following:

  • Instead of writing bind f (fun x -> e) you can define a custom let!-operator and write let! x = f in e.

  • And, instead of writing bind f (fun _ -> e) you can write f ;! e.

Now, if we can overload the symbol bind to work with any monad, then the syntactic sugar described above would work for all of them. This is accomplished as follows.

We define a typeclass monad, with two methods return and ( let! ).

class monad (m:Type -> Type) =
{
   return : (#a:Type -> a -> m a);
   ( let! )  : (#a:Type -> #b:Type -> (f:m a) -> (g:(a -> m b)) -> m b);
}

Doing so introduces return and ( let! ) into scope at the following types:

let return #m {| d : monad m |} #a (x:a) : m a = d.return x
let ( let! ) #m {| d : monad m |} #a #b (f:m a) (g: a -> m b) : m b = d.bind f g

That is, we now have ( let! ) in scope at a type general enough to use with any monad instance.

Note

There is nothing specific about let!; F* allows you to add a suffix of operator characters to the let-token. See this file for more examples of monadic let operators

The type st s is a state monad parameterized by the state s, and st s is an instance of a monad.

let st (s:Type) (a:Type) = s -> a & s

instance st_monad s : monad (st s) =
{
   return = (fun #a (x:a) -> (fun s -> x, s));
   ( let! ) = (fun #a #b (f: st s a) (g: a -> st s b) (s0:s) ->
               let x, s1 = f s0 in
               g x s1);
}

With some basic actions get and put to read and write the state, we can implement st computations with a syntax similar to normal, direct-style code.

let get #s
  : st s s
  = fun s -> s, s

let put #s (x:s)
  : st s unit
  = fun _ -> (), x

let get_inc =
  let! x = get in
  return (x + 1)

Of course, we can also do proofs about our st computations: here’s a simple proof that get_put is noop.

let get_put #s =
  let! x = get #s in
  put x

let noop #s : st s unit = return ()

let get_put_identity (s:Type)
  : Lemma (get_put #s `FStar.FunctionalExtensionality.feq` noop #s)
  = ()

Now, the nice thing is that since ( let! ) is monad polymorphic, we can define other monad instances and still use the syntactic sugar to build computations in those monads. Here’s an example with the option monad, for computations that may fail.

instance opt_monad : monad option =
{
   return = (fun #a (x:a) -> Some x);
   ( let! ) = (fun #a #b (x:option a) (y: a -> option b) ->
             match x with
             | None -> None
             | Some a -> y a)
}

let raise #a : option a = None

let div (n m:int) =
  if m = 0 then raise
  else return (n / m)

let test_opt_monad (i j k:nat) =
  let! x = div i j in
  let! y = div i k in
  return (x + y)

Exercise

Define a typeclass for functors, type functions m: Type -> Type which support the operations fmap : (a -> b) -> m a -> m b.

Build instances of functor for a few basic types, e.g., list.

Derive an instance for functors from a monad, i.e., prove

instance monad_functor #m {| monad m |} : functor m = admit()

This file provides the definitions you need.

Answer

class functor (m:Type -> Type) =
{
  fmap: (#a:Type -> #b:Type -> (a -> b) -> m a -> m b);
}

let id (a:Type) = a

instance id_functor : functor id =
{
  fmap = (fun #a #b f -> f);
}

let test_id (a:Type) (f:a -> a) (x:id a) = fmap f x

instance option_functor : functor option =
{
  fmap = (fun #a #b (f:a -> b) (x:option a) ->
            match x with
            | None -> None
            | Some y -> Some (f y));
}

let test_option (f:int -> bool) (x:option int) = fmap f x

instance monad_functor #m (d:monad m) : functor m =
{
  fmap = (fun #a #b (f:a -> b) (c:m a) -> let! x = c in return (f x))
}

Beyond Monads with Let Operators

Many monad-like structures have been proposed to structure effectful computations. Each of these structures can be captured as a typeclass and used with F*’s syntactic sugar for let operators.

As an example, we look at graded monads, a construction studied by Shin-Ya Katsumata and others, in several papers. This example illustrates the flexibility of typeclasses, including typeclasses for types that themselves are indexed by other typeclasses.

The main idea of a graded monad is to index a monad with a monoid, where the monoid index characterizes some property of interest of the monadic computation.

A monoid is a typeclass for an algebraic structure with a single associative binary operation and a unit element for that operation. A simple instance of a monoid is the natural numbers with addition and the unit being 0.

class monoid (a:Type) =
{
   op   : a -> a -> a;
   one  : a;
   properties: squash (
     (forall (x:a). op one x == x /\ op x one == x) /\
     (forall (x y z:a). op x (op y z) == op (op x y) z)
   );
}

instance monoid_nat_plus : monoid nat =
{
  op = (fun (x y:nat) -> x + y);
  one = 0;
  properties = ()
}

A graded monad is a type constructor m indexed by a monoid as described by the class below. In other words, m is equipped with two operations:

  • a return, similar to the return of a monad, but whose index is the unit element of the monoid

  • a ( let+ ), similar to the ( let! ) of a monad, but whose action on the indexes corresponds to the binary operator of the indexing monoid.

class graded_monad (#index:Type) {| monoid index |}
                   (m : index -> Type -> Type) = 
{
  return : #a:Type -> x:a -> m one a;
  
   ( let+ )   : #a:Type -> #b:Type -> #ia:index -> #ib:index ->
           m ia a -> 
           (a -> m ib b) ->
           m (op ia ib) b

}

With this class, we have overloaded ( let+ ) to work with all graded monads. For instance, here’s a graded state monad, count_st whose index counts the number of put operations.

let count_st (s:Type) (count:nat) (a:Type) = s -> a & s & z:nat{z==count}

let count_return (#s:Type) (#a:Type) (x:a) : count_st s one a = fun s -> x, s, one #nat

let count_bind (#s:Type) (#a:Type) (#b:Type) (#ia:nat) (#ib:nat)
               (f:count_st s ia a)
               (g:(a -> count_st s ib b))
  : count_st s (op ia ib) b
  = fun s -> let x, s, n = f s in
          let y, s', m = g x s in
          y, s', op #nat n m

instance count_st_graded (s:Type) : graded_monad (count_st s) =
{ 
  return = count_return #s;
  ( let+ ) = count_bind #s;
}

// A write-counting grade monad
let get #s : count_st s 0 s = fun s -> s, s, 0
let put #s (x:s) : count_st s 1 unit = fun _ -> (), x, 1

We can build computations in our graded count_st monad relatively easily.

let test #s =
  let+ x = get #s in
  put x

//F* + SMT automatically proves that the index simplifies to 2
let test2 #s : count_st s 2 unit =
  let+ x = get in
  put x ;+
  put x

F* infers the typeclass instantiations and the type of test to be count_st s (op #monoid_nat_plus 0 1) unit.

In test2, F* infers the type count_st s (op #monoid_nat_plus 0 (op #monoid_nat_plus 1 1)) unit, and then automatically proves that this type is equivalent to the user annotation count_st s 2 unit, using the definition of monoid_nat_plus. Note, when one defines let+, one can also use e1 ;+ e2 to sequence computations when the result type of e1 is unit.

Summary

Typeclasses are a flexible way to structure programs in an abstract and generic style. Not only can this make program construction more modular, it can also make proofs and reasoning more abstract, particularly when typeclasses contain not just methods but also properties characterizing how those methods ought to behave. Reasoning abstractly can make proofs simpler: for example, if the monoid-ness of natural number addition is the only property needed for a proof, it may be simpler to do a proof generically for all monoids, rather than reasoning specifically about integer arithmetic.

That latter part of this chapter presented typeclasses for computational structures like monads and functors. Perhaps conspicuous in these examples were the lack of algebraic laws that characterize these structures. Indeed, we focused primarily on programming with monads and graded monads, rather than reasoning about them. Enhancing these typeclasses with algebraic laws is a useful, if challenging exercise. This also leads naturally to F*’s effect system in the next section of this book, which is specifically concerned with doing proofs about programs built using monad-like structures.