ocaml - 来自外部的参数化 GADT

Question

GADT 允许某种形式的动态类型:

type _ gadt =
  | Int: int -> int gadt
  | Float: float -> float gadt

let f: type a. a gadt -> a = function
  | Int x -> x + 1
  | Float x -> x +. 1.

我希望能够执行相同类型的调度，但使用参数化类型，并且可以从外部访问 gadt 的参数。 如果参数是通用量化的或固定的，这很容易:

type (_,_) container = 
  | List: 'a list -> ('a,'a list) container

let f : type a b. (a,b) container -> b = fun (List l) -> l
let g : type a b. a -> (a, b) container -> b = fun x (List l) -> x::l
let h : type b. (int, b) container -> b = fun (List l) ->  1::l

但是，如果参数有其他形式的约束，则这不起作用:

class ['a] ko (x:'a) = object 
    method m : type b. ('a, b) container -> b = fun (List l) -> x::l
end

我收到错误:类型构造函数 a#0 将转义其范围。 我猜这是由于从外到内的限制，没有完全理解该领域。

我发现的唯一解决方案是使用更高级的模块:

open Higher
module Higher_List = Newtype1 (struct type 'a t = 'a list end)
type ('a,_) container = List: 'a list -> ('a, Higher_List.t) container

class ['a] c (x:'a) = object
    method m : type b. b container -> ('a,b) app = fun (List l) -> Higher_List.inj(x::l)
end

然而，这个解决方案远非完美:首先它很冗长，到处都是 inj 和 prj，更重要的是，它有很多限制:'a 参数不能有约束，也不能有方差...

有人知道更好的解决方案吗？

编辑

经过一番思考，Drup 解决方案是有效的，但必须小心谨慎!在我的完整问题(不是这个问题中的玩具程序)中，我需要在方法定义中访问 self 。因此，回到 Drup 解决方案，我必须将 self 传递给中间函数，为此，我必须给它一个类型。所以我必须首先声明一个类类型...

class type ['a] c_type = object
    method m: ('a, 'b) container -> 'b
end

let cons : type a b. a c_type -> a -> (a,b) container  -> b =
    fun self x (List l) -> x::l

class ['a] c (x:'a) = object(self: 'a #c_type)
    method m = cons (self :> 'a c_type) x
end

但是，如果类 c 对 'a 有约束，则这将不起作用:cons 的类型将无效，因为a必须被普遍量化，但在a c_type中受到限制。解决方案是编写 c_type，而不对 'a 进行约束。但请注意，这意味着大量重写。在许多情况下，仅仅省略约束并不足以使其消失:它的所有用法都必须是无约束的......

所以最终的解决方案如下:

type (_,_) container = 
  | List: 'a list -> ('a,'a list) container

class type ['a] c_type = object
    (* no constraint on 'a, and take care of its usage ! *)
    method m: ('a, 'b) container -> 'b
end

let cons : type a b. a c_type -> a -> (a,b) container  -> b =
    fun self x (List l) -> x::l (* in real code, self is used... *)

class ['a] c (x:'a) = object(self: 'a #c_type)
    constraint 'a = < .. > (* well just for the example *)
    method m = cons (self :> 'a c_type) x
end

Answer 1

当你可以做简单的事情时为什么要尝试复杂的事情？ :)

type (_,_) container =
  | List: 'a list -> ('a,'a list) container

let cons : type a b. a -> (a, b) container -> b = fun x (List l) -> x::l

class ['a] ko (x:'a) = object
    method m : type b. ('a, b) container -> b = cons x
end

这种构造很棘手，因为局部抽象类型的放置很重要。在您的情况下，您希望在类的外层使用本地抽象类型(对于类型a)，这是不可能的。制作一个中间的、适当抽象的函数通常会有所帮助。

此外，请勿使用更高。这是您可以在模块系统中对 HKT 进行编码的证明，而不是鼓励您实际这样做。