ModeOfUse.md

Consider the following (not particularly useful) Haskell function

  f :: forall a . Eq a => a -> a -> ()
  f x y = if x == y then f [x, x] [y, y] else ()

My understanding is that this would be translated to something like

  functor F (struct X : sig type a
                            structure Eq : EQ where type t = a
                        end) = struct
    structure Xinst = struct
      type a = X.a list
      structure Eq = EqList (Eq)
    end
    structure Finst = F (Xinst) 
    fun f x y = if Eq.== x y then Finst.f [x, x] [y, y] else ()
  end

But note that we use F in the body of F in order to call f at the type a list in the recursive call.

It seems like one may claim that typeclasses are merely a mode of use of the ML+recursive modules. But that's an awful lot of machinery to bring along.

Yeah, it would look like that. And indeed the functor F would need to be recursive. A bit simplified:

functor F (X : EQ)
  : sig
      val v : X.t -> X.t -> ()
    end
  = struct
      val v = fn x y => if X.eq x y then (F(EqList(X))).v [x, x] [y, y] else ()
    end

But I'm not sure whether polymorphic recursion would be a problem for type inference. Presumably it would need to have the usual restriction, i.e., that the source-language program provides a type annotation for f.

It's funny: I never actually realized before that the MTC paper doesn't allow recursion!

Adding this twitter thread for reference: https://twitter.com/lambdageek/status/544610916869079041