Idris의 내부
Idris의 내부 (Idris' Internals)
주의: 이것은 여전히 David Christiansen이 Edwin의 2013 Idris 개발자 회의 발표에서 기록한 비교적 날것의 메모예요. 유용한 안내서로 바뀌는 과정에 있으며, 기여해도 좋아요.
이 문서는 이미 Idris에 익숙하다고 가정해요. 내부 작업을 하고자 하는 사람들을 위한 문서예요. 새 백엔드를 개발하려는 사람들은 코드 생성 대상을 살펴보고 싶을 거예요.
출처: 문서
본문
Core/TT.hs
Idris는 단순하고 명시적인 코어 언어로 컴파일돼요. 이 코어 언어는 Π처럼 보이기 때문에 TT라고 불려요. 그것은 최소한의 언어이며, 국소적으로 이름 없는(locally nameless) 표현을 사용해요. 즉, 국소 변수는 de Bruijn 인덱스로 표현되고, 전역적으로 정의된 상수는 이름으로 표현돼요.
TT 데이터 타입은 Idris 코드에서 흔한 요령을 사용해요: 그것은 저장된 이름들의 타입에 대해 다형(polymorphic)이고, Functor를 파생해요. 이것은 fmap이 범용 순회(general-purpose traversal)로 사용되게 해줘요.
λ, Π, let-바인딩에 사용되는 바인더(binders)를 위한 일반적인 구성이 있어요. 이것들은 BinderType을 사용해 구분돼요.
컴파일 중에 일부 용어 (특히 타입)은 지워질 거예요. 이것은 TT의 Erased 생성자를 사용해 표현돼요. TT 용어를 생성할 때 편리한 요령은, 용어가 유일하게 결정되는 곳에 Erased를 삽입하는 것이에요. 타입 검사기가 그것을 채워줄 것이기 때문이에요.
생성자 Proj는 최적화의 결과예요. 그것은 새 패턴-매칭 연산을 정의하는 것보다 더 경제적인 방식으로 특정 생성자 인자를 추출하는 데 사용돼요.
Raw 데이터 타입은 아직 타입 체킹되지 않은 용어를 나타내요. 타입 검사기는 가능하면 Raw를 TT로 변환해요.
Core/CaseTree.hs
case 트리는 TT 언어에서 최상위 패턴-매칭 정의를 표현하는 데 사용돼요.
TT 데이터 타입과 마찬가지로, SC와 CaseAlt와 함께 Functor 파생 요령이 사용돼, 포함된 용어들 위에 매핑하는 함수를 GHC가 생성하게 해요.
생성자 case들 (CaseAlt의 ConCase)은 번호가 매겨진 생성자들을 참조해요. 모든 생성자에는 0,1,2,… 번호가 매겨져요. 컴파일러의 이 단계에서 태그들은 데이터 타입-국소적(datatype-local)이에요. 그러나 역함수화(defunctionalization) 후에는 전역적으로 유일하게 만들어져요.
n+1 패턴(SucCase)과 어수선해 보이는 것들은 코드를 빠르게 만들기 위한 것이에요 — 표현을 "정리"하기 전에 물어봐 주세요.
Core/Evaluate.hs
이 모듈은 Idris의 주요 평가기를 포함해요. 평가기는 REPL과, 정규화된 용어를 동등성으로 비교해야 하는 타입 체킹 중에 둘 다 사용돼요.
평가기의 핵심 데이터 타입 중 하나는 컨텍스트(context)예요. 컨텍스트는 전역 이름을 그 값들로 매핑하는 것이지만, 타입 지향 모호성 해소(type-directed disambiguation)를 빠르게 하도록 조직돼 있어요. 특히, 사용자가 입력할 수 있는 이름의 주요 부분이 키로 사용되고, 그 값들은 이름공간에서 실제 값들로의 맵이에요.
Def 데이터 타입은 전역 컨텍스트의 정의를 나타내요. 모든 전역 이름은 이 구조로 매핑돼요.
Type과 Term은 둘 다 TT의 동의어예요.
데이터 타입은 적절한 NameType을 가진 TyDecl로 표현돼요. Function은 주석이 달린 타입을 가진 전역 상수 용어이고, Operator는 Haskell로 구현된 기본 연산(primitive)을 나타내며, CaseOp는 일반적인 패턴-매칭 정의를 나타내요. CaseOp는 서로 다른 목적을 위한 네 가지 버전이 있으며, 모두 저장되는데 그것이 제일 쉽기 때문이에요.
CaseInfo의 tc_dictionary는 타입 클래스 사전이어서 전체성 검사를 더 쉽게 만들기 때문이에요.
normalise* 함수들은 서로 다른 동작을 제공해요 — 그러나 normalise가 가장 흔해요.
normaliseC— "resolved"는 이름이 적절하게 de Bruijn 인덱스로 변환됨을 뜻해요.normaliseAll— non-total이더라도 모든 것을 줄여요.normaliseTrace— 디버깅을 위한 특수 목적 함수예요.
simplify — 작은 것들을 줄여요 — 리스트 인자는 줄이지 말 것들을 나타내요.
Core/Typecheck.hs
표준적인 내용이에요. 바라건대 변경이 필요하지 않아요.
Core/Elaborate.hs
Idris 정의는 하나씩 정교화되어 대응하는 TT로 바뀌어요. 이것은 Elab 모나드(사용자 지정 상태가 있으면 Elab') 안의 EDSL로서 택틱 언어로 행해져요.
오류를 위한 플럼빙(plumbing)이 많아요.
모든 정교화는 전역 컨텍스트에 상대적이에요.
elaborate가 반환하는 쌍 안의 문자열은 로그 정보예요. JFP 논문을 보세요. 그러나 이름들이 서로 매핑되지는 않을 거예요. 그 논문은 로깅, 추가 상태 등이 없는 "이상화된 버전"이에요.
모든 택틱은 Raw s를 받아들이고, 타입 체킹은 거기서 일어나요.
claim (x : t)은 새 x : t를 가정해요.
부탁: 사물을 정리해주세요!
proofSearch 플래그는 실패가 인간에서 왔는지(그러면 실패) 기계에서 왔는지(그러면 계속) 시도하기 위한 것이에요.
대안을 명시적으로 제공하는 Idris-수준 문법: (| x, y, z |)는 x, y, z를 순서대로 시도하고 처음 성공하는 것을 취해요.
Core/ProofState.hs
(설명 없음)
Core/Unify.hs
통일(unification)을 다뤄요. 통일은 다음과 같이 답할 수 있어요:
- 이것은 작동해요
- 이것은 절대 작동할 수 없어요
- 이 다른 통일 문제들이 해결되면 작동할 거예요 (예:
f x를1과 통일하기)
match_unify — 이름을 이름에, 용어를 용어에 매칭한다는 점만 빼고 통일과 같은 것이에요. x + y는 x = 0으로 0 + y에 매칭돼요. <== 문법과 타입 클래스 해석에 사용돼요.
Idris/AbsSyntaxTree.hs
PTerm은 Idris 문법의 데이터 타입이에요. P는 Program(프로그램)을 뜻해요.
각 PTerm은 일련의 택틱을 적용함으로써 TT 용어로 바뀌어요.
IState는 주요 인터프리터 상태예요. 전역 컨텍스트는 tt_ctxt 필드예요.
Ctxt는 잠재적으로 모호한 이름들을 그 지시 대상(referents)으로 매핑해요.
Idris/ElabDecls.hs
이곳이 PTerm에서 TT로의 실제 정교화가 일어나는 곳이에요.
Idris/ElabTerm.hs
build는 Raw를 만드는 함수예요. 모든 "잡동사니"는 메타변수(metavars) 같은 것들을 다루기 위한 것이에요. 그것은 아직 정의되어야 할 이름들을 기억해야 하며, 타입을 아직 알지 못해요 (나중에 통일로 채워져요). 또한 case 표현식은 최상위 함수로 바뀌어야 해요.
resolveTC는 타입 클래스 해석이에요.