문법 설탕

문법 설탕 (Syntactic Sugar)

이 문서에서는 다음 주제를 다뤄요:

• 숨은 인자 언어유희(Hidden argument puns)
• do 표기법 (Do-notation)
  • Desugaring
  • 예제
• 관용구 괄호 (Idiom brackets)

숨은 인자 언어유희 (Hidden argument puns)

--hidden-argument-puns 옵션을 사용하면, 패턴 {x}는 {x = x}로 해석되고, 패턴 ⦃ x ⦄는 ⦃ x = x ⦄로 해석돼요. 여기서 x는 스코프 안에 있는 생성자를 가리키지 않는 비한정(unqualified) 이름이어야 해요: x가 한정(qualified)되면 패턴은 언어유희로 해석되지 않고, x가 비한정이면서 스코프 안의 생성자를 가리키면 코드가 거부돼요.

{(x)}와 ⦃ (x) ⦄는 언어유희로 해석되지 않는다는 점에 주의하세요.

또한 {x}는 λ {x} → … 또는 syntax f {x} = …에서 언어유희로 해석되지 않아요. 하지만 λ (c {x}) → …에서는 {x}가 언어유희로 해석돼요.

Do 표기법 (Do-notation)

do 블록은 레이아웃 키워드 do와 그 뒤에 오는 일련의 do 문장으로 구성돼요:

do-stmt    ::= pat ← expr [where lam-clauses]
             | let decls
             | expr
lam-clause ::= pat → expr

바인드의 where 절은 화살표 왼쪽의 패턴이 매칭하지 못하는 경우를 처리하는 데 사용돼요. 아래에서 자세히 설명할게요.

참고: 화살표는 유니코드(←/→) 또는 ASCII(<-/->) 변형을 사용할 수 있어요.

예를 들어:

filter : {A : Set} → (A → Bool) → List A → List A
filter p xs = do
  x    ← xs
  true ← p x ∷ []
    where false → []
  x ∷ []

do 표기법은 스코프 검사 전에 desugar되며 _>>=_와 _>>_에 대한 호출로 번역되는데, 이들은 임의의 사용자 정의 함수일 수 있어요. 이는 do 블록이 특정 모나드 개념에 묶이지 않는다는 뜻이에요. 실제로 do 블록에 모나드 문장이 없으면 let의 설탕으로 사용될 수 있어요:

pure-do : Nat → Nat
pure-do n = do
  let p2 m = m * m
      p4 m = p2 (p2 m)
  p4 n

check-pure-do : pure-do 5 ≡ 625
check-pure-do = refl

do 표기법을 desugar하는 데 사용되는 연산자는 사용자가 desugar된 버전을 직접 쓴 것처럼 해석돼서, 스코프 안에서 해당 이름으로 가리켜지는 함수들을 참조해요. 이를 제어하려면 do 키워드가 모듈 이름으로 한정될 수 있는데, 이 경우 연산자는 해당 모듈에서 가져와요:

module Add where
  _>>_ : Nat → Nat → Nat
  x >> y = x + y

qualified-example : Nat
qualified-example = Add.do
  1
  2
  3

_ : qualified-example ≡ 6
_ = refl

한정 모듈이 do 표현식의 스코프에서 열리지 않는다는 점, 즉 아무 바인딩도 스코프로 가져오지 않는다는 점을 주의하세요. 이는 한정된 do 표현식 안에서 _>>=_와 _>>_를 명시적으로 사용하면 여전히 비한정 버전을 참조한다는 뜻이에요.

Desugaring

문장	설탕	Desugar 결과
단순 바인드	do x ← m m'	m >>= λ x → m'
패턴 바인드	do p ← m where pᵢ → mᵢ m'	m >>= λ where p → m' pᵢ → mᵢ
부정 매칭	do () ← m	m >>= λ ()
비바인딩 문장	do m m'	m >> m'
Let	do let ds m'	let ds in m'

바인드의 패턴이 완전하면(exhaustive) where 절은 생략할 수 있어요.

예제 (Example)

Do 표기법은 인덱스된 데이터에 대한 패턴 매칭과 함께 사용하면 상당히 강력해져요. 예를 들어, 단순 타입 람다 계산법을 위한 '구성에 의한 정확(correct-by-construction)' 타입 체커를 작성해 봐요.

먼저 원시 항(raw terms)을 정의해요. 변수에는 de Bruijn 인덱스를 사용하고 람다에는 명시적 타입 주석을 단답니다:

infixr 6 _=>_
data Type : Set where
  nat  : Type
  _=>_ : (A B : Type) → Type

data Raw : Set where
  var : (x : Nat) → Raw
  lit : (n : Nat) → Raw
  suc : Raw
  app : (s t : Raw) → Raw
  lam : (A : Type) (t : Raw) → Raw

다음으로, 잘 타입된 항(well-typed terms)을 정의해요:

Context = List Type

-- x ∈ xs의 증명은 xs에서 x가 위치한 인덱스입니다.
infix 2 _∈_
data _∈_ {A : Set} (x : A) : List A → Set where
  zero : ∀ {xs} → x ∈ x ∷ xs
  suc  : ∀ {y xs} → x ∈ xs → x ∈ y ∷ xs

data Term (Γ : Context) : Type → Set where
  var : ∀ {A} (x : A ∈ Γ) → Term Γ A
  lit : (n : Nat) → Term Γ nat
  suc : Term Γ (nat => nat)
  app : ∀ {A B} (s : Term Γ (A => B)) (t : Term Γ A) → Term Γ B
  lam : ∀ A {B} (t : Term (A ∷ Γ) B) → Term Γ (A => B)

잘 타입된 항이 주어지면 모든 타입 정보(람다의 주석만 제외)를 기계적으로 지워 대응하는 원시 항을 얻을 수 있어요:

rawIndex : ∀ {A} {x : A} {xs} → x ∈ xs → Nat
rawIndex zero    = zero
rawIndex (suc i) = suc (rawIndex i)

eraseTypes : ∀ {Γ A} → Term Γ A → Raw
eraseTypes (var x)   = var (rawIndex x)
eraseTypes (lit n)   = lit n
eraseTypes suc       = suc
eraseTypes (app s t) = app (eraseTypes s) (eraseTypes t)
eraseTypes (lam A t) = lam A (eraseTypes t)

이제 타입 체커를 작성할 준비가 됐어요. 목표는 원시 항을 받아 타입 오류로 실패하거나, 시작한 원시 항으로 지워지는 잘 타입된 항을 반환하는 함수를 만드는 거예요. 먼저 반환 타입을 정의해요. 문맥과 검사할 원시 항으로 매개변수화돼요:

data WellTyped Γ e : Set where
  ok : (A : Type) (t : Term Γ A) → eraseTypes t ≡ e → WellTyped Γ e

변수에 대응하는 타입도 필요해요:

data InScope Γ n : Set where
  ok : (A : Type) (i : A ∈ Γ) → rawIndex i ≡ n → InScope Γ n

지움 증명이 refl인 경우에 대한 타입 동의어도 만들어 봐요:

infix 2 _ofType_
pattern _ofType_ x A = ok A x refl

do 표기법 예제이니 모나드가 있는 편이 좋겠네요. 문자열 오류가 있는 either 모나드를 사용해 봐요:

TC : Set → Set
TC A = Either String A

typeError : ∀ {A} → String → TC A
typeError = left

모나드 연산에는 instance 인자를 사용해서 어떤 모나드가 사용되는지 추론하게 해요.

타입의 동일성을 비교해야 해요. 이것이 패턴 매칭 바인드를 활용할 첫 기회예요:

_=?=_ : (A B : Type) → TC (A ≡ B)
nat      =?= nat      = pure refl
nat      =?= (_ => _) = typeError "type mismatch: expected nat, got _ => _"
(_ => _) =?= nat      = typeError "type mismatch: expected _ => _, got nat"
(A => B) =?= (A₁ => B₁) = do
  refl ← A =?= A₁
  refl ← B =?= B₁
  pure refl

문맥에서 변수를 찾는 것도 필요해요:

lookupVar : ∀ Γ n → TC (InScope Γ n)
lookupVar []      n       = typeError "variable out of scope"
lookupVar (A ∷ Γ) zero    = pure (zero ofType A)
lookupVar (A ∷ Γ) (suc n) = do
  i ofType B ← lookupVar Γ n
  pure (suc i ofType B)

잘 타입된 de Bruijn 인덱스가 주어진 원시 인덱스로 지워진다는 증명 의무가 완전히 내부적으로 처리되는 방식에 주목하세요 (이 경우 ofType 동의어의 refl 패턴에 의해).

마지막으로 실제 타입 체커를 구현해 봐요:

infer : ∀ Γ e → TC (WellTyped Γ e)
infer Γ (var x)    = do
  i ofType A ← lookupVar Γ x
  pure (var i ofType A)
infer Γ (lit n)    = pure (lit n ofType nat)
infer Γ suc        = pure (suc ofType nat => nat)
infer Γ (app e e₁) = do
  s ofType A => B ← infer Γ e
    where _ ofType nat → typeError "numbers cannot be applied to arguments"
  t ofType A₁     ← infer Γ e₁
  refl            ← A =?= A₁
  pure (app s t ofType B)
infer Γ (lam A e)  = do
  t ofType B ← infer (A ∷ Γ) e
  pure (lam A t ofType A => B)

app 경우에는 where 절을 사용해 적용할 함수가 잘 타입되었지만 함수 타입이 아닌 경우의 오류를 처리해요.

관용구 괄호 (Idiom brackets)

관용구 괄호는 적용형 펑터(applicative functor), 즉 두 연산을 갖춘 펑터 F와 더 편리하게 작업할 수 있게 해주는 표기법이에요:

pure  : ∀ {A} → A → F A
_<*>_ : ∀ {A B} → F (A → B) → F A → F B

관용구 괄호의 이름 해석은 do 표기법과 동일하게 동작해요: 괄호가 한정되지 않으면 연산자들은 사용자가 직접 쓴 것처럼 해석되고, 괄호가 한정되면 한정하는 모듈에서 조회돼요.

관용구 괄호의 문법은 다음과 같아요:

(| e a₁ .. aₙ |)

또는 유니코드 렌즈 괄호 ⦇ (U+2987)와 ⦈ (U+2988)을 사용해요:

⦇ e a₁ .. aₙ ⦈

이것은 (좌결합 _<*>_라고 가정하면) 다음과 같이 확장돼요:

pure e <*> a₁ <*> .. <*> aₙ

관용구 괄호는 연산자와 잘 어울려요. 예를 들어:

(| if a then b else c |)

은 다음과 같이 desugar돼요:

pure if_then_else_ <*> a <*> b <*> c

관용구 괄호는 적용이 없거나 여러 번인 경우도 지원해요. 적용형 펑터가 추가 이항 연산 _<|>_를 가지면:

_<|>_ : ∀ {A B} → F A → F A → F A

관용구 괄호는 세로 막대 |로 구분된 여러 적용을 지원해요:

(| e₁ a₁ .. aₙ | e₂ a₁ .. aₘ | .. | eₖ a₁ .. aₗ |)

이것은 (우결합 _<|>_라고 가정하면) 다음과 같이 확장돼요:

(pure e₁ <*> a₁ <*> .. <*> aₙ) <|> ((pure e₂ <*> a₁ <*> .. <*> aₘ) <|> (pure eₖ <*> a₁ <*> .. <*> aₗ))

적용 없는 관용구 괄호 (|) 또는 ⦇⦈은, empty가 스코프에 있으면 empty로 확장돼요:

empty :  ∀ {A} → F A

empty와 _<|>_를 가진 적용형 펑터는 일반적으로 Alternative라고 불려요.

pure, _<*>_, _<|>_가 스코프에 없어도 (|)를 사용할 수 있다는 점에 주의하세요.

제약 사항:

• 바인딩 문법과 연산자 섹션은 관용구 괄호 내부에 바로 나타날 수 없어요.
• 관용구 괄호 내부의 최상위 적용은 암시적 적용(implicit application)을 포함할 수 없어서, 다음과 같은 것은:

  (| foo {x = e} a b |)
  

  불법이에요. e가 순수한 경우 다음을 쓸 수 있어요:

  (| (foo {x = e}) a b |)
  

  이는 다음과 같이 desugar돼요:

  pure (foo {x = e}) <*> a <*> b
  

더 알아보기 (Learn more)

• Agda 문서: 문법 설탕 원문