shh*_*you 3 type-systems programming-languages functional-programming
什么是联合类型和交集类型？
我已经咨询了这个问题,但是一些小型工作类型系统会更好,而不是必要的实用系统.
具体来说,通过联合类型,我指的是本博文中提到的 而不是sum类型,其中伪代码看起来像
{String, null} findName1() {
if (...) {
return "okay";
} else {
return null;
}
}
在维基百科页面有交集类型与联合类型的简短说明,但似乎这个没有进一步的参考.
联合和交集类型只是将类型视为值集(大多数是无限集).如果您正在考虑类型,则可以将对结果集的集合的任何操作应用于类型(值集)以创建新类型(值集),至少在概念上.
联合类型在某种意义上类似于总和类型,您似乎熟悉它.事实上,我经常听到描述为"歧视联盟"类型的和类型.基本区别在于,类似(Haskell表示法)的和类型data FooBar = Foo Integer | Bar String允许您判断给定FooBar值是包含a Integer还是a String(因为FooBar值标记为Foo或Bar).即使我们写data FooBar = Foo Integer | Bar Integer两个类型相同的地方,"标签"也会增加额外的信息,我们可以告诉它FooBar是"哪个整数" .
类型的联合类型将是(无效的Haskell)data FooBar = Integer | String.FooBar简单中的值是所有字符串值和所有整数值.如果我们创建一个相同两种类型的联合类型,那么data FooBar = Integer | Integer它应该在逻辑上与just无法区分Integer,因为一个集合与它自身的联合本身.
原则上,你可以用类型U中的值来做的事情是类型A和B的联合,它们只是处理As的操作,也适用于Bs; ,仅适用于无论是作为或BS的任何操作可能得到错误的类型的输入,因为ü没有信息说无论是A还是B. 1
(Undiscriminated)联合类型在类型系统类似于Haskell的语言中不会非常有趣,因为具体类型是不相交的2,因此对As和B都有效的唯一操作适用于所有值(除非A是B,其中它只是适用于该单一类型的所有操作).
但在某种程度上,类型类(如果你熟悉它们)是提供类似联合类型的东西的一种方式.一个多态但被约束为某个类型类的成员的类型有点像类型类中所有类型的并集(除了你不知道它们是什么,因为类型类原则上是开放的); 您可以使用这样的值做的唯一事情是已声明处理类型类中每种类型的值的thins .
在具有子类型的语言中,联合类型可能很有趣(在面向对象的编程语言中很常见).如果你将一个普通超类型的两个子类型联合在一起,你得到的东西至少支持超类型的操作,但是它排除了超类型的任何其他子类型,所以它与使用超强型.
交集类型正是概念,但使用交集而不是并集.这意味着您可以使用类型I中的值来执行的操作是类型A和B的交集,这些操作用于处理As 以及处理Bs的操作; 我保证的任何东西都是A和B,所以它可以安全地给予任何一种操作.
在使用类似Haskell的类型系统的语言中,这些也不会非常有趣.因为具体类型是不相交的2,所以任何非平凡的交叉都是空的.但同样,类型类约束可以提供类似交集类型的东西; 如果向同一个类型变量添加多个类型类约束,那么在期望该类型变量的地方可以使用的唯一值是所有类型类的"交集"中的类型,以及可以在这些值是适用于任何类型类的操作.
1您可以想象组合操作A -> C和操作B -> D来获取操作(A | B) -> (C | D),就像您可以使用和类型的标记将和类型"路由"到适当的操作一样.但对于完全普遍的联盟类型来说,它变得模糊不清 如果A和B重叠(并且只要你有联合类型,重叠类型就会进入争论),那么你在重叠区域中的某个值上调用哪个操作？如果你可以判断它是A还是B,那么你真的有一个和类型而不是一个联合类型,如果你应用一些任意的解决策略,比如选择A -> C操作,因为A先前在union类型的定义中列出了,那么事情就是在简单的情况下工作正常,但如果你有类型(A | B) & (B | A)(我用它&来表示交集),会变得非常混乱.
2虽然"不相交类型"这一点值得商榷.在类似的类型中,data Maybe a = Nothing | Just a你可以合理地争辩说,Nothing即使是不同的,它也是"相同的价值" a.如果是这样,那么union的Maybe String并集Maybe Integer只包含一个Nothing(而不是两个Nothing都是"无字符串",Nothing那就是"无整数").和交集Maybe String和Maybe Integer仅包含一个值,这个生命Nothing.