Impredicative类型与普通旧的子类型

Question

我的一个朋友上周提出了一个看似无害的Scala语言问题,我没有得到一个好的答案:是否有一种简单的方法来声明属于某些常见类型类的东西的集合.当然,Scala中没有关于"类型类"的一流概念,因此我们必须从特征和上下文界限(即暗示)来考虑这一点.

具体地说,给定一些T[_]表示类型类型和类型的特征A,B并且C在范围内具有相应的含义T[A],T[B]并且T[C],我们希望声明类似于a的东西List[T[a] forAll { type a }],我们可以在其中抛出实例A,B并且C不受惩罚.这当然在Scala中不存在; 去年的一个问题更深入地讨论了这个问题.

自然的后续问题是"Haskell如何做到这一点？" 那么,GHC尤其具有称为impredicative polymorphism的类型系统扩展,在"Boxy Types"论文中有所描述.简而言之,给定一个类型类,T可以合法地构建一个列表[forall a. T a => a].给定这种形式的声明,编译器会执行一些字典传递魔术,它允许我们在运行时保留与列表中每个值的类型相对应的类型类实例.

事实是,"字典传递魔法"听起来很像"vtables".在像Scala这样的面向对象语言中,子类型是一种比"Boxy类型"方法更简单,更自然的机制.如果我们的A,B以及C所有延伸的特性T,那么我们可以简单地宣布List[T]并且快乐.同样,作为万里注意到,在评论下面,如果他们都继承特质T1,T2并且T3然后我可以使用List[T1 with T2 with T3]作为等同于impredicative哈斯克尔[forall a. (T1 a, T2 a, T3 a) => a].

但是,主,知名与亚型相比,类型类的缺点是紧耦合:我A,B和C类型都让他们的T行为出炉让我们假设这是一个重要的因素在于,和我.不能使用子类型.因此,在斯卡拉的中间地带是皮条客^ H ^ H ^ H ^ H ^ Himplicit转换:给出了一些A => T,B => T并C => T在隐范围,我又可以很愉快地填充List[T]与我A,B和C值...

......直到我们想要List[T1 with T2 with T3].在这一点上,即使我们有隐式转换A => T1,A => T2并且A => T3,我们不能把一个A到列表中.我们可以重构我们隐含的转换以实际提供A => T1 with T2 with T3,但我以前从未见过任何人这样做过,而且它似乎是另一种形式的紧密耦合.

好吧,所以我的问题最终是,我想,这是之前在这里提出的几个问题的组合:"为什么要避免使用子类型？" 和"对类型类别进行子类型化的优势" ...是否有一些统一的理论认为不可预测的多态性和亚型多态性是同一个？隐含的转换是不是两个人的秘密爱情孩子？并且有人可以在Scala中表达一个好的,干净的模式来表达多个边界(如上面的最后一个例子)吗？

Answer 1

你会将具有存在主义类型的impredicative类型混淆.Impredicative类型允许您将多态值放在数据结构中,而不是任意具体的值.换句话说,[forall a. Num a => a]意味着您有一个列表,其中每个元素都可以作为任何数字类型工作,因此您不能将eg Int和Doubletype [forall a. Num a => a]放在类型列表中,但是您可以0 :: Num a => a在其中放置类似的内容.Impredicative类型不是你想要的.

你想要的是存在类型,即[exists a. Num a => a](不是真正的Haskell语法),它表示每个元素都是一些未知的数字类型.但是,要在Haskell中编写它,我们需要引入一个包装器数据类型:

data SomeNumber = forall a. Num a => SomeNumber a

请注意从更改exists到forall.那是因为我们正在描述构造函数.我们可以把任何数值类型中,但随后类型系统"忘记"该类型是.一旦我们把它取回(通过模式匹配),我们所知道的是它是一些数字类型.在SomeNumber幕后发生的是,类型包含一个隐藏字段,它存储类型类字典(又名.vtable/implicit),这就是我们需要包装器类型的原因.

现在我们可以使用类型[SomeNumber]作为任意数字的列表,但是我们需要在路上包装每个数字,例如[SomeNumber (3.14 :: Double), SomeNumber (42 :: Int)].查找每种类型的正确字典,并在我们包装每个数字的位置自动存储在隐藏字段中.

存在类型和类型类的组合在某些方面类似于子类型,因为类型类和接口之间的主要区别在于类型类vtable与对象分开传播,而存在类型将对象和vtable再次组合在一起.

但是,与传统的子类型不同,您不必强制将它们一对一配对,因此我们可以编写这样的内容,将一个vtable与两个相同类型的值打包在一起.

data TwoNumbers = forall a. Num a => TwoNumbers a a

f :: TwoNumbers -> TwoNumbers
f (TwoNumbers x y) = TwoNumbers (x+y) (x*y)

list1 = map f [TwoNumbers (42 :: Int) 7, TwoNumbers (3.14 :: Double) 9]
-- ==> [TwoNumbers (49 :: Int) 294, TwoNumbers (12.14 :: Double) 28.26]

甚至更高档的东西.一旦我们在包装器上进行模式匹配,我们就会回到类型类的土地上.虽然我们不知道哪种类型的x和y是,我们知道他们是一样的,我们必须提供给他们进行数字运算正确的字典.

上面的所有内容与多个类型类似.编译器将在每个vtable的包装器类型中生成隐藏字段,并在模式匹配时将它们全部放入范围.

data SomeBoundedNumber = forall a. (Bounded a, Num a) => SBN a

g :: SomeBoundedNumber -> SomeBoundedNumber
g (SBN n) = SBN (maxBound - n)

list2 = map g [SBN (42 :: Int32), SBN (42 :: Int64)]
-- ==> [SBN (2147483605 :: Int32), SBN (9223372036854775765 :: Int64)]

因为我对Scala来说是一个初学者,我不确定我能帮助解决你问题的最后部分,但我希望这至少可以解决一些困惑并给你一些关于如何思考的想法继续.