Y = forall A. λf.
    let g = thunk (λx. (force f) ((force (unroll x)) x)) : thunk ((μX. thunk (X -> A)) -> A)
    in g (roll g : μX. thunk (X -> A))

를 타입 검사한 게 지난 일이었다.

(Y[λ⟨ isEven: nat -> bool, isOdd: nat -> bool ⟩]) (λm.
    λ⟨
        isEven: λn. match n {
            Nat.zero as n => return true
            Nat.succ as n => return (force m::isOdd) (n.0)
        }
        isOdd: λn. match n {
            Nat.zero as n => return false
            Nat.succ as n => return (force m::isEven) (n.0)
        }
    ⟩
)

이제 위 코드를 대충 타입 검사할 수 있는 거 같다.

이제 시맨틱은 필요한 만큼 구현했으니 드디어 신택스나 코드젠으로 넘어갈 수 있겠다.