내장 타입들

내장 타입들 (Built-ins)

• 내장 타입 사용하기 (Using the built-in types)
• 단위 타입 (The unit type)
• Σ-타입 (The Σ-type)
• 리스트 (Lists)
• Maybe
• 불리언 (Booleans)
• 자연수 (Natural numbers)
• 기계 단어 (Machine words)
• 정수 (Integers)
• 부동소수점 (Floats)
• 문자 (Characters)
• 문자열 (Strings)
• 동등성 (Equality)
• 소트 (Sorts)
• 유니버스 레벨 (Universe levels)
• 크기 타입 (Sized types)
• 공유도 (Coinduction)
• IO
• 리터럴 오버로딩 (Literal overloading)
• 반성 (Reflection)
• 재작성 (Rewriting)
• 정적 값 (Static values)
• 엄격성 (Strictness)

Agda 타입 검사기는 여러 가지 서로 다른 개념에 대해 알고 있고 그것들을 특별하게 취급해. 가장 두드러지는 것은 자연수로, Haskell 정수로의 특별한 표현과 빠른 산술 지원이 있어. 하지만 이런 개념들의 표면 문법은 고정되어 있지 않아서, (예를 들어) 자연수의 특별 취급을 사용하려면 적절한 데이터 타입을 정의한 다음 BUILTIN 프래그마로 그 타입을 자연수 개념에 바인딩해.

일부 내장 타입은 대응하는 Agda 정의가 없는 원시 함수를 지원해. 이 함수들은 primitive 키워드로 타입 시그니처를 주어 선언돼.

내장 타입 사용하기 (Using the built-in types)

내장 타입의 자신만의 버전을 정의하고 BUILTIN 프래그마로 바인딩하는 것이 가능하지만, Agda.Builtin 모듈의 정의를 사용하는 것이 권장돼. 이 모듈들은 Agda를 설치할 때 설치되므로 항상 사용할 수 있어. 예를 들어, 내장 자연수는 Agda.Builtin.Nat에 정의되어 있어. 표준 라이브러리와 agda-prelude는 이 모듈들의 정의를 재수출해.

단위 타입 (The unit type)

module Agda.Builtin.Unit

단위 타입은 다음과 같이 UNIT 내장에 바인딩돼:

record ⊤ : Set where
{-# BUILTIN UNIT ⊤ #-}

Agda는 단위 타입을 알아야 하는데, 반성된 타입 검사 모나드의 원시 연산들 중 일부가 단위 타입의 값을 반환하기 때문이야.

Σ-타입 (The Σ-type)

module Agda.Builtin.Sigma

의존 쌍의 내장 Σ-타입은 다음과 같이 정의돼:

record Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
  constructor _,_

  field
    fst : A
    snd : B fst

open Σ public

infixr 4 _,_

{-# BUILTIN SIGMA Σ #-}

리스트 (Lists)

module Agda.Builtin.List

내장 리스트는 LIST 내장을 사용해 바인딩돼:

data List {a} (A : Set a) : Set a where
  []  : List A
  _∷_ : (x : A) (xs : List A) → List A
{-# BUILTIN LIST List #-}
infixr 5 _∷_

생성자들은 타입을 바인딩할 때 자동으로 바인딩돼. 리스트는 레벨 다형일 필요는 없어; List : Set → Set도 허용돼.

불리언과 마찬가지로, LIST 내장을 바인딩하는 효과는 primStringToList과 primStringFromList 같은 리스트를 다루는 원시 함수를 사용할 수 있게 하고, GHC 백엔드가 List 타입을 Haskell 리스트로 컴파일하도록 알려준다는 것이야.

Maybe

module Agda.Builtin.Maybe

내장 maybe 타입은 MAYBE 내장을 사용해 바인딩돼:

data Maybe {a} (A : Set a) : Set a where
  nothing : Maybe A
  just    : A → Maybe A
{-# BUILTIN MAYBE Maybe #-}

생성자들은 타입을 바인딩할 때 자동으로 바인딩돼. Maybe는 레벨 다형일 필요는 없어; Maybe : Set → Set도 허용돼.

리스트와 마찬가지로, MAYBE 내장을 바인딩하는 효과는 maybe를 다루는 원시 함수를 사용할 수 있게 하고 — 예를 들어 문자열이 비어 있지 않으면 그 head와 tail을 반환하는 primStringUncons — GHC 백엔드가 Maybe 타입을 Haskell maybe로 컴파일하도록 알려준다는 것이야.

불리언 (Booleans)

module Agda.Builtin.Bool where

내장 불리언은 BOOL, TRUE, FALSE 내장을 사용해 바인딩돼:

data Bool : Set where
  false true : Bool
{-# BUILTIN BOOL  Bool  #-}
{-# BUILTIN TRUE  true  #-}
{-# BUILTIN FALSE false #-}

자연수와 달리 생성자들을 별도로 바인딩해야 한다는 점에 주의해. 그 이유는 이름을 마음대로 지을 수 있으므로 Agda가 어떤 생성자가 true에 해당하고 어떤 것이 false에 해당하는지 알 수 없기 때문이야.

불리언 타입을 바인딩하는 효과는 내장 NATEQUALS 같은 불리언을 반환하는 원시 함수를 사용할 수 있게 하고, GHC 백엔드가 그 타입을 Haskell Bool로 컴파일하도록 알려준다는 것이야.

자연수 (Natural numbers)

module Agda.Builtin.Nat

내장 자연수는 NATURAL 내장을 사용해 다음과 같이 바인딩돼:

data Nat : Set where
  zero : Nat
  suc  : Nat → Nat
{-# BUILTIN NATURAL Nat #-}

데이터 타입과 생성자의 이름은 자유롭게 선택할 수 있지만, 데이터 타입의 형태는 위에 주어진 것과 일치해야 해 (생성자의 순서는 예외). 생성자들은 명시적으로 바인딩할 필요가 없다는 점에 주의해.

위와 같이 내장 자연수를 바인딩하면 다음 효과들이 있어:

• 자연수 리터럴의 사용이 활성화돼. 기본적으로 자연수 리터럴의 타입은 Nat이지만, 다른 타입도 포함하도록 오버로드될 수 있어.
• 닫힌 자연수는 컴파일 시점에 Haskell 정수로 표현돼.
• 컴파일러 백엔드는 자연수를 대상 언어의 적절한 숫자 타입으로 컴파일해.
• 아래 설명된 내장 자연수 함수들의 바인딩이 활성화돼.

자연수에 대한 함수 (Functions on natural numbers)

자연수에 대한 내장 함수가 여럿 있어. 이것들은 Agda 정의와 원시 구현 둘 다 가진다는 점에서 특별해. 원시 구현은 닫힌 용어에 대한 적용을 평가하는 데 사용되고, 그 외에는 Agda 정의가 사용돼. 이것은 함수에 대해 증명할 수 있게 하면서도 컴파일 시점 평가의 좋은 성능을 누리게 해줘. 내장 함수들은 다음과 같아:

_+_ : Nat → Nat → Nat
zero  + m = m
suc n + m = suc (n + m)
{-# BUILTIN NATPLUS _+_ #-}

_-_ : Nat → Nat → Nat
n     - zero  = n
zero  - suc m = zero
suc n - suc m = n - m
{-# BUILTIN NATMINUS _-_ #-}

_*_ : Nat → Nat → Nat
zero  * m = zero
suc n * m = (n * m) + m
{-# BUILTIN NATTIMES _*_ #-}

infixl 30 _*_
infixl 20 _+_

_==_ : Nat → Nat → Bool
zero  == zero  = true
suc n == suc m = n == m
_     == _     = false
{-# BUILTIN NATEQUALS _==_ #-}

_<_ : Nat → Nat → Bool
_     < zero  = false
zero  < suc _ = true
suc n < suc m = n < m
{-# BUILTIN NATLESS _<_ #-}

div-helper : Nat → Nat → Nat → Nat → Nat
div-helper k m  zero    j      = k
div-helper k m (suc n)  zero   = div-helper (suc k) m n m
div-helper k m (suc n) (suc j) = div-helper k m n j
{-# BUILTIN NATDIVSUCAUX div-helper #-}

mod-helper : Nat → Nat → Nat → Nat → Nat
mod-helper k m  zero    j      = k
mod-helper k m (suc n)  zero   = mod-helper 0 m n m
mod-helper k m (suc n) (suc j) = mod-helper (suc k) m n j
{-# BUILTIN NATMODSUCAUX mod-helper #-}

Agda 정의는 그것들이 대응하는 내장 함수를 정말로 정의하는지 확인하기 위해 검사돼. 정의가 정확히 위에 주어진 것일 필요는 없어 — 예를 들어 덧셈과 곱셈은 어느 인자에 대한 재귀로도 정의될 수 있고, 곱셈의 재귀 경우에서 덧셈의 인자를 바꿀 수도 있어.

NATDIVSUCAUX와 NATMODSUCAUX는 자연수 나눗셈과 나머지(modulo) 연산을 정의하기 위한 보조 함수를 바인딩하는 내장이며, 다음 속성들을 만족해:

div n (suc m) ≡ div-helper 0 m n m
mod n (suc m) ≡ mod-helper 0 m n m

기계 단어 (Machine words)

module Agda.Builtin.Word
module Agda.Builtin.Word.Properties

Agda는 내장 64비트 기계 단어를 지원하며, WORD64 내장으로 바인딩돼:

postulate Word64 : Set
{-# BUILTIN WORD64 Word64 #-}

기계 단어는 다음 원시들을 사용해 자연수로/로부터 변환할 수 있어:

primitive
  primWord64ToNat   : Word64 → Nat
  primWord64FromNat : Nat → Word64

자연수로 변환하는 것은 자명한 포함(embedding)이고, 자연수에서 변환하는 것은 모듈로 나눈 나머지를 준다. 전자 정리의 증명:

primitive
  primWord64ToNatInjective : ∀ a b → primWord64ToNat a ≡ primWord64ToNat b → a ≡ b

은 Properties 모듈에 있어. 후자 정리의 증명은 원시가 아니며, primTrustMe를 사용해 라이브러리에서 정의할 수 있어.

기본 산술 연산은 자연수로 변환해 대응하는 연산을 수행한 다음 다시 변환함으로써 Word64에 정의할 수 있어. 컴파일러는 이것들을 64비트 산술을 사용하도록 최적화해. 예를 들어:

addWord : Word64 → Word64 → Word64
addWord a b = primWord64FromNat (primWord64ToNat a + primWord64ToNat b)

subWord : Word64 → Word64 → Word64
subWord a b = primWord64FromNat ((primWord64ToNat a + 18446744073709551616) - primWord64ToNat b)

이것들은 64비트 단어에 대한 원시 덧셈과 뺄셈으로 컴파일되는데, GHC 백엔드에서는 Haskell 64비트 단어(Data.Word.Word64)에 대한 연산으로 매핑돼.

정수 (Integers)

module Agda.Builtin.Int

내장 정수는 INTEGER 내장에, 양수용 생성자 하나와 음수용 생성자 하나를 가진 데이터 타입으로 바인딩돼. 생성자에 대한 내장은 INTEGERPOS와 INTEGERNEGSUC이야.

data Int : Set where
  pos    : Nat → Int
  negsuc : Nat → Int
{-# BUILTIN INTEGER       Int    #-}
{-# BUILTIN INTEGERPOS    pos    #-}
{-# BUILTIN INTEGERNEGSUC negsuc #-}

여기서 negsuc n은 정수 -n - 1을 나타내. 자연수와 달리 컴파일 시점에 정수의 특별한 표현은 없는데, Haskell 정수와 비교해 데이터 타입을 사용하는 오버헤드가 그렇게 크지 않기 때문이야.

내장 정수는 다음 원시 연산을 지원해 (String에 대한 적절한 바인딩이 주어지면):

primitive
  primShowInteger : Int → String

부동소수점 (Floats)

module Agda.Builtin.Float
module Agda.Builtin.Float.Properties

부동소수점 숫자는 FLOAT 내장으로 바인딩돼:

postulate Float : Set
{-# BUILTIN FLOAT Float #-}

이것은 부동소수점 리터럴을 사용할 수 있게 해줘. Floats는 타입 검사기에 의해 IEEE 754 binary64 배정밀도 부동소수점으로 표현되며, 정확히 하나의 NaN 값이 있다는 제한이 있어. 다음 원시 함수들이 사용 가능해 (Nat, Bool, String, Int, Maybe _에 대한 적절한 바인딩과 함께):

primitive
  -- Relations
  primFloatIsInfinite        : Float → Bool
  primFloatIsNaN             : Float → Bool
  primFloatIsNegativeZero    : Float → Bool

  -- Conversions
  primNatToFloat             : Nat → Float
  primIntToFloat             : Int → Float
  primFloatToRatio           : Float → (Σ Int λ _ → Int)
  primRatioToFloat           : Int → Int → Float
  primShowFloat              : Float → String

  -- Operations
  primFloatPlus              : Float → Float → Float
  primFloatMinus             : Float → Float → Float
  primFloatTimes             : Float → Float → Float
  primFloatDiv               : Float → Float → Float
  primFloatPow               : Float → Float → Float
  primFloatNegate            : Float → Float
  primFloatSqrt              : Float → Float
  primFloatExp               : Float → Float
  primFloatLog               : Float → Float
  primFloatSin               : Float → Float
  primFloatCos               : Float → Float
  primFloatTan               : Float → Float
  primFloatASin              : Float → Float
  primFloatACos              : Float → Float
  primFloatATan              : Float → Float
  primFloatATan2             : Float → Float → Float
  primFloatSinh              : Float → Float
  primFloatCosh              : Float → Float
  primFloatTanh              : Float → Float
  primFloatASinh             : Float → Float
  primFloatACosh             : Float → Float
  primFloatATanh             : Float → Float

원시 이항 관계들은 그 IEEE 754 등가물을 구현하므로, primFloatEquality는 반사적이지 않고, primFloatInequality와 primFloatLess는 전체(total)가 아니야. (구체적으로 NaN은 자신을 포함해 어떤 것과도 관련되지 않아.)

primFloatIsSafeInteger 함수는 값이 안전 정수(safe integer)인지, 즉 산술 연산이 정밀도를 잃지 않는 범위 안에 있는지 결정해.

부동소수점 숫자는 다음 원시를 사용해 그 원시(raw) 표현으로 변환될 수 있어:

primitive
  primFloatToWord64          : Float → Maybe Word64

이것은 NaN에 대해 nothing을 반환하고 다음을 만족해:

primFloatToWord64Injective : ∀ a b → primFloatToWord64 a ≡ primFloatToWord64 b → a ≡ b

(Properties 모듈에서). 이 원시들은 --safe 옵션으로 안전한 일치 가능한 명제 동등성을 정의하는 데 사용할 수 있어. primFloatToWord64는 백엔드에 걸쳐 일관성을 보장할 수 없으므로, 특정 결과에 의존하는 것은 무정합성(불일치)을 초래할 수 있어.

반올림 연산(primFloatRound, primFloatFloor, primFloatCeiling)은 Maybe Int 타입의 값을 반환하며, NaN이나 무한대에 적용되면 nothing을 반환해:

primitive
  primFloatRound             : Float → Maybe Int
  primFloatFloor             : Float → Maybe Int
  primFloatCeiling           : Float → Maybe Int

primFloatDecode 함수는 부동소수점 숫자를 그 가수(mantissa)와 지수(exponent)로 디코딩하는데, 가수가 가능한 가장 작은 정수가 되도록 정규화해. NaN이나 무한대에 적용되면 실패하며 nothing을 반환해. primFloatEncode 함수는 가수와 지수의 쌍을 부동소수점 숫자로 인코딩해. 결과 숫자를 float로 표현할 수 없으면 실패해. primFloatEncode는 정밀도를 잃을 수 있다는 점에 주의해.

primFloatDecode : Float → Maybe (Σ Int λ _ → Int)
primFloatEncode : Int → Int → Maybe Float

문자 (Characters)

module Agda.Builtin.Char
module Agda.Builtin.Char.Properties

문자 타입은 CHARACTER 내장으로 바인딩돼:

postulate Char : Set
{-# BUILTIN CHAR Char #-}

문자 타입을 바인딩하면 문자 리터럴을 사용할 수 있게 돼. 문자에 대해 다음 원시 함수들이 사용 가능해 (Bool, Nat, String에 대한 적절한 바인딩과 함께):

primitive
  primIsLower    : Char → Bool
  primIsDigit    : Char → Bool
  primIsAlpha    : Char → Bool
  primIsSpace    : Char → Bool
  primIsAscii    : Char → Bool
  primIsLatin1   : Char → Bool
  primIsPrint    : Char → Bool
  primIsHexDigit : Char → Bool
  primToUpper    : Char → Char
  primToLower    : Char → Char
  primCharToNat  : Char → Nat
  primNatToChar  : Nat → Char
  primShowChar   : Char → String

이 함수들은 Data.Char의 대응하는 Haskell 함수로 구현돼 (primCharToNat와 primNatToChar에 대해 각각 ord와 chr). primNatToChar를 전체(total)로 만들기 위해 chr는 자연수에 모듈로 0x110000을 적용해. 게다가 문자열의 동작과 맞추기 위해 서로게이트 코드 포인트는 대체 문자 U+FFFD로 매핑돼.

자연수로 변환하는 것은 명백한 포함이고, 그 증명:

primitive
  primCharToNatInjective : ∀ a b → primCharToNat a ≡ primCharToNat b → a ≡ b

은 Properties 모듈에서 찾을 수 있어.

문자열 (Strings)

module Agda.Builtin.String
module Agda.Builtin.String.Properties

문자열 타입은 STRING 내장으로 바인딩돼:

postulate String : Set
{-# BUILTIN STRING String #-}

문자열 타입을 바인딩하면 문자열 리터럴을 사용할 수 있게 돼. 문자열에 대해 다음 원시 함수들이 사용 가능해 (Bool, Char, List에 대한 적절한 바인딩과 함께):

primitive
  primStringUncons   : String → Maybe (Σ Char (λ _ → String))
  primStringToList   : String → List Char
  primStringFromList : List Char → String
  primStringAppend   : String → String → String
  primStringEquality : String → String → Bool
  primShowString     : String → String

문자열 리터럴은 오버로드될 수 있어.

리스트와의 왕복 변환은 단사적이고, 그 증명들:

primitive
  primStringToListInjective : ∀ a b → primStringToList a ≡ primStringToList b → a ≡ b
  primStringFromListInjective : ∀ a b → primStringFromList a ≡ primStringFromList b → a ≡ b

은 Properties 모듈에서 찾을 수 있어.

문자열은 유니코드 서로게이트 코드 포인트(U+D800부터 U+DFFF 범위의 문자)를 나타낼 수 없어. 이것들은 문자열 리터럴에 나타나면 유니코드 대체 문자 U+FFFD로 대체돼.

동등성 (Equality)

module Agda.Builtin.Equality

항등 타입은 다음과 같이 EQUALITY 내장에 바인딩될 수 있어:

infix 4 _≡_
data _≡_ {a} {A : Set a} (x : A) : A → Set a where
  refl : x ≡ x
{-# BUILTIN EQUALITY _≡_  #-}

이것은 rewrite 구문에서 타입 lhs ≡ rhs의 증명을 사용할 수 있게 해줘.

항등 타입의 다른 변형들도 내장으로 허용돼:

data _≡_ {A : Set} : (x y : A) → Set where
  refl : (x : A) → x ≡ x

primEraseEquality의 타입은 항등 타입의 종류와 일치해야 해.

module Agda.Builtin.Equality.Erase

내장 동등성 타입을 바인딩하면 primEraseEquality 원시도 활성화돼:

primitive
  primEraseEquality : ∀ {a} {A : Set a} {x y : A} → x ≡ y → x ≡ y

이 함수는 두 값 x와 y 사이의 동등성 증명을 받아, x와 y가 실제로 정의적으로 같아질 때까지 그것에 막혀(stuck) 있어. 그런 경우에는 primEraseEquality e가 refl로 축약돼.

primEraseEquality의 용도 중 하나는 (예를 들어 반성에 의한) 비용이 드는 함수로 계산된 동등성 증명을 대각선에서 자명하게 refl인 것으로 대체하는 것이야.

primTrustMe

module Agda.Builtin.TrustMe

primEraseEquality 원시로부터 primTrustMe 개념을 유도할 수 있어:

primTrustMe : ∀ {a} {A : Set a} {x y : A} → x ≡ y
primTrustMe {x = x} {y} = primEraseEquality unsafePrimTrustMe
  where postulate unsafePrimTrustMe : x ≡ y

타입에서 볼 수 있듯이, primTrustMe는 무정합성(불일치)을 피하기 위해 극도로 주의해서 사용해야 해. 그것을 포스툴레이트와 다르게 만드는 것은 x와 y가 실제로 정의적으로 같으면 primTrustMe가 refl로 축약된다는 것이야. primTrustMe의 용도 중 하나는 String 같은 내장 타입에 대한 원시 불리언 동등성을 증명 객체를 반환하는 것으로 끌어올리는 것이야:

eqString : (a b : String) → Maybe (a ≡ b)
eqString a b = if primStringEquality a b
               then just primTrustMe
               else nothing

이 정의로 eqString "foo" "foo"는 just refl로 계산돼.

소트 (Sorts)

Agda 타입 시스템에 사용되는 원시 소트들은 Agda.Primitive 모듈에서 BUILTIN 프래그마로 선언돼. 이 프래그마들은 다른 모듈에서 직접 사용해서는 안 되지만, Agda.Primitive를 임포트할 때 이 내장 소트들을 이름 바꿀 수는 있어.

{-# BUILTIN PROP           Prop      #-}
{-# BUILTIN TYPE           Set       #-}
{-# BUILTIN STRICTSET      SSet      #-}

{-# BUILTIN PROPOMEGA      Propω     #-}
{-# BUILTIN SETOMEGA       Setω      #-}
{-# BUILTIN STRICTSETOMEGA SSetω     #-}

{-# BUILTIN LEVELUNIV      LevelUniv #-}

원시 소트 Set은 --no-import-sorts 플래그가 활성화되지 않는 한, 모든 최상위 Agda 모듈의 맨 위에 자동으로 임포트돼.

유니버스 레벨 (Universe levels)

module Agda.Primitive

유니버스 레벨도 BUILTIN 프래그마로 선언돼. Agda.Builtin 모듈들과 대조적으로 Agda.Primitive 모듈은 자동 임포트되므로 레벨 내장들을 바꾸는 것은 불가능해. 참고로 다음이 그 바인딩들이야:

postulate
  Level : LevelUniv
  lzero : Level
  lsuc  : Level → Level
  _⊔_   : Level → Level → Level

{-# BUILTIN LEVEL     Level #-}
{-# BUILTIN LEVELZERO lzero #-}
{-# BUILTIN LEVELSUC  lsuc  #-}
{-# BUILTIN LEVELMAX  _⊔_   #-}

--level-universe 플래그가 설정되지 않으면 LevelUniv은 Set이 된다는 점에 주의해.

크기 타입 (Sized types)

module Agda.Builtin.Size

크기 타입에 대한 내장들은 이름이 BUILTIN 프래그마에 의해 정의된다는 점에서 다른 내장들과 달라. 따라서 크기 원시들을 바인딩하려면 다음만 쓰면 돼:

{-# BUILTIN SIZEUNIV SizeUniv #-}  --  SizeUniv : SizeUniv
{-# BUILTIN SIZE     Size     #-}  --  Size     : SizeUniv
{-# BUILTIN SIZELT   Size<_   #-}  --  Size<_   : ..Size → SizeUniv
{-# BUILTIN SIZESUC  ↑_       #-}  --  ↑_       : Size → Size
{-# BUILTIN SIZEINF  ∞        #-}  --  ∞        : Size
{-# BUILTIN SIZEMAX  _⊔ˢ_     #-}  --  _⊔ˢ_     : Size → Size → Size

공유도 (Coinduction)

module Agda.Builtin.Coinduction

다음 내장들이 공유도적(coinductive) 정의에 사용돼:

postulate
  ∞  : ∀ {a} (A : Set a) → Set a
  ♯_ : ∀ {a} {A : Set a} → A → ∞ A
  ♭  : ∀ {a} {A : Set a} → ∞ A → A
{-# BUILTIN INFINITY ∞  #-}
{-# BUILTIN SHARP    ♯_ #-}
{-# BUILTIN FLAT     ♭  #-}

더 자세한 내용은 공유도(Coinduction)를 참조해.

IO

module Agda.Builtin.IO

내장 IO 타입을 바인딩하는 유일한 목적은 Agda가 main 함수가 올바른 타입을 가지는지 확인하게 하는 것이야 (컴파일러(Compilers) 참조).

postulate IO : Set → Set
{-# BUILTIN IO IO #-}

리터럴 오버로딩 (Literal overloading)

module Agda.Builtin.FromNat
module Agda.Builtin.FromNeg
module Agda.Builtin.FromString

리터럴 오버로딩을 위한 장치는 변환 함수에 대한 내장들을 사용해.

반성 (Reflection)

module Agda.Builtin.Reflection

반성 장치는 Agda 프로그램을 나타내기 위한 내장 타입들을 가져. 자세한 설명은 반성(Reflection)을 참조해.

재작성 (Rewriting)

실험적이고 완전히 안전하지 않은 재작성 장치(rewrite 구문과 혼동해서는 안 됨)는 재작성 관계에 대한 내장 REWRITE를 가져:

postulate _↦_ : ∀ {a} {A : Set a} → A → A → Set a
{-# BUILTIN REWRITE _↦_ #-}

이 내장은 Agda.Builtin.Equality.Rewrite에서 Agda.Builtin.Equality의 내장 동등성 타입에 바인딩돼.

정적 값 (Static values)

STATIC 프래그마는 컴파일 전에 정규화되어야 할 정의를 표시하는 데 사용할 수 있어. 대표적인 사용 사례는 내장 언어(embedded language)의 인터프리터를 STATIC으로 표시하는 것이야:

{-# STATIC <Name> #-}

엄격성 (Strictness)

module Agda.Builtin.Strict

평가 순서를 제어하는 두 개의 원시가 있어:

primitive
  primForce      : ∀ {a b} {A : Set a} {B : A → Set b} (x : A) → (∀ x → B x) → B x
  primForceLemma : ∀ {a b} {A : Set a} {B : A → Set b} (x : A) (f : ∀ x → B x) → primForce x f ≡ f x

여기서 _≡_는 내장 동등성이야. 컴파일 시점에 x가 약한 헤드 정규형(whnf)에 있으면, 즉 다음 중 하나이면 primForce x f는 f x로 평가돼:

• 생성자 적용
• 리터럴
• 람다 추상화
• 타입 생성자 적용 (데이터 또는 레코드 타입)
• 함수 타입
• 유니버스 (Set _)

마찬가지로 primForceLemma x f는 primForce를 사용하는 프로그램에 대해 추론하게 해주며, x가 whnf에 있으면 refl로 평가돼. 런타임에 primForce e f는 (GHC 백엔드에 의해) let x = e in seq x (f x)로 컴파일돼.

예를 들어 다음 함수를 고려해 보자:

-- pow’ n a = a 2ⁿ
pow’ : Nat → Nat → Nat
pow’ zero    a = a
pow’ (suc n) a = pow’ n (a + a)

여기 (컴파일 시점과 런타임 평가 모두에서) 평가되지 않은 a + a 썽크(thunk)에 의한 공간 누수가 있어. 이 문제는 primForce로 고칠 수 있어:

infixr 0 _$!_
_$!_ : ∀ {a b} {A : Set a} {B : A → Set b} → (∀ x → B x) → ∀ x → B x
f $! x = primForce x f

-- pow n a = a 2ⁿ
pow : Nat → Nat → Nat
pow zero    a = a
pow (suc n) a =  pow n $! a + a

더 알아보기 (Learn more)

• Agda 문서: built-ins 원문