GHC TypeLits开销

从GHC.TypeLits使用Sing有什么开销？ 例如对于该程序：

{-# 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并且值是否会在编译时计算？

---

是的，这相当于Test.test = __integer 5 ， cast角色只是输入系统噪音（您可以阅读Martin Sulzmann，Manuel MT Chakravarty，Simon Peyton在论文“System F with Type Equality Coercions”琼斯和凯文唐纳利）。 相关报价：

Cast表达式没有任何操作效果，但它们用于向类型系统解释何时应将一种类型的值视为另一种类型的值。

编辑：其实，与GHC 7.6汇编代码test = fromSing (sing :: Sing 5)是从代码不同的test = 5 ，显然有实际上是一些开销，但这个问题似乎是固定的头。

链接地址: http://www.djcxy.com/p/16127.html

上一篇: GHC TypeLits overhead

下一篇: How to change android version and code version number in Android Studio?