在F#中表达存在类型 [英] Expressing existential types in F#

问题描述

据我所知，F#对存在类型不提供任何支持.因此，我正在寻找另一种表达想法的方法.

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.

我有一个数据结构，可以用许多不同的方式来解释其内容.在这个特定的示例中，我想可以将其视为一个int或一个实数:

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

其中real是有意义的，例如:

where real is something meaningful, say:

type real = int * int

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

现在，我需要一个功能addPacked : PackedType -> Packed -> Packed -> Packed.我希望它是通用的，即:

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)

在这里，我最终以NumberOp存在.所以我想问是否还有另一种表达方式.我无法更改Packed，[un]pack*函数和addPacked的类型.

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.

推荐答案

通常，您可以对类型进行编码

In general, you can encode the type

∃t.F<t>

为

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

不幸的是，每个通用量化都需要在F#中创建一个新类型，因此，忠实的编码除了F之外还需要两种类型.这是我们为您的示例执行的操作:

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) }

不幸的是，这里有很多样板.另外，我对每种帮助程序类型的抽象成员都使用了无用的名称Apply-如果您可以找到自己喜欢的名称，请随意替换更有意义的名称.我试图保持与您的风格相当接近，但是在我自己的代码中，我可能会避免直接使用字段访问器来破坏addPacked中的记录.

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.

这篇关于在F#中表达存在类型的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！