在 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 ->打包 ->打包 ->打包.我希望它是通用的，即:

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屋！