Typeclasses

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

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

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

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

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

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

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

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

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

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 = ()
  }

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

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)

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

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.

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.

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)

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.