Higher Standard

Higher kinded polymorphism in Standard ML!

An attempt at translating some of Jeremy Yallop and Leo White's higher library into SML.

DISCLAIMER: Due to what may be a bug in SML/NJ (or a bug in my code, honestly not sure which), some fairly standard operations cause crashes. See Issues for details.

Higher kinded polymorphism is implemented through defunctionalization. Instead of promoting type variables to allow abstraction over type constructors (anything of kind k -> * ), we demote type constructor application with the type ('a,'f) app, which represents 'a 'f. In more concrete terms: (int,list) app == int list. To achieve this, we make ('a,'f) app abstract, and then provide functors to construct a defunctionalized type constructor for a given real type constructor. These are Higher.Mk1 and Higher.Mk2, which can be easily generalized to MkN if desired. A central use case of abstracting over type constructors is allowing haskell style type class constraints on them. The original paper uses the ocaml object system to represent type classes, but SML has no such system. It does however have records. Ideally, we'd like to be able to do this:

type 'f Functor = { fmap : forall 'a 'b . ('a -> 'b) -> ('a,'f) app -> ('b,'f) app }

Unfortunately, SML lacks any first class polymorphism, so all type variables must be bound at the site of the type declaration, and not inside the record field. This results in the rather unsatisfying

type ('a,'b,'f) Functor = { fmap : ('a -> 'b) -> ('a,'f) app -> ('b,'f) app }

Not only does this not look as nice, it causes issues when trying to use type class instances. For example:

(*  won't_work : ('a,'b,'f) Functor -> (int,'f) app -> (int,'f) app *) 
fun won't_work (cls : ('a,'b,'f) Functor) f = #fmap cls (fn x => x+1) f

This fails to type check because cls is not polymorphic in the body of won't_work, since 'a and 'b are bound at the declaration of the function, not inside the argument. To alleviate this, we provide the MkCls functor:

functor MkCls (type ('a,'b,'c,'d,'e,'P) base) :
sig
  type 'P cls
  val instance : ('a,'b,'c,'d,'e,'P) base -> 'P cls
  val & : 'P cls -> (('a,'b,'c','d,'e,'P) base -> 'f) -> 'f
end

Unfortunately this can be used to create objects that don't act like type classes, but it's meant to be used like so:

structure Functor = 
  Higher.MkCls (type ('a,'b,'c,'d,'e,'f) base = 
    { fmap : ('a -> 'b) -> ('a,'f) app -> ('b,'f) app }
  )

The first 5 type variables are intended for use anywhere in your type class, but you don't have to use all of them. The final 'f is intended to be the type the class is constraining. If you need more than 5 type variables to write your class, the code can be rewritten to use as many as you like. Now Functor.into turns a record into a Functor instance, whose fields we can access with Functor.&, i.e. Functor.&instance #fmap. This allows writing fairly idiomatic functions with type class arguments:

(*  <$ : 'f Functor.cls -> 'a -> ('b,'f) app -> ('a,'f) app *)
fun <$ cls x = Functor.&cls #fmap (const x)

To use the when and unless examples from the original paper, assuming we've created a monad class:

(*  when : 'm Monad.cls -> bool -> (unit,'m) app -> (unit,'m) app *)
fun when cls b m = if b then m else Monad.&cls #pure ()

(*  unless : 'm Monad.cls -> bool -> (unit,'m) app -> (unit,'m) app *)
fun unless cls b m = when cls (not b) m

Check out lens.sml for an implementation of van Laarhoven style lenses!