https://github.com/damhiya/MetaLambda/


아아- 이것은 「Contextual modal type thery」 라는 것이다.

메타프로그래밍을 타입 안전하게 할 수 있지.


contextual modal type이란 뭔가?


https://www.researchgate.net/publication/220613624_Contextual_modal_type_theory

그건 이 논문을 읽어보면 알 수 있지만 프로그래머가 솔깃할만한 이야기만 하겠음


메타프로그래밍으로 제일 유명한 언어로 흔히 리습이 꼽히는데, 리습의 메타프로그래밍은 다음과 같은 특징이 있음

1. Quasi-quotation

리습에서 사용하는 메타프로그래밍은 quasi-quotation에 기반함. 리습에 있는 (quasi)quote/unquote 를 사용하는거라고 생각하면 됨.

참고로 quasi-quotation은 원래 언어철학 쪽에서 나옴. https://en.wikipedia.org/wiki/Quasi-quotation


2. Homogeneous metaprogramming

메타언어와 대상언어가 동일함. 만약 메타프로그래밍용 언어가 대상언어와 다르다면 Heterogeneous 임 (러스트 등이 해당)


3. Infinite stage

대상언어에서도 메타프로그래밍을 할 수 있음. 다시 말해서 "메타프로그래밍을 하는 프로그램"을 만들어 내는 메타프로그램을 작성할 수 있음.

그리고 이 "메타프로그램-대상프로그램"의 관계가 무한히 중첩될 수 있음. 이런걸 infinite stage라고 함.


4. Homoiconicity

얘는 내가 제대로 설명을 못하겠다. 일단 Homoiconicity는 Homogeneous 랑은 다른거임. 나는 이게 메타언어에서 대상언어를 표현하는 syntax하고 관련이 있다고 이해하고 있는데 맞는지는 잘 모르겠음.


5. Hygienic macro

이건 리습에선 옵션이긴 한데, hygienic macro를 사용하면 치환 과정에서 변수가 올바르게 바인딩 되도록 알아서 변수 이름을 바꿈.


리습 메타프로그래밍은 다른 언어에서 많이 차용해감.

하스켈도 Template Haskell 이라고 하는 quasi-quotation 기반 메타프로그래밍 시스템이 있음.



하지만 일반적인 상황에서는 메타프로그래밍이 기피됨. 너무 어렵거든.

메타프로그래밍이 힘든 가장 큰 이유는 에러가 macro expansion 후에 발생하기 때문임.

메타프로그래밍을 지원하는 대부분의 언어는 일단 macro expansion을 거친 뒤에 타입검사를 하고 컴파일 되는데, macro expansion 후에 타입체킹 과정에서 에러가 발생하면 (리습은 타입검사가 없으니 런타임에 터질 수도 있지만) macro expansion 된 출력물을 보면서 디버깅을 해야하는 상황이 발생함.


다행히도 똑똑한 사람들이 여기에 대한 해결책을 만들었는데, 그게 contextual modal type theory임.

CMTT에 기반한 언어에서는 먼저 타입검사를 실행하고, macro expansion이 일어난 다음에 컴파일 됨. 타입검사를 통과했다면 macro expansion된 후의 코드는 반드시 올바른 타입을 가짐.

그리고 리습 매크로랑 비슷한 특징을 많이 공유함. CMTT도 homogeneous, infinite stage고 hygienic 매크로 처럼 변수명이 충돌해서 binding이 이상하게 되지 않도록 자동으로 처리해줌.


내가 만든건 CMTT 논문에서 소개하는 타입시스템을 heterogeneous하게 바꾼 좀 간단한 언어야.

메타언어가 CMTT고 대상언어는 그냥 simply typed lambda calculus임.

일단 type checker하고 evaluation만 구현했고, 파서를 아직 안만듬.


https://github.com/damhiya/MetaLambda/blob/896100278fef8172768eb29b56a88938c38e680a/2-stage/Test.hs#L57

이건 예제 코드인데

nine' --> box(f. fn y -> ((fn x -> f (f (f x))) ((fn x -> f (f (f x))) ((fn x -> f (f (f x))) y))))

nine' 이라는 메타프로그램을 평가하면 이런 object 코드가 만들어짐.



https://arxiv.org/abs/2111.08099

최근에는 이 CMTT에서 다형성이랑 대상언어에 대한 패턴매칭을 할 수 있게 확장한 논문도 나왔음

저 논문에 나온 Mœbius 라는 언어는 타입 시스템만 제시 된거고 구현은 아직 없음


https://github.com/Beluga-lang/Beluga

마찬가지로 contextual type을 쓰는 Beluga 라는 언어도 있음