F# existential types

ExistentialEngines.fs

// The engine interface and helpers

type IEngine<'a,'b> =
    abstract member Capacity : int // Does not depend on 'a or 'b; just an example
    // Some other stuff here possible depending on 'a and 'b

/// A function which works on any engine polymorphically and returns a result of type 'r'. Needed because
/// F# does not support higher-ranked types (not the same as HKT!) in regular functions. This does work in members.
type EngineFunction<'r> =
    abstract member Apply : IEngine<'a,'b> -> 'r

/// Hides type parameters of an engine. "Existential types" because "there is (exists) a type passed as a parameter to
/// IEngine, but I won't tell you which".
type ExistsEngine =
    abstract member Elim : EngineFunction<'r> -> 'r

// Helper for introduction. Use this to "unify" engines of different types.
let existsEngine engine = { new ExistsEngine with
    member _.Elim f = f.Apply engine
}

// Helper for elimination. Use this to do something with any engine.
let elimExistsEngine f (engine : ExistsEngine) = engine.Elim f

// Example

// A string, int engine
let engine1 = { new IEngine<string,int> with
    member _.Capacity = 3
}

// A int, string, so different type from engine1
let engine2 = { new IEngine<int, string> with
    member _.Capacity = 5
}

// A list with both engines, in a way
let bothEngines = [existsEngine engine1; existsEngine engine2] // List<ExistsEngine>

// Corresponds to the function which determines the capacity of any engine.
let capacity = { new EngineFunction<int> with
    member _.Apply engine = engine.Capacity
}

// Maximum capacity of all engines, regardless of their type
let maxCapacity = bothEngines |> List.map (elimExistsEngine capacity) |> List.max // int