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代码不同，显然有实际是一些开销，但这个问题似乎是固定的头。