예: 잘 타입된 인터프리터
예: 잘 타입된 인터프리터 (Example: The Well-Typed Interpreter)
이 절에서는 지금까지 본 기능들을 사용해 더 큰 예제, 즉 변수, 함수 적용, 이항 연산자, if...then...else 구성물을 가진 간단한 함수형 프로그래밍 언어용 인터프리터를 작성할게요. 표현될 수 있는 어떤 프로그램이든 잘 타입되도록 보장하기 위해 의존 타입 시스템을 사용할게요.
출처: 문서
본문
언어 표현하기 (Representing Languages)
먼저 언어의 타입을 정의해봅시다. Ty로 표현된 정수, 불리언, 함수가 있어요:
data Ty = TyInt | TyBool | TyFun Ty Ty
이 표현들을 구체적인 Idris 타입으로 번역하는 함수를 작성할 수 있어요 — 타입이 일급(first class)이므로 다른 값처럼 계산될 수 있다는 것을 기억하세요:
interpTy : Ty -> Type
interpTy TyInt = Integer
interpTy TyBool = Bool
interpTy (TyFun a t) = interpTy a -> interpTy t
오직 잘 타입된 프로그램만 표현될 수 있도록 언어의 표현을 정의할게요. 식의 표현을 그 타입과 지역 변수의 타입들(컨텍스트)로 인덱싱할게요. 컨텍스트는 Vect 데이터 타입으로 표현될 수 있고, 자주 사용되므로 묵시적 인자로 표현될 거예요. 이를 위해 using 블록 안에서 모든 것을 정의해요 (이 지점 이후의 모든 것은 using 블록 안에 있도록 들여써야 한다는 것을 기억하세요):
using (G:Vect n Ty)
식은 지역 변수의 타입들과 식 자체의 타입으로 인덱싱돼요:
data Expr : Vect n Ty -> Ty -> Type
식의 완전한 표현은 다음이에요:
data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where
Stop : HasType FZ (t :: G) t
Pop : HasType k G t -> HasType (FS k) (u :: G) t
data Expr : Vect n Ty -> Ty -> Type where
Var : HasType i G t -> Expr G t
Val : (x : Integer) -> Expr G TyInt
Lam : Expr (a :: G) t -> Expr G (TyFun a t)
App : Expr G (TyFun a t) -> Expr G a -> Expr G t
Op : (interpTy a -> interpTy b -> interpTy c) ->
Expr G a -> Expr G b -> Expr G c
If : Expr G TyBool ->
Lazy (Expr G a) ->
Lazy (Expr G a) -> Expr G a
위 코드는 Idris 표준 라이브러리의 Vect와 Fin 타입을 사용해요. 프렐류드에 제공되지 않으므로 import 해요:
import Data.Vect
import Data.Fin
식이 그 타입으로 인덱싱되므로, 생성자 정의에서 언어의 타입 규칙을 읽을 수 있어요. 각 생성자를 차례로 살펴봅시다.
변수에는 이름 없는(nameless) 표현을 사용해요 — 그것들은 de Bruijn 인덱스예요. 변수는 컨텍스트에서의 소속 증명인 HasType i G T로 표현되는데, 이는 컨텍스트 G의 변수 i가 타입 T를 가진다는 증명이에요. 이는 다음과 같이 정의돼요:
data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where
Stop : HasType FZ (t :: G) t
Pop : HasType k G t -> HasType (FS k) (u :: G) t
Stop을 가장 최근에 정의된 변수가 잘 타입되었다는 증명으로, Pop n을 n번째로 최근에 정의된 변수가 잘 타입되었다면 n+1번째도 잘 타입되었다는 증명으로 취급할 수 있어요. 실제로 이는 Var 생성자를 통해 Stop으로 가장 최근에 정의된 변수를, Pop Stop으로 다음 변수를 가리키는 식으로 계속한다는 뜻이에요:
Var : HasType i G t -> Expr G t
따라서 식 \x. \y. x y에서 변수 x는 de Bruijn 인덱스 1(Pop Stop으로 표현)을 갖고, y는 0(Stop으로 표현)을 가져요. 이것은 정의와 사용 사이의 람다 수를 세어 찾아요.
값은 정수의 구체적인 표현을 운반해요:
Val : (x : Integer) -> Expr G TyInt
람다는 함수를 만들어요. 타입 a -> t의 함수 범위 안에는 타입 a의 새 지역 변수가 있으며, 이것은 컨텍스트 인덱스로 표현돼요:
Lam : Expr (a :: G) t -> Expr G (TyFun a t)
함수 적용은 a에서 t로의 함수와 타입 a의 값이 주어지면 타입 t의 값을 만들어요:
App : Expr G (TyFun a t) -> Expr G a -> Expr G t
임의의 이항 연산자를 허용하는데, 연산자의 타입이 인자의 타입이 무엇이어야 하는지를 알려줘요:
Op : (interpTy a -> interpTy b -> interpTy c) ->
Expr G a -> Expr G b -> Expr G c
마지막으로, If 식은 불리언이 주어지면 선택을 해요. 각 분기는 같은 타입이어야 하고, 취해진 분기만 평가되도록 분기를 느슨하게(lazily) 평가할게요:
If : Expr G TyBool ->
Lazy (Expr G a) ->
Lazy (Expr G a) ->
Expr G a
인터프리터 작성하기 (Writing the Interpreter)
Expr를 평가할 때, 범위 안의 값들과 그 타입들을 알아야 해요. Env는 범위 안의 타입들로 인덱싱된 환경이에요. 환경은 또 다른 형태의 리스트일 뿐이지만, 지역 변수 타입들의 벡터와 강하게 지정된 연결을 가지므로, 일반 리스트 문법을 사용할 수 있도록 일반적인 ::와 Nil 생성자를 사용해요. 변수가 컨텍스트에 정의되었다는 증명이 주어지면 환경에서 값을 만들 수 있어요:
data Env : Vect n Ty -> Type where
Nil : Env Nil
(::) : interpTy a -> Env G -> Env (a :: G)
lookup : HasType i G t -> Env G -> interpTy t
lookup Stop (x :: xs) = x
lookup (Pop k) (x :: xs) = lookup k xs
이것이 주어지면, 인터프리터는 특정 환경에 대해 Expr를 구체적인 Idris 값으로 번역하는 함수예요:
interp : Env G -> Expr G t -> interpTy t
완전한 인터프리터는 참고용으로 다음과 같이 정의돼요. 각 생성자에 대해 그에 해당하는 Idris 값으로 번역해요:
interp env (Var i) = lookup i env
interp env (Val x) = x
interp env (Lam sc) = \x => interp (x :: env) sc
interp env (App f s) = interp env f (interp env s)
interp env (Op op x y) = op (interp env x) (interp env y)
interp env (If x t e) = if interp env x then interp env t
else interp env e
각 경우를 차례로 살펴봅시다. 변수를 번역하려면 환경에서 그것을 찾기만 하면 돼요:
interp env (Var i) = lookup i env
값을 번역하려면 값의 구체적인 표현을 반환하기만 하면 돼요:
interp env (Val x) = x
람다는 더 흥미로워요. 이 경우 람다의 범위를 환경의 새 값으로 해석하는 함수를 구성해요. 즉, 객체 언어의 함수가 Idris 함수로 번역돼요:
interp env (Lam sc) = \x => interp (x :: env) sc
적용의 경우, 함수와 그 인자를 해석해 직접 적용해요. f를 해석하는 것이 함수를 만들어야 한다는 것을 그 타입 때문에 알고 있어요:
interp env (App f s) = interp env f (interp env s)
연산자와 조건문은, 다시, 동등한 Idris 구성물로의 직접 번역이에요. 연산자의 경우 함수를 피연산자에 직접 적용하고, If의 경우 Idris if...then...else 구성물을 직접 적용해요.
interp env (Op op x y) = op (interp env x) (interp env y)
interp env (If x t e) = if interp env x then interp env t
else interp env e
테스트 (Testing)
간단한 테스트 함수들을 만들 수 있어요. 첫째, 두 입력을 더하는 \x. \y. y + x는 다음과 같이 작성돼요:
add : Expr G (TyFun TyInt (TyFun TyInt TyInt))
add = Lam (Lam (Op (+) (Var Stop) (Var (Pop Stop))))
더 흥미롭게, 팩토리얼 함수 fact (예: \x. if (x == 0) then 1 else (fact (x-1) * x))는 다음과 같이 작성될 수 있어요:
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)))
실행 (Running)
마무리하려면, 사용자 입력에 대해 팩토리얼 함수를 해석하는 메인 프로그램을 작성해요:
main : IO ()
main = do putStr "Enter a number: "
x <- getLine
printLn (interp [] fact (cast x))
여기서 cast는 가능하면 값을 한 타입에서 다른 타입으로 변환하는 오버로드된 함수예요. 여기서는 문자열을 정수로 변환하며, 입력이 유효하지 않으면 0을 줘요. Idris 대화형 환경에서 이 프로그램 실행의 예시는 다음과 같아요:
$ idris interp.idr
____ __ _
/ _/___/ /____(_)____
/ // __ / ___/ / ___/ Version 1.3.2
_/ // /_/ / / / (__ ) https://www.idris-lang.org/
/___/\__,_/_/ /_/____/ Type :? for help
Type checking ./interp.idr
*interp> :exec
Enter a number: 6
720
*interp>
곁가지: cast (Aside: cast)
프렐류드는 타입 간 변환을 허용하는 Cast 인터페이스를 정의해요:
interface Cast from to where
cast : from -> to
이것은 cast의 소스 타입과 대상 타입을 정의하는 다중 매개변수 인터페이스예요. cast가 적용되는 지점에서 타입 검사기가 두 매개변수를 모두 추론할 수 있어야 해요. 모든 프리미티브 타입들 사이에, 의미가 있는 한, cast가 정의되어 있어요.