在调用功能和回调之间对齐多态性变体类型



我正在尝试编写一个事件处理程序,该事件处理程序不需要处理所有已知类型的事件,并且正在尝试使用OCAML多态性变体类型(event.mli)进行建模:

type 'events event =
  [< `click of int * int | `keypress of char | `quit of int ] as 'events
(* Main loop should take an event handler callback that handles 'less than' all known event types *)
val mainLoop : ('events event -> unit) -> unit
val handler : 'events event -> unit

示例实现(event.ml):

type 'events event =
  [< `click of int * int | `keypress of char | `quit of int ] as 'events
let mainLoop handler =
  for n = 1 to 10 do
    handler begin
      if n mod 2 = 0 then `click (n, n + 1)
      else if n mod 3 = 0 then `keypress 'x'
      else `quit 0
    end
  done
let handler = function
  | `click (x, y) -> Printf.printf "Click x: %d, y: %dn" x y
  | `quit code -> exit code

不幸的是,由于以下错误而失败:

File "event.ml", line 1:
Error: The implementation event.ml
       does not match the interface event.cmi:
       Values do not match:
         val mainLoop :
           ([> `click of int * int | `keypress of char | `quit of int ] -> 'a) ->
           unit
       is not included in
         val mainLoop :
           ([< `click of int * int | `keypress of char | `quit of int ] event ->
            unit) ->
           unit
       File "event.ml", line 4, characters 4-12: Actual declaration

如何将mainLoop的实现推断为([< `click of int * int | `keypress of char | `quit of int ] -> unit) -> unit类型,即('events event -> unit) -> unit

让我们用普通英语和一些常识来解释'亚型理论'。

在面向对象的语言(例如Java或Ocaml)中,您可能定义的最通用类是空类,即。没有属性和方法的类。实际上,任何类都可以从中衍生出来,在类型方面,任何类类型都是空类型的子类型。

现在,函数被认为是 contravariant 在其输出上的 convariant

如果我们查看函数的表现如何打字,我们会看到:

  • 您可以将其接受类型的值或该类型的任何子类型的值传递给它。在极端情况下,如果您定义一个接受空类实例的函数,显然,该功能将无法对其做任何事情。因此,所有其他类的实例也将做到,因为我们知道该功能不会期望它任何东西。
  • 函数的结果可能是将其定义为返回的类型的值,或该类型任何子类型的值。

为什么我们使用两个不同的单词来表现出相同的行为来进行输入和输出?

好吧,现在考虑ML样式类型理论中的常用类型构造函数:产品(*类型构造函数),总和(代数数据类型)和箭头(函数类型)。基本上,如果您使用产品或总和定义了T型,则专门(使用子类型)他们的任何参数都会产生T的专业化(亚型)。我们称此功能称为协方差。例如,由总和制成的列表构造函数是协变量的:如果您有a类列表,并且b始于a,则类型b lista list的子类型。确实,对于接受a list的功能,您可以将其传递给没有错误的b list

如果我们查看箭头 ->构造函数,故事略有不同。类型x -> y的功能F采用x的任何子类型,并返回y的任何子类型。如果我们认为X是函数类型,则意味着F实际键入(u -> v) -> y,而x = u -> v。到目前为止,一切都很好。在这种情况下,uv如何变化?这取决于F可能对其做什么。F知道它只能将uu的子类型传递给该功能,因此F可以通过的最一般值是u,这意味着所传递的实际函数可以接受u的任何SUPERTYPE作为IT参数。在极端情况下,我可以给F一个函数,该函数接受空对象作为其参数并返回类型v的东西。因此,突然之间,一组类型从"类型和亚型"变为"类型和超级型"。因此,u -> v类型的子类型是u' -> v',其中v'v的子类型,而u'的子类型是u supertype 。这就是为什么我们的箭头构造器在其输入中违反了构造。类型构造函数的方差是如何根据其参数的亚型/supertypes确定其子类型/超级型。

接下来,我们必须考虑多态性变体。如果类型x定义为[ `A | `B ],那么与y = [ `A ]类型有什么关系?子类型的主要属性是,给定类型的任何值都可以安全地升至超级类型(实际上是通常定义子类型的方式)。在这里,`A属于两种类型,因此铸件两种方式都是安全的,但是`B仅存在于第一种类型中,因此可能不会将其施放到第二种。因此,可以将y的值施加到第一个,但是x的值不得将其施加到第二个。子类别的关系很明确:yx的子类型!

[> ... ][< ...]符号呢?第一种代表一种类型及其所有超级型(其中有一个无穷大),而第二种表示类型及其所有子类型(这是一个有限的集合,包括空类型)。因此,对于采用多态性变体v的函数的自然推断的类型将在输入上,该变体及其所有子类型,即。[< v ],但是高阶函数(将函数作为参数作为参数的功能)将看到该参数差异被翻转,因此其输入类型将与([> v ] -> _) -> _相似。函数方差的确切规则在上面链接的Wikipedia页面中表示。

现在,您可能可以了解为什么无法构建您目标的类型-([< _ ] -> _) -> _)-。我们禁止箭头的差异。

那么,您可以在代码中做什么?我的猜测是,您真正想做的是推理算法将从您的示例代码:([> basic_event ] -> _) -> _)中推断出来的。 basic_event类型将是恰好覆盖3个变体的类型。

type basic_event =
   [ `click of int * int | `keypress of char | `quit of int ]
(* Main loop should take an event handler callback that handles 'less than' 
   all known event types *)
val mainLoop : ([> basic_event ] -> unit) -> unit
val handler : [< `click of int * int | `quit of int ] -> unit

在您的情况下,最好不要在类型中包含下层或上限,并在函数签名中使用这些界限,如上述代码中所述。

我认为问题在您的类型定义中,我知道您的类型最多包含这三个事件(首先,首先为什么最多'最多'而不是'至少''?)但是,在这种情况下,使用mainLoop的签名,您不能预备您的类型。

例如,查看x的类型:

let (x : [< `A | `B]) = `A
val x : [< `A | `B > `A ] = `A

[< ... >][< ...]不同。这意味着即使您施放mainLoop,您也会有一个错误:

let mainLoop (handler :
              [< `click of int * int | `keypress of char | `quit of int ]
              event -> unit) = ...
       Values do not match:
         val mainLoop :
           ([ `click of int * int | `keypress of char | `quit of int ] event ->
            unit) ->
           unit
       is not included in
         val mainLoop :
           ([< `click of int * int | `keypress of char | `quit of int ] event ->
            unit) ->
           unit

但是真的有问题吗?为什么不将type 'events event = [< ...更改为type 'events event = [ ...

,我认为使用下界而不是上限更好:

type 'events event =
  [> `click of int * int | `keypress of char | `quit of int ] as 'events
val mainLoop : ('events event -> unit) -> unit
val handler : 'events event -> unit
let mainLoop handler =
  for n = 1 to 10 do
    handler (
      if n mod 2 = 0 then `click (n, n + 1)
      else if n mod 3 = 0 then `keypress 'x'
      else `quit 0
    )
  done
let handler = function
  | `click (x, y) -> Printf.printf "Click x: %d, y: %dn" x y
  | `quit code -> exit code
  | _ -> ()

最新更新