GHC TypeLits開銷

Question

使用Sing從GHC.TypeLits是否有任何開銷？例如，對於該程序：

{-# LANGUAGE DataKinds #-} 

module Test (test) where 

import GHC.TypeLits 

test :: Integer 
test = fromSing (sing :: Sing 5) 

GHC生成核心代碼：

Test.test1 :: GHC.Integer.Type.Integer 
[GblId, 
Str=DmdType, 
Unf=Unf{Src=<vanilla>, TopLvl=True, Arity=0, Value=True, 
     ConLike=True, WorkFree=True, Expandable=True, 
     Guidance=IF_ARGS [] 100 0}] 
Test.test1 = __integer 5 

Test.test :: GHC.Integer.Type.Integer 
[GblId, 
Str=DmdType, 
Unf=Unf{Src=<vanilla>, TopLvl=True, Arity=0, Value=True, 
     ConLike=True, WorkFree=True, Expandable=True, 
     Guidance=ALWAYS_IF(unsat_ok=True,boring_ok=True)}] 
Test.test = 
    Test.test1 
    `cast` (<GHC.TypeLits.NTCo:SingI> <GHC.TypeLits.Nat> <5> ; (<GHC.TypeLits.TFCo:R:SingNatn 
                   <5>> ; <GHC.TypeLits.NTCo:R:SingNatn 
                      <5>>) 
      :: GHC.TypeLits.SingI GHC.TypeLits.Nat 5 
       ~# 
      GHC.Integer.Type.Integer) 

這是代碼的等效和Test.test = __integer 5值將在編譯時被計算或不？

Answer 1

是的，這相當於Test.test = __integer 5，該cast部分只是類型的系統噪音（你可以看到它在紙"System F with Type Equality Coercions"馬丁Sulzmann，曼努埃爾·M. T. Chakravarty，西蒙佩頓瓊斯和凱文·唐納利表示）。相關報價：

角色表達式沒有操作效果，但它們用於 解釋的類型系統時一種類型的值應被視爲 作爲另一個。

編輯：其實，與GHC 7.6 assembly code爲test = fromSing (sing :: Sing 5)是從test = 5代碼不同，顯然有實際是一些開銷，但這個問題似乎是固定的頭。