專業單參數

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 + a SingI-樣式類型開始建模之前，我很確定。

Answer 1

好的，主要回答我自己的問題：知道SingBool 'False只有一個居民是不足以讓GHC擺脫模式匹配的，因爲我們可以稱之爲singSFalse (error "matched")，例如singSFalse (error "matched")。底部永遠是另一個居民。因此，專門化（例如基於具體的內聯TypeApplication s的內聯）在Haskell（惰性，非全部）w.r.t中並不能很好地處理singletons（將這些類型的應用程序轉化爲可能是常量值的應用程序）。零成本抽象。

然而，通過使用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 ::()只能計算非整數，懶惰（例如，非整數）值中的一個值更具信息性。哈斯克爾）的設置。