자료형의 i번째 생성자를 다음과 같이 정의할 수 있다.
단, A_i는 이 생성자가 가지는 인자의 수이다.
예를 들어, data Nat = Succ Nat | Zero를 다음과 같이 인코딩할 수 있다.
Succ :≡ λx. λc. λd. c (x c d).
Zero :≡ λc. λd. d.
도보시오: https://en.wikipedia.org/wiki/Mogensen%E2%80%93Scott_encoding -- 스콧 인코딩.
자료형의 i번째 생성자를 다음과 같이 정의할 수 있다.
단, A_i는 이 생성자가 가지는 인자의 수이다.
예를 들어, data Nat = Succ Nat | Zero를 다음과 같이 인코딩할 수 있다.
Succ :≡ λx. λc. λd. c (x c d).
Zero :≡ λc. λd. d.
도보시오: https://en.wikipedia.org/wiki/Mogensen%E2%80%93Scott_encoding -- 스콧 인코딩.
댓글 0