GHC TypeLits overhead

Question

Có chi phí sử dụng Sing từ GHC.TypeLits không? Ví dụ đối với các chương trình:

{-# LANGUAGE DataKinds #-} 

module Test (test) where 

import GHC.TypeLits 

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

GHC tạo mã lõi:

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) 

là mã này tương đương với Test.test = __integer 5 và giá trị sẽ được tính tại thời gian biên dịch hay không?

Answer 1

Có, đây là tương đương với Test.test = __integer 5, phần cast chỉ là loại hệ thống tiếng ồn (bạn có thể đọc về ý nghĩa của nó trong giấy "System F with Type Equality Coercions" bởi Martin Sulzmann, Manuel M. T. Chakravarty, Simon Peyton Jones và Kevin Donnelly). quote liên quan:

biểu Cast không có hoạt động hiệu lực, nhưng họ phục vụ để giải thích cho các hệ thống kiểu khi một giá trị của một loại cần được điều trị như nhau.

Edit: Trên thực tế, với GHC 7,6 các assembly code cho test = fromSing (sing :: Sing 5) khác với mã cho test = 5 và dường như có thực sự là một số phí, nhưng vấn đề này dường như được cố định trong HEAD.