언어 확장
언어 확장 (Language Extensions)
Idris를 확장하는 두 가지 방법, 타입 프로바이더(Type Providers)와 정교화기 반영(Elaborator Reflection)에 대해 설명하는 문서예요.
출처: 문서
본문
타입 프로바이더 (Type Providers)
Idris 타입 프로바이더는 Idris 바깥 세계에 대한 관찰을 타입 시스템에 반영하는 방법이에요. F# 타입 프로바이더와 유사하게, 이것들은 타입 체킹 도중에 효과 있는(effectful) 계산을 실행해서, 나머지 프로그램을 검사할 때 타입 검사기가 사용할 수 있는 정보를 반환하도록 해요. F# 타입 프로바이더가 코드 생성에 기반한 반면, Idris 타입 프로바이더는 정보를 생성하기 위해 Idris의 일반적인 실행 의미론만 사용해요.
타입 프로바이더는 단순히 타입 IO (Provider t)의 용어(term)예요. 여기서 Provider는 성공 결과와 오류를 위한 생성자를 가진 데이터 타입이에요. 타입 t는 Type(타입들의 타입)일 수도 있고, 구체적인 타입일 수도 있어요. 그러면 타입 프로바이더 p는 %provide (x : t) with p 문법으로 호출돼요. 타입 검사기가 이 줄을 만나면 IO 액션 p가 실행돼요. 그런 다음 결과 용어가 IO 모나드에서 추출돼요. 그것이 어떤 y : t에 대해 Provide y라면, x는 나머지 타입 체킹과 컴파일된 코드에서 y로 묶여요. 실행이 실패하면 일반 오류가 보고되고 타입 체킹이 종료돼요. 결과 용어가 어떤 문자열 e에 대해 Error e라면, 타입 체킹이 실패하고 오류 e가 사용자에게 보고돼요.
예시 Idris 타입 프로바이더는 이 저장소에서 볼 수 있어요. 더 자세한 설명은 David Christiansen의 WGP '13 논문과 M.Sc. 논문에서 볼 수 있어요.
정교화기 반영 (Elaborator Reflection)
언어를 확장하는 또 다른 방법은 정교화기 반영(elaborator reflection)으로, 이는 정교화기 반영 섹션에서 설명해요.