리터럴 오버로딩

리터럴 오버로딩 (Literal Overloading)

자연수 (Natural numbers)

기본적으로 자연수 리터럴은 내장 자연수 타입에 매핑돼요. 이는 자연수를 받는 함수에 바인딩되는 FROMNAT 빌트인으로 바꿀 수 있어요:

{-# BUILTIN FROMNAT fromNat #-}

이렇게 하면 fromNat이 스코프 안에 비한정으로 (이름을 바꿨어도) 있을 때 자연수 리터럴 n이 fromNat n으로 desugar돼요.

desugaring이 암시적 인자 삽입 전에 일어나므로 fromNat은 암시적 또는 instance 인자를 몇 개든 가질 수 있다는 점을 주의하세요. 이는 fromNat을 포함하는 타입 클래스를 정의해 오버로드된 리터럴을 지원하는 데 활용할 수 있어요:

module number-simple where

  record Number {a} (A : Set a) : Set a where
    field fromNat : Nat → A

  open Number {{...}} public

{-# BUILTIN FROMNAT fromNat #-}

이 정의는 임의의 자연수를 주어진 타입에 매핑할 수 있어야 하므로 Fin n 같은 타입에는 맞지 않아요. Number 클래스를 추가 제약으로 정제하면 이 문제를 풀 수 있어요:

record Number {a} (A : Set a) : Set (lsuc a) where
  field
    Constraint : Nat → Set a
    fromNat : (n : Nat) {{_ : Constraint n}} → A

open Number {{...}} public using (fromNat)

{-# BUILTIN FROMNAT fromNat #-}

이것이 Agda.Builtin.FromNat에서 사용되는 정의예요.

Nat에 대한 Number instance는 단순히 이렇게 돼요:

instance
  NumNat : Number Nat
  NumNat .Number.Constraint _ = ⊤
  NumNat .Number.fromNat    m = m

Fin n에 대한 Number instance는 다음과 같이 정의할 수 있어요:

_≤_ : (m n : Nat) → Set
zero  ≤ n     = ⊤
suc m ≤ zero  = ⊥
suc m ≤ suc n = m ≤ n

fromN≤ : ∀ m n → m ≤ n → Fin (suc n)
fromN≤ zero    _       _  = zero
fromN≤ (suc _) zero    ()
fromN≤ (suc m) (suc n) p  = suc (fromN≤ m n p)

instance
  NumFin : ∀ {n} → Number (Fin (suc n))
  NumFin {n} .Number.Constraint m         = m ≤ n
  NumFin {n} .Number.fromNat    m {{m≤n}} = fromN≤ m n m≤n

test : Fin 5
test = 3

리터럴의 제약이 자명한 것이 중요해요. 여기서 3 ≤ 5는 ⊤로 평가되고 그 주민은 통일(unification)으로 찾아져요.

표준 라이브러리의 미리 정의된 함수와 instance NumNat을 사용하면 NumFin instance는 간단히 이렇게 돼요:

open import Data.Fin using (Fin; #_)
open import Data.Nat using (suc; _≤?_)
open import Relation.Nullary.Decidable using (True)

instance
  NumFin : ∀ {n} → Number (Fin n)
  NumFin {n} .Number.Constraint m         = True (suc m ≤? n)
  NumFin {n} .Number.fromNat    m {{m<n}} = #_ m {m<n = m<n}

참고: 숫자 리터럴의 오버로딩은 표현식에서만 동작하고 패턴에서는 동작하지 않아요. 다음은 거부돼요:

isZero : ∀ {n} → Fin n → Bool
isZero 0 = true   -- error: zero is not a constructor of the datatype Fin
isZero _ = false

음수 (Negative numbers)

음의 정수 리터럴에는 기본 매핑이 없고 FROMNEG 빌트인을 통해서만 사용할 수 있어요. 이를 함수 fromNeg에 바인딩하면 음의 정수 리터럴 -n이 fromNeg n으로 desugar되는데, 여기서 n은 내장 자연수예요. Agda.Builtin.FromNeg에서:

record Negative {a} (A : Set a) : Set (lsuc a) where
  field
    Constraint : Nat → Set a
    fromNeg : (n : Nat) {{_ : Constraint n}} → A

open Negative {{...}} public using (fromNeg)
{-# BUILTIN FROMNEG fromNeg #-}

문자열 (Strings)

문자열 리터럴은 FROMNAT과 똑같이 동작하는 FROMSTRING 빌트인으로 오버로드돼요. 바인딩되지 않으면 문자열 리터럴은 내장 문자열에 매핑돼요. Agda.Builtin.FromString에서:

record IsString {a} (A : Set a) : Set (lsuc a) where
  field
    Constraint : String → Set a
    fromString : (s : String) {{_ : Constraint s}} → A

open IsString {{...}} public using (fromString)
{-# BUILTIN FROMSTRING fromString #-}

제약 (Restrictions)

현재 정수와 문자열 리터럴만 오버로드할 수 있어요. 오버로딩은 아직 패턴에서 동작하지 않아요.

더 알아보기 (Learn more)