https://github.com/damhiya/MetaLambda


identity function

1 2 3 4>> fn (x : base) -> x fn (x_0 : base) -> x_0 (base -> base) fn (x_0 : base) -> x_0


처치엔코딩 3*3 = 9

1 2 3 4>> let box[f.U] = box[f : base -> base . fn (x : base) -> f (f (f x))] in box[f : base -> base. U with (U with (f))] let box[f_0 . U_0] = box[f_0 : base -> base . fn (x_0 : base) -> f_0 (f_0 (f_0 x_0))] in box[f_0 : base -> base . U_0 with ( U_0 with ( f_0 ) )] [f_0 : base -> base |- base -> base] box[f_0 : base -> base . fn (x_1 : base) -> (fn (x_0 : base) -> f_0 (f_0 (f_0 x_0))) ((fn (x_0 : base) -> f_0 (f_0 (f_0 x_0))) ((fn (x_0 : base) -> f_0 (f_0 (f_0 x_0))) x_1))]


box comonad에 대한 co-join

(modal logic의 axiom 4 : □P → □□P 에 대응하는 term임)

1 2 3 4>> fn (bx : [|- base ]) -> let box[.x] = bx in box[.box[.x with ()]] fn (bx_0 : [ |- base]) -> let box[ . x_0] = bx_0 in box[ . box[ . x_0 with ()]] [ |- base] -> [ |- [ |- base]] fn (bx_0 : [ |- base]) -> let box[ . x_0] = bx_0 in box[ . box[ . x_0 with ()]]


저번에 만든건 2 stage였는데, infinite stage로 바꾸고 파서랑 pretty printer 추가해서 repl로 만듬.

repl에서 입력한 값 저장해두고 나중에 쓰는건 안되고 걍 closed expression 입력하면 타입검사하고 평가해서 출력해줌

(첫줄은 파싱한거 그대로 출력, 둘째줄은 타입, 셋째줄은 eval한 결과)


Contextual modal type 자세히 설명하는 글도 쓰고는 싶은데 좀 벅차네..