This is an exercise repository of Implement Programming language according to the book TaPL (Types and Programming Language)
> cabal sandbox init
> cabal install --only-dependencies
> cabal configure
> cabal build
> cabal install
> tapl-hs
TaPL-hs REPL
========================================
0) Exit
1) Sarith (from Chapter 3-4)
2) Sulamb (from Chapter 5-7)
3) Tyarith (from Chapter 8)
----------------------------------------
Select Mode (default: 2) >> # enter language index (quit for 0)
Sulamb>> cabal sandbox init
> cabal install --only-dependencies
> cabal configure --enable-tests --enable-library-coverage
> cabal build
> run-cabal-test --show-details=always
> cabal runSarith is programming language according to TaPL Chapter.3-4 Tyarith is according to Chapter.8
This language's syntax is like scheme
true ; boolean true
false ; boolean false
0 ; natural number zero(succ 0) ; => 1
(pred 0) ; => 0
(succ (succ 0)) ; => 2
(pred (succ 0)) ; => 0
(succ (pred (succ 0))) ; => 1
(succ true) ; => TypeError
(pred true) ; => TypeError(zero? 0) ; => true
(zero? (succ 0)) ; => false
(zero? false) ; => TypeError(if true 0 (succ 0)) ; => 0
(if false 0 (succ 0)) ; => (succ 0)
(if 0 true false) ; => TypeErrorSulamb is programming language according to TaPL Chapter.5-7
This language based on untype-lambda-calculus. All functions are auto curried.
(\ x x) ; identity function
(\ x (\ y y)) ; meaning λx.λy.y
(\ (x y) y) ; meaning λxy.y (the same as λx.λy.y)
(f x) ; apply function `f` with `x`
(\ (l m n) (l m n)) ; λlmn.l m n
;; Example
(id) ; => (\ x x)
(id (\ y y)) ; => (\ y y)
(id (id (\ w w))) ; => (\ w w)(tru) ; Church-true
(fls) ; Church-false
(tst p t f) ; Church-if
(and a b) ; Church-and
(or a b) ; Church-or
;; Example
(tru) ; => (\ t (\ f t))
(fls) ; => (\ t (\ f f))
(and tru tru) ; => tru
(and fls tru) ; => fls
(or fls fls) ; => fls
(or fls tru) ; => tru
(tst tru (\ v v) (\ w w)) ; => (\ v v)
(tst fls (\ v v) (\ w w)) ; => (\ w w)(zro) ; Church-zero
(one) ; Church-one
(scc x) ; Church-succ
(zro? x) ; Church-zero?
;; Example
(zro? zro) ; => tru
(zro? one) ; => fls
(zro? (scc zro)) ; => fls(pir v w) ; Church-pair constructor
(fst p) ; Church-fst
(snd p) ; Church-snd
;; Example
(fst (pir (\ v v) (\ w w))) ; => (\ v v)
(snd (pir (\ v v) (\ w w))) ; => (\ w w)