类型相等约束和多态性

Question

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

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

g是单态函数还是多态函数，恰好只对T有效？它看起来很单调，但编译器会像f一样处理它吗？GHC关于平等约束的用户指南部分没有讨论实施细节。

我似乎记得多态函数可能需要INLINEABLE或SPECIALIZE杂注来启用所有优化，并且使不必要的多态性可能会产生运行时成本。这里的g也会是这样吗？或者GHC会更清楚并立即简化它吗？或者，这取决于情况？

Answer 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)

并且即使使用CCD_ 8，这种差异也将在核心中持续存在。

事实上，如果您阻止内联，那么最终的核心(甚至最终的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

并用CCD_ 9和CCD_。

据我所见，即使在使用-O2的优化装配中，这种差异仍然可见。

因此，我认为可以肯定地说，g得到了足够的多态性处理，关于不必要多态性的运行时成本的警告确实适用。

Answer 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]

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