7

GHC.TypeLitsSingから使用するオーバーヘッドはありますか? たとえば、プログラムの場合：

{-# 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あり、値はコンパイル時に計算されますか?

4

1 に答える 1

3

はい、これは と同等です。このTest.test = __integer 5部分は単なる型システム ノイズです (その意味については、Martin Sulzmann、Manuel MT Chakravarty、Simon Peyton Jones、Kevin Donnelly による論文「System F with Type Equality Coercions」castで読むことができます)。関連する引用:

キャスト式は操作上の効果はありませんが、ある型の値を別の型として扱う必要がある場合に型システムに説明するのに役立ちます。

編集:実際には、GHC 7.6 のアセンブリ コードは のコードとtest = fromSing (sing :: Sing 5)は異なり、test = 5実際にはオーバーヘッドがあるようですが、この問題は HEAD で修正されているようです。

于 2013-09-26T17:51:57.223 に答える