문법 확장

문법 확장 (Syntax Extensions)

Idris는 여러 방식으로 임베디드 도메인 특화 언어(EDSL, Embedded Domain Specific Languages)의 구현을 지원해요 [1]. 우리가 이미 본 한 가지 방식은 do 표기법(do notation)을 확장하는 것이에요. 또 다른 중요한 방식은 핵심 문법(core syntax)의 확장을 허용하는 것이에요. 이 절에서는 문법을 확장하는 두 가지 방법, 즉 문법 규칙(syntax rules)과 dsl 표기법(dsl notation)을 설명할게요.

문법 규칙 (syntax rules)

우리는 if...then...else 식을 봤지만, 이는 내장된 것이 아니에요. 대신 프렐류드(prelude)에서 다음과 같이 함수를 정의할 수 있어요 (이 함수는 Laziness 절에서 이미 봤어요):

ifThenElse : (x:Bool) -> Lazy a -> Lazy a -> a;
ifThenElse True  t e = t;
ifThenElse False t e = e;

그리고 문법 선언(syntax declaration)으로 핵심 문법을 확장해요:

syntax if [test] then [t] else [e] = ifThenElse test t e;

문법 선언의 왼쪽은 문법 규칙을 기술하고, 오른쪽은 그 펼침(expansion)을 기술해요. 문법 규칙 자체는 다음으로 구성돼요:

  • 키워드(Keywords) — 여기서는 if, then, else이고, 유효한 식별자여야 해요.

  • 비터미널(Non-terminals) — 여기서는 [test], [t], [e]처럼 대괄호로 감싸며, 임의의 식을 나타내요. 파싱 모호성을 피하기 위해, 이 식들은 최상위 수준에서는 문법 확장을 사용할 수 없어요 (괄호 안에서는 사용할 수 있지만).

  • 이름(Names) — 중괄호로 감싸며, 오른쪽에 묶일 수 있는 이름을 나타내요.

  • 기호(Symbols) — 따옴표로 감싸며, 예: ":=". 문법 규칙에 예약어("let", "in" 같은)를 포함하는 데에도 사용할 수 있어요.

문법 규칙 형태의 제한은, 반드시 기호나 키워드를 적어도 하나 포함해야 하고, 비터미널을 나타내는 반복 변수(variables)가 없어야 한다는 것이에요. 어떤 식이든 사용할 수 있지만, 규칙에 비터미널이 두 개 연속으로 있으면 단순한 식(즉 변수, 상수, 괄호로 감싼 식)만 사용될 수 있어요. 규칙은 이전에 정의된 규칙을 사용할 수 있지만 재귀적일 수는 없어요. 따라서 다음 문법 확장은 유효할 거예요:

syntax [var] ":=" [val]                = Assign var val;
syntax [test] "?" [t] ":" [e]          = if test then t else e;
syntax select [x] from [t] "where" [w] = SelectWhere x t w;
syntax select [x] from [t]             = Select x t;

문법 매크로는 패턴(patterns)에서만 적용되도록 (즉 패턴 매치 절의 왼쪽에서만), 또는 용어(terms)에서만 적용되도록 (즉 패턴 매치 절의 왼쪽을 제외한 모든 곳에서) — pattern 또는 term 문법 규칙으로 표시해 더 제한할 수도 있어요. 예를 들어 하한이 상한보다 낮다는 것을 so를 사용해 정적으로 검사하는 다음과 같은 구간(interval)을 정의할 수 있어요:

data Interval : Type where
   MkInterval : (lower : Double) -> (upper : Double) ->
                So (lower < upper) -> Interval

패턴에서는 증명 인자에 항상 Oh가 매치되고, 용어에서는 증명 항(proof term)을 제공해야 하는 문법을 정의할 수 있어요:

pattern syntax "[" [x] "..." [y] "]" = MkInterval x y Oh
term    syntax "[" [x] "..." [y] "]" = MkInterval x y ?bounds_lemma

용어에서 [x...y] 문법은 증명 의무(proof obligation) bounds_lemma를 (아마 이름이 바뀌어서) 생성할 거예요.

마지막으로, 문법 규칙은 대안적인 바인딩 형식(binding forms)을 도입하는 데 사용될 수 있어요. 예를 들어 for 루프는 각 반복마다 변수를 바인딩해요:

syntax for {x} "in" [xs] ":" [body] = forLoop xs (\x => body)

main : IO ()
main = do for x in [1..10]:
              putStrLn ("Number " ++ show x)
          putStrLn "Done!"

{x} 형식을 사용해 x가 묶인 변수(bound variable)를 나타내고 오른쪽에 치환된다고 명시했어요. in은 이미 예약어이므로 따옴표 안에 넣었어요.

dsl 표기법 (dsl notation)

잘 타입된 인터프리터(Well-Typed Interpreter) 절은 의존 타입을 사용하는 흔한 프로그래밍 패턴의 단순한 예시예요. 즉: 객체 언어(object language)와 그 타입 시스템을 의존 타입으로 기술해 오직 잘 타입된 프로그램만 표현될 수 있게 보장한 다음, 그 표현을 사용해 프로그래밍하는 것이에요. 이 접근법으로 예를 들어 이진 데이터 직렬화 프로그램 [2]이나 동시 프로세스를 안전하게 실행하는 프로그램 [3]을 작성할 수 있어요.

안타깝게도 객체 언어 프로그램의 형태 때문에 실제로는 이렇게 프로그래밍하기가 꽤 어려워요. 예를 들어 Expr의 팩토리얼 프로그램을 떠올려보세요:

fact : Expr G (TyFun TyInt TyInt)
fact = Lam (If (Op (==) (Var Stop) (Val 0))
               (Val 1) (Op (*) (App fact (Op (-) (Var Stop) (Val 1)))
                               (Var Stop)))

이것은 특히 유용한 패턴이므로, Idris는 그러한 객체 언어에서 프로그래밍하기 쉽게 만들어주는 문법 오버로딩(syntax overloading) [1]을 제공해요:

mkLam : TTName -> Expr (t::g) t' -> Expr g (TyFun t t')
mkLam _ body = Lam body

dsl expr
    variable    = Var
    index_first = Stop
    index_next  = Pop
    lambda      = mkLam

dsl 블록은 각 문법 구성물이 객체 언어에서 어떻게 표현되는지 기술해요. 여기서 expr 언어에서, 어떤 변수든 Var 생성자로 번역되고, Pop과 Stop을 사용해 de Bruijn 인덱스(즉 변수 자체가 묶인 이후의 바인딩 수를 세는 것)를 만들며, 어떤 람다든 Lam 생성자로 번역돼요. mkLam 함수는 단순히 첫 번째 인자 — 사용자가 변수에 대해 선택한 이름 — 를 무시해요. 이런 방식으로 let과 의존 함수 문법(pi)을 오버로드하는 것도 가능해요. 이제 fact를 다음과 같이 작성할 수 있어요:

fact : Expr G (TyFun TyInt TyInt)
fact = expr (\x => If (Op (==) x (Val 0))
                      (Val 1) (Op (*) (app fact (Op (-) x (Val 1))) x))

이 새로운 버전에서, expr은 다음 식이 오버로드될 것임을 선언해요. idiom 괄호(idiom brackets)를 사용해 한 걸음 더 나아갈 수 있어요:

(<*>) : (f : Lazy (Expr G (TyFun a t))) -> Expr G a -> Expr G t
(<*>) f a = App f a

pure : Expr G a -> Expr G a
pure = id

이것들이 Applicative 구현의 일부일 필요는 없다는 점에 유의하세요 — idiom 괄호 표기법이 <*>와 pure 이름으로 직접 번역되고, 임시(ad-hoc) 타입 지시 오버로딩이 허용되기 때문이에요. 이제 다음과 같이 말할 수 있어요:

fact : Expr G (TyFun TyInt TyInt)
fact = expr (\x => If (Op (==) x (Val 0))
                      (Val 1) (Op (*) [| fact (Op (-) x (Val 1)) |] x))

임시 오버로딩과 인터페이스 사용을 조금 더 하면, 새 문법 규칙으로 다음과 같은 수준까지도 갈 수 있어요:

syntax "IF" [x] "THEN" [t] "ELSE" [e] = If x t e

fact : Expr G (TyFun TyInt TyInt)
fact = expr (\x => IF x == 0 THEN 1 ELSE [| fact (x - 1) |] * x)

[1]

(1, 2) Edwin Brady and Kevin Hammond. 2012. Resource-Safe systems programming with embedded domain specific languages. In Proceedings of the 14th international conference on Practical Aspects of Declarative Languages (PADL'12), Claudio Russo and Neng-Fa Zhou (Eds.). Springer-Verlag, Berlin, Heidelberg, 242-257. DOI=10.1007/978-3-642-27694-1_18 https://dx.doi.org/10.1007/978-3-642-27694-1_18

[2]

Edwin C. Brady. 2011. IDRIS —: systems programming meets full dependent types. In Proceedings of the 5th ACM workshop on Programming languages meets program verification (PLPV '11). ACM, New York, NY, USA, 43-54. DOI=10.1145/1929529.1929536 https://doi.acm.org/10.1145/1929529.1929536

[3]

Edwin Brady and Kevin Hammond. 2010. Correct-by-Construction Concurrency: Using Dependent Types to Verify Implementations of Effectful Resource Usage Protocols. Fundam. Inf. 102, 2 (April 2010), 145-176. https://dl.acm.org/citation.cfm?id=1883636

출처: 문서