Expressing existential types in F#

Question

As far a I can tell, F# doesn't have any support for existential types. So, I'm looking for another way to express my idea.

I've got a data structure and its contents can be interpreted in a number of different ways. In this particular example I'll suppose it can be viewed as an int or a real:

type Packed = (* something sensible *) unit

type PackedType = | PackedInt
                  | PackedReal


let undefined<'a> : 'a = failwith "undefined"

let unpackInt : Packed -> int = undefined
let unpackReal : Packed -> real = undefined

let packInt : int -> Packed = undefined
let packReal : real -> Packed = undefined

where real is something meaningful, say:

type real = int * int

let addReal : real -> real -> real = undefined

Now, I need a function addPacked : PackedType -> Packed -> Packed -> Packed. I'd like it to be general, that is:

type NumberOp = [forall t] { opPack : 't -> Packed; opUnpack : Packed -> 't; opAdd : 't -> 't -> 't }

let getNumberOp (t : PackedType) =
    match t with
    | PackedInt -> { opPack = packInt; opUnpack = unpackInt; opAdd = (+) }
    | PackedReal -> { opPack = packReal; opUnpack = unpackReal; opAdd = addReal }


let addPacked (t : PackedType) (a : Packed) (b : Packed) =
    let { opPack = pack; opUnpack = unpack; opAdd = add } = getNumberOp t
    pack <| add (unpack a) (unpack b)

Here I ended up with NumberOp being existetial. So I'm asking whether there is another way to express this. I can't alter Packed, [un]pack* functions and addPacked's type.

I've found this answer. It states that there is a “well-known pattern”, but the text is difficult to read and I couldn't make it work.

Answer 1

In general, you can encode the type

∃t.F<t>

as

∀x.(∀t.F<t> → x) → x

Unfortunately, each universal quantification requires creating a new type in F#, so a faithful encoding requires two types in addition to F. Here's how we can do this for your example:

type 't NumberOps = {
    opPack : 't -> Packed
    opUnpack : Packed -> 't
    opAdd : 't -> 't -> 't 
}

type ApplyNumberOps<'x> = 
    abstract Apply :  't NumberOps -> 'x

// ∃ 't. 't NumberOps
type ExNumberOps =
    abstract Apply : ApplyNumberOps<'x> -> 'x

// take any 't NumberOps to an ExNumberOps
// in some sense this is the only "proper" way to create an instance of ExNumberOps
let wrap n = { new ExNumberOps with member __.Apply(f) = f.Apply(n) }

let getNumberOps (t : PackedType) =
    match t with
    | PackedInt -> wrap { opPack = packInt; opUnpack = unpackInt; opAdd = (+) }
    | PackedReal -> wrap { opPack = packReal; opUnpack = unpackReal; opAdd = addReal }

let addPacked (t : PackedType) (a : Packed) (b : Packed) =
    (getNumberOps t).Apply 
        { new ApplyNumberOps<_> with 
            member __.Apply({ opPack = pack; opUnpack = unpack; opAdd = add }) = 
                pack <| add (unpack a) (unpack b) }

There's a lot of boilerplate here, unfortunately. Also, I've used the unhelpful names Apply for the abstract members of each helper type - feel free to substitute something more meaningful if you can find names that you prefer. I've tried to keep fairly close to your style, but in my own code I'd probably avoid destructuring the record within addPacked, using the field accessors directly instead.