haskell - 强制性和存在主义

Question

data T t where
  A :: Show (t a) => t a -> T t
  B :: Coercible Int (t a) => t a -> T t

f :: T t -> String
f (A t) = show t

g :: T t -> Int
g (B t) = coerce t

为什么 f编译但 g产生如下错误？我正在使用 GHC 8.4。

• Couldn't match representation of type ‘Int’ with that of ‘t a’
  Inaccessible code in
    a pattern with constructor:
      B :: forall k (t :: k -> *) (a :: k).
           Coercible Int (t a) =>
           t a -> T t,
    in an equation for ‘g’
• In the pattern: B t
  In an equation for ‘g’: g (B t) = coerce t

还有， Coercible即使嵌入 GADT 也能实现零成本约束？

UPD:编译器错误: https://ghc.haskell.org/trac/ghc/ticket/15431

Answer 1

作为一种解决方法，您可以用 Data.Type.Coercion.Coercion 替换约束(一开始不是免费的)。 (它在字典周围添加了一个额外的 data 包装器)。

data T t where
  A :: Show (t a) => t a -> T t
  B :: !(Coercion Int (t a)) -> t a -> T t
    -- ! for correctness: you can’t have wishy-washy values like B _|_ (I "a")
    -- Such values decay to _|_
f :: T t -> String
f (A x) = show x
f (B c x) = show (coerceWith (sym c) x)

newtype I a = I a
main = putStrLn $ f $ B Coercion $ I (5 :: Int)

GHC 8.6 将从两个方面改善这种情况:

您的原始代码将起作用，因为底层错误已修复。

Coercion可以解压到Coercible由于-funbox-small-strict-fields，这将自动发生.因此，这个 T将免费获得与您的原始性能相同的性能特征。