类型等式约束和多态性

Posted 2023-03-06

【中文标题】类型等式约束和多态性

【英文标题】：Type equality constraints and polymorphism

【发布时间】：2021-01-01 16:53:25

【问题描述】：

等式约束的确切语义是什么？这两种类型完全等价吗？

f :: Int -> IO [T]
g :: (a ~ T) => Int -> IO [a]

g 是只对 T 有效的单态函数还是多态函数？它看起来很单态，但编译器会像f 那样处理它吗？ GHC 用户指南section on equality constraints 没有讨论实现细节。

我似乎记得多态函数可能需要 INLINEABLE 或 SPECIALIZE pragma 来启用所有优化，并且使事情不必要地多态可能会产生运行时成本。 g 是否也是这种情况，或者 GHC 会更好地了解并立即简化它吗？或者，这取决于？

【参考方案1】：

嗯，这些类型肯定不是完全等价的。

类型检查器认为它们是不同的类型。如果你用-ddump-types 编译，你会看到：

TYPE SIGNATURES
  f :: Int -> IO [Double]
  g :: forall a. (a ~ Double) => Int -> IO [a]

这两种类型在编译时的行为也不同。例如，对于 TypeApplications 扩展，g @Double 10 是一个有效的表达式，而 f @Double 10 不是。

在核心中，等式约束被实现——就像所有约束一样——作为一个额外的字典参数，您会在生成的核心中看到这种类型的差异。特别是，如果您编译以下程序：

-# LANGUAGE GADTs #-

module EqualityConstraints where

import Control.Monad

f :: Int -> IO [Double]
f n = replicateM n readLn

g :: (a ~ Double) => Int -> IO [a]
g n = replicateM n readLn

与：

ghc -ddump-types -ddump-simpl -dsuppress-all -dsuppress-uniques \
    -fforce-recomp EqualityConstraints.hs

您会看到如下所示的核心：

-- RHS size: terms: 12, types: 22, coercions: 3, joins: 0/0
g = \ @ a $d~ eta ->
      case eq_sel $d~ of co  __DEFAULT ->
      replicateM
        $fApplicativeIO eta (readLn ($fReadDouble `cast` <Co:3>))
      

-- RHS size: terms: 6, types: 4, coercions: 0, joins: 0/0
f = \ n -> replicateM $fApplicativeIO n (readLn $fReadDouble)

即使使用-O2，这种差异也会在核心中持续存在。

确实，如果您阻止内联，最终的核心（甚至最终的 STG）将涉及一些不必要的字典传递，您可以通过以下方式看到：

-# LANGUAGE GADTs #-

import Control.Monad

f :: Int -> IO [Double]
-# NOINLINE f #-
f n = replicateM n readLn

g :: (a ~ Double) => Int -> IO [a]
-# NOINLINE g #-
g n = replicateM n readLn

main = do
  f 2
  g 2

并使用-ddump-simpl 和-ddump-stg 进行编译。

据我所知，即使在-O2 的优化程序集中，这种差异仍然可见。

所以，我认为可以肯定地说，g 已被充分多态地处理，以至于关于不必要的多态性的运行时成本的警告确实适用。

【讨论】：

非常有趣，谢谢！我有点希望它会是一样的 :) 现在我想知道 GHC 是否没有采用一些低悬的优化路径。

哇！我的印象是编译版本中完全没有强制（因为，毕竟，除了在类型检查器中，它们实际上没有做任何事情，这也完全没有......对吗？）。

@DanielWagner Casting 和 coersions 似乎是 Core 的一部分，因此它们应该一直存在，直到转换为 STG。事实上，我在-ddump-stg 的输出中看不到它们。

【参考方案2】：

一个很大的区别是在类型类中使用此类约束。

class F a where f :: Int -> IO [a]
instance F Int where f n = pure [1,2,3]
instance (a ~ Int) => F a where f n = pure [1,2,3]

如果您使用第二个实例声明，您将无法创建任何其他实例，因为尽管有约束，所有类型都将与 a 统一。

【讨论】：

是的，这是 Haskell 中的成人仪式之一。几乎每个人都会被这个咬伤。甚至多次，根据我自己的经验：) 将约束视为考虑实例的必要先决条件太诱人了，这不是实例解析的工作原理。

这最终成为在某些情况下控制类型推断的非常有用的技巧。只有当编译器已经确定类型参数是Int 时，才能选择第一个实例（如果不确定，它将放弃关于不明确类型变量的错误）。当编译器还不确定时，可以使用第二个实例，然后使其变为确定（正是因为不可能有任何其他实例），并使用该信息来在别处解析类型。

chrisdone.com/posts/haskell-constraint-trick