Simulating higher-kinded polymorphism with Object Algebra's in F#

Question

In the paper Streams à la carte: Extensible Pipelines with Object Algebras Biboudis et al. outline a method of "emulating type-constructor ploymorphism" using object algebras.

I am trying to use this method to implement a higher-order example, similar to those described in Typed Tagless Final Interpreters, within F# and have the following:

type App<'f,'a> = interface end

type ExprSYM<'f,'a> = 
  abstract litInt: int -> App<'f,int>
  abstract litBool : bool -> App<'f,bool>
  abstract add : App<'f,int> -> App<'f,int> -> App<'f,int>
  abstract gt : App<'f,int> -> App<'f,int> -> App<'f,bool>
  abstract conj : App<'f,bool> -> App<'f,bool> -> App<'f,bool>

The section relating to Brand Freshness describes nesting a class inside a type constructor. My translation to F# looks like:

type Eval<'a> =
  static member t = new obj()
  static member prj (app : App<Eval.t,'a>) = app :> Eval<'a>
  inherit App<Eval.t,'a>

However, I get the error The type 't' is not defined.

What is the correct way to write this in F#?

Answer 1

Using a nested class doesn't particularly buy you anything; as the authors say

In the Yallop and White technique for OCaml, this is ensured syntactically by the “freshness” of the brand, t, which is private to the type constructor. In Java, the property is ensured by convention: every subtype S of App has a locally defined brand t and no subtype of App<S.t, X> other than S exists.

so you can obtain the same result with a different convention in F# (which doesn't support nested classes or static members within interfaces). For example, you could create the subclass plus a separate marker class inside a module:

module Pull = 
    type t = class end
    type Pull<'t> = 
        inherit App<t, 't>
    let prj (app : App<t, 't>) = app :?> Pull<'t>

and then ensure that you don't use Pull.t elsewhere.