类型相等约束和多态性

Question

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

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

是g单态函数还是多态函数，碰巧只适用于 T？它看起来很单态，但编译器会像这样处理f吗？关于等式约束的 GHC 用户指南部分没有讨论实现细节。

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

Answer 1

嗯，这些类型当然不完全相同。

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

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

这两种类型在编译时的行为也不同。例如，对于TypeApplications扩展名，g @Double 10is 是一个有效的表达式，而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它被充分多态地处理，以至于关于不必要的多态性的运行时成本的警告确实适用。