Pea*_*ker 16 polymorphism haskell types type-systems
由于类型变量不能保存多类型,因此使用Rank*Types似乎不能重复使用现有函数,因为它们具有monotype限制.
例如,当中间类型是多类型时,我们不能使用函数(.).我们被迫在现场重新实施(.).这对于(.)来说当然是微不足道的,但对于更多实体代码来说却是一个问题.
我还认为((f.g)x)不等于(f(gx))对参考透明度及其益处的严重打击.
在我看来,这是一个显示停止问题,并且似乎使Rank*Types扩展几乎不适合广泛使用.
我错过了什么吗？是否有计划使Rank*Types与类型系统的其他部分更好地交互？
编辑:你如何使(runST.永远)的类型工作？
nom*_*olo 11
Rank-N类型的最新提议是Don的链接FPH论文.在我看来,它也是最好的一群.所有这些系统的主要目标是要求尽可能少的类型注释.问题是当从Hindley/Milner转到System F时,我们失去了主要类型,类型推断变得不可判定 - 因此需要类型注释.
"boxy类型"工作的基本思想是尽可能地传播类型注释.类型检查器在类型检查和类型推断模式之间切换,希望不再需要注释.这里的缺点是,是否需要类型注释很难解释,因为它取决于实现细节.
Remy的MLF系统是迄今为止最好的提议; 它需要最少量的类型注释,并且在许多代码转换下是稳定的.问题是它扩展了类型系统.以下标准示例说明了这一点:
choose :: forall a. a -> a -> a
id :: forall b. b -> b
choose id :: forall c. (c -> c) -> (c -> c)
choose id :: (forall c. c -> c) -> (forall c. c -> c)
以上两种类型都可以在System F中使用.第一种是标准的Hindley/Milner类型并使用预测实例化,第二种使用impredicative instantiation.这两种类型都不比另一种类型更通用,因此类型推断必须猜测用户想要哪种类型,这通常是一个坏主意.
MLF改为使用有限量化扩展系统F. 上例中的主要(=最一般)类型是:
choose id :: forall (a < forall b. b -> b). a -> a
你可以阅读此为" choose id已输入a到a其中a必须的一个实例forall b. b -> b."
有趣的是,仅凭这一点并不比标准的欣德利/米尔纳更强大.因此,MLF还允许严格的量化.以下两种类型是等效的:
(forall b. b -> b) -> (forall b. b -> b)
forall (a = forall b. b -> b). a -> a
通过类型注释引入刚性量化,技术细节确实非常复杂.好处是MLF只需要很少的类型注释,并且在需要它们时有一个简单的规则.缺点是:
类型可能变得难以阅读,因为"<"的右侧可以包含进一步的嵌套量化.
直到最近,还没有明确键入的MLF变体.这对于类型化编译器转换非常重要(如GHC一样).Boris Yakobowski博士论文的第3部分首次尝试了这种变体.(第1部分和第2部分也很有趣;它们通过"图形类型"描述了MLF的更直观表示.)
回到FPH,它的基本思想是在内部使用MLF技术,但需要在let绑定上使用类型注释.如果您只想要Hindley/Milner类型,则无需注释.如果您需要更高级别的类型,则需要指定所请求的类型,但仅限于let(或顶级)绑定.
FPH(像MLF)支持impredicative实例化,所以我不认为你的问题适用.因此,在f . g上面输入您的表达式应该没有问题.然而,FPH尚未在GHC中实施,而且很可能不会.困难来自与平等强制的相互作用(以及可能的类型约束).我不确定最新的状态是什么,但我听说SPJ希望摆脱不可靠性.所有那些富有表现力的动力都需要付出代价,到目前为止还没有找到经济实惠且随附的解决方案.
是否有计划使Rank*Types与类型系统的其他部分更好地交互？
鉴于ST monad有多常见,至少Rank2类型足以证明相反.但是,你可能会看一下"性感/四四方方的类型"系列论文,了解如何使任意等级多态性与其他方法更好地发挥作用.
FPH:Haskell的一流多态性,Dimitrios Vytiniotis,Stephanie Weirich和Simon Peyton Jones,提交给ICFP 2008.
另请参阅-XImpredicativeTypes - 有趣的是,它将被弃用!
小智 6
关于ImpredicativeTypes:这实际上并没有对peaker的问题产生影响(我相对肯定).该扩展与数据类型有关.例如,GHC会告诉你:
Maybe :: * -> *
(forall a. a -> a) :: *
然而,这有点谎言.在一个不可预测的系统中是这样,在这样的系统中,你可以写:
Maybe (forall a. a -> a) :: *
它会工作正常.这就是ImpredicativeTypes所启用的.没有扩展,考虑这个的适当方式是:
Maybe :: *m -> *m
(forall a :: *m. a -> a) :: *p
因此,当您尝试构建上述应用程序时,存在一种不匹配.
尽管如此,GHC在不确定性方面还是相当不一致的.例如,id我上面给出的类型是:
id :: (forall a :: *m. a -> a)
但GHC很乐意接受注释(启用了RankNTypes,但没有ImpredicativeTypes):
id :: (forall a. a -> a) -> (forall a. a -> a)
即使forall a. a -> a不是一个典型的.因此,它将允许对量化变量进行不可预测的实例化,这些变量仅(->)在您注释时才使用.但我想,它不会自己做,这会导致runST $ ...问题.过去通过临时实例化规则来解决(我从未特别明确过去的详细信息),但该规则在添加后不久就被删除了.