单例参数的专业化

Question

我在玩单身人士的专业化：

{-# LANGUAGE DataKinds      #-}
{-# LANGUAGE GADTs          #-}
{-# LANGUAGE KindSignatures #-}
module Data.Test where
data SingBool (b :: Bool) where
STrue :: SingBool 'True
SFalse :: SingBool 'False
sing :: SingBool b -> Bool
sing SFalse = False
sing STrue  = True
{-# SPECIALIZE sing :: SingBool 'False -> Bool #-}

这专门针对以下内容：

singSFalse :: SingBool 'False -> Bool
singSFalse SFalse = False

我希望它能生成singSFalse _ = False的 RHS。

解压缩强制只是为了满足类型检查器，还是该模式匹配涉及实际的运行时开销？我想GHC不会为了不增加懒惰而丢弃参数上的模式匹配来解释bottom。但我想在开始通过Proxy+SingI样式类型类对此进行建模之前确定这一点。

Answer 1

好的，主要回答我自己的问题：知道SingBool 'False只有一个居民不足以让 GHC 摆脱模式匹配，因为我们可以像singSFalse (error "matched")一样调用函数，例如底部总是另一个居民。

因此，专业化(例如基于具体TypeApplication的内联(并不能很好地与Haskell(懒惰，非全域(w.r.t.零成本抽象中的单例(将这些类型应用程序转换为大概的常量值应用程序(一起使用。

但是，通过使用带有代理的SingI样式类型类(例如singByProxy(，我们没有同样的问题：

{-# LANGUAGE DataKinds      #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MagicHash      #-}
module Data.Test where
import           GHC.Exts (Proxy#)
class SingIBool (b :: Bool) where
sing :: Proxy# b -> Bool
instance SingIBool 'False where
sing _ = False
instance SingIBool 'True where
sing _ = True
refurbulate :: SingIBool b => Proxy# b -> Int
refurbulate p
| sing p = 0
| otherwise = 1

专业化refurbulate @(Proxy# 'False)不仅会像const False那样实现，也不会在值级别传递任何Proxy#参数，所以它相当coerce False :: Proxy# -> Bool。整洁！但是，我无法在现实世界中使用单例:(

---

回顾为什么单例失败(以获得优化(并且类型类工作：

通过专门化类型类实例，我们了解了sing的 RHS，从中我们可以推导出整体性。

通过专用于单例，我们可以知道如果评估终止，参数的计算值是多少。

知道类型类方法x :: ()的规范 RHS 比仅仅知道参数x :: ()只能在非全的、惰性(例如 Haskell 的(设置中计算到一个值更有信息量。