什么是行类型?它们是代数数据类型吗?

MiP*_*MiP 20 .net f# ocaml functional-programming

我经常听说F#缺乏对OCaml行类型的支持,这使得语言比F#更强大.

这些是什么?它们是代数数据类型,例如总和类型(有区别的联合)还是产品类型(元组,记录)?是否可以在其他方言中写行类型,例如F#?

ivg*_*ivg 21

首先,我们需要修复术语.至少在类型理论中,特别是在OCaml的类型系统中,没有"行类型" 这样的东西.存在"行多态",我们将在0以下讨论它.

行多态性是多态的一种形式.OCaml提供两种多态 - 参数和行,而缺少其他两种 - ad hoc和包含(也称为子类型)1.

首先,什么是多?在类型系统的上下文中,多态性允许单个术语具有多种类型.这里的问题是单词类型本身在计算机科学和编程语言社区中严重超载.因此,为了最大限度地减少混淆,让我们在这里重新介绍它,在同一页2上.一种术语通常表示术语语义的某种近似.语义可以像一组配有一组操作或更复杂的值(如效果,注释和任意理论)一样简单.通常,语义表示一个术语的所有可能行为的集合.类型系统表示一组规则,允许某些语言构造,并根据其类型禁止其他语言.即,它验证术语的组合行为是否正确.例如,如果某种语言中存在函数应用程序构造,则类型系统将仅允许应用程序使用具有与参数类型匹配的类型的参数.这就是多态性发挥作用的地方.在单形类型系统中,这种匹配可能只是一对一,即文字.多态类型系统提供了指定一些与一族类型匹配的正则表达式的机制.因此,不同类型的多态性只是不同类型的正则表达式,您可以使用它们来表示类型族.

现在让我们从这个角度来看待不同类型的多态.例如,参数多态就像正则表达式中的点.例如,'a list. list- 这意味着我们按字面意思匹配list,list类型的参数可以是任何类型.行多态性是星形运算符,例如,<quacks : unit; ..>与...相同<quacks : unit; .*>.这意味着它匹配任何类型,quacks并做任何其他3.说到名义上的子类型,在这种情况下,我们有名义类(在regexp中也称为字符类),并且我们指定了一系列具有其基类名称的类型.例如,duck就像[:duck:]*任何正确注册为类成员的值匹配此类型(通过类继承和new运算符)4.最后,ad-hoc多态实际上也是名义上的,并映射到正则表达式中的字符类.这里的主要区别在于ad-hoc多态的类型概念不是应用于值,而是应用于名称.因此,名称(如函数名称或+运算符)可能具有多个定义(实现),应使用某种语言机制静态注册(例如,重载运算符,实现方法等).因此,ad-hoc多态只是名义子类型的特例.

现在,当我们清楚时,我们可以讨论行多态性给我们带来什么.行多态性是结构类型系统的一个特征(也称为动态类型语言中的鸭子类型),与提供子类型多态性的名义类型系统形成对比.一般来说,正如我们上面所讨论的,它允许我们指定一种类型为"任何嘎嘎叫"而不是"任何实现IDuck接口的东西".当然,你可以通过定义duck接口并使用一些inheritimplements机制显式地将所有实现注册为此接口的实例来对标称类型执行相同的操作.但这里的主要问题是您的层次结构是密封的,即您需要更改代码以在新创建的接口中注册实现.这打破了开放/封闭原则并阻碍了代码重用.名义子类型的另一个问题是,除非你的层次结构形成一个格子(即,对于任何两个类总是有一个最小上限),你不能在它上面实现类型推断5.

进一步阅读

  • 目标ML:ML的有效面向对象扩展 - 对该主题的全面描述.

  • FrançoisPottier和DidierRémy.ML类型推理的本质.在Benjamin C. Pierce,编辑,类型和编程语言高级主题,麻省理工学院出版社,2005年. - 有关行的详细解释,请参见第10.8节.

  • 结构多态性的简单类型推断 - 详细解释在存在类型推断时结构和行多态之间的相互作用.


0)正如@nekketsuuu在评论中指出的那样,我使用的术语有点自愿,因为我的目的是提供一个易于理解和高层次的想法,而不是深入细节.从那以后我修改了帖子,使其更加严格.

1)然而,OCaml提供了具有继承和子类型概念的类,它仍然不是根据通用定义的子类型多态性,因为它不是名义上的.从答案的其余部分可以更清楚地看出来.

2)我只是在修理术语,我并不是说我的定义是正确的.许多人认为类型表示值的表示,并且历史上这是正确的.

3)也许是一个更好的正则表达式,<.*; quacks : unit; .*>但我认为你有了这个主意.

4)因此OCaml没有子类型多态性,尽管它有一个子类型的概念.当您指定类型时,它将与子类型不匹配,它只会按字面匹配,并且您需要使用显式向上转换运算符来使类型T的值适用于super(T)预期的上下文.因此,尽管OCaml中存在子类型,但它与多态性无关.

5)虽然格子要求看起来并不可能,但在现实生活中很难对层次结构施加这种限制,或者如果强加,则类型推断的精度将始终与类型层次结构的精度相关联.所以在实践中,它不起作用,参见 斯卡拉

(在第一次阅读时跳过此注释)虽然在OCaml中存在行变量,用于将行多态嵌入到仅具有参数多态的OCaml类型推断中.

‡)通常,单词类型与类型系统可互换使用,以指代整个类型系统中的一组特定规则.例如,有时我们说"OCaml有行键入"来表示OCaml类型系统为"行多态"提供规则的事实.

  • 非常彻底的答案 - 特别是层次结构的格结构非常有启发性!但是,我无法关注您_所以,临时多态性只是名义子类型化的一个特例_。我将 ad-hoc 描述为两种对于特定目的等效的类型。不过,我看不到这两种类型之间的子类型关系。 (2认同)
  • 是的,我试图简短,因为我不想进入特别打字的特殊性,作为一个完全不同的问题.ad-hoc多态类型表示一类类型,其名义上(即,通过绑定到某个名称,而不是通过结构)将其自身置于该名称的适用类型的类中.这基本上是名义子类型的特殊情况,除了通过重载函数的名称指定接口,并且层次结构高度为1. (2认同)

Pat*_*atJ 10

行类型很奇怪.而且非常强大.

行类型用于在OCaml中实现对象和多态变体.

但首先,这是没有行类型我们不能做的事情:

type t1 = { a : int; b : string; }
type t2 = { a : int; c : bool; }

let print_a x = print_int x.a

let ab = { a = 42; b = "foo"; }
let ac = { a = 123; c = false; }

let () =
 print_a ab;
 print_a ac
Run Code Online (Sandbox Code Playgroud)

这段代码当然会拒绝编译,因为print_a必须有一个唯一的类型:或者t1,或者t2不是两者.但是,在某些情况下,我们可能需要这种确切的行为.这就是行类型的用途.这就是他们所做的:更"灵活"的类型.

在OCaml中,行类型主要有两种用途:对象多态变体.在代数方面,对象为您提供"行产品"和多态变体"行和".

关于行类型的注意事项是,您最终可以使用一些子类型进行声明,并且非常反直观的类型和语义(特别是在案例类中).

您可以查看本文以获取更多详细信息.

  • 你的答案始于这么多的承诺,然后就结束了.你基本上给了两个链接.好吧,三个.:( (3认同)

Ric*_*nne 8

我将用他的例子完成PatJ的优秀答案,用类编写.

鉴于以下类别:

class t1 = object
  method a = 42
  method b = "Hello world"
end

class t2 = object
  method a = 1337
  method b = false
end
Run Code Online (Sandbox Code Playgroud)

以下对象:

let o1 = new t1
let o2 = new t2
Run Code Online (Sandbox Code Playgroud)

您可以编写以下内容:

let print_a t = print_int t#a;;
val print_a : < a : int; .. > -> unit = <fun>

print_a o1;;

42
- : unit = ()

print_a o2;;

1337
- : unit = ()
Run Code Online (Sandbox Code Playgroud)

您可以在print_a签名中看到行类型.这< a : int; .. >是一种字面意思是"任何至少a具有签名方法的对象int"的类型.

  • 我对ocaml语法不理解的是为什么使用`..`而不是类型变量.使用purescript我可以定义`forall r.{label :: String | r} - > {label :: String | r} - > String`.现在两个记录必须具有相同的行类型.但我也可以用另一个类型var替换第二个`r`来表示两种行类型可能不同.这如何与ocaml一起使用? (4认同)
  • &gt; 我不明白 ocaml 语法的原因是为什么使用 .. 而不是类型变量。因为`..` 是一个隐式类型变量。您可以使用 `as` 使其明确,例如,您在 OCaml 中的示例是:`(&lt; label : string; .. &gt; as 'a) -&gt; 'a` (2认同)