Skip to content

Latest commit

 

History

History
133 lines (113 loc) · 7.38 KB

Readme.md

File metadata and controls

133 lines (113 loc) · 7.38 KB

Types and Programming Languages

stack cabal lint format Netlify Status

Quick Start Guide

$ git clone https://github.com/waddlaw/TAPL.git
$ cd TAPL
app versionn
cabal-install 3.2.0.0
stack 2.5.1
cabal-fmt 0.1.5.1
ormolu 0.1.4.1

Available Systems

id chapter package name parse eval typecheck prettyprint run application
1 ch03 bool ✅ ✅ N/A ✅ stack run bool
2 ch03 arith ✅ ✅ N/A ✅ stack run arith
3 ch05 lambda-untyped ✅ ✅ N/A ✅ stack run untyped-lambda
4 ch09 lambda-simple ✅ ✅ ✅ ✅ stack run simple-lambda
5 ch11 lambda-fullsimple ✅ ✅ ✅ ✅ stack run fullsimple-lambda
6 ch19 featherweight-java ✅ ✅ 🚧 ✅ stack run fj
7 ch22 recon 🚧 ✅ 🚧 ✅ 🚧
8 ch23 systemf 🚧 🚧 🚧 ✅ 🚧

Components

Fig System Name 1 2 3 4 5 6 7 8
3-1 Booleans (B) ✅ ✅ ✅ ✅ ✅ ✅
3-2 Arithmetic expressions (NB) ✅ ✅ ✅ ✅
5-3 Untyped lambda-calculus (λ) ✅
8-1 Typing rules for booleans (B) ✅ ✅ ✅ ✅
8-2 Typing rules for numbers (NB) ✅ ✅ ✅
9-1 Pure simply typed lambda-calculus (λ->) ✅ ✅ ✅ ✅
11-1 Uninterpreted base types
11-2 Unit type ✅
11-3 Ascription ✅
11-4 Let binding ✅
11-5 Pairs ✅
11-6 Tuples ✅
11-7 Records ✅
11-8 (Untyped) record patterns ✅
11-9 Sums ✅
11-10 Sums (with unique typing) 🚧
11-11 Variants 🚧
11-12 General recursion 🚧 ✅ ✅
11-13 Lists 🚧 ✅
13-1 References
14-1 Errors
14-2 Error handling
14-3 Exceptions carrying values
15-1 Simply typed lambda-calculus with subtyping (λ<:)
15-2 Records (same as Figure 11-7)
15-3 Records and subtyping
15-4 Bottom type
15-5 Variants and subtyping
16-1 Subtype relation with records (compact version)
16-2 Algorithmic subtyping
16-3 Algorithmic typing
19-1 Featherweight Java (syntax and subtyping) ✅
19-2 Featherweight Java (auxiliary definitions) ✅
19-3 Featherweight Java (evaluation) ✅
19-4 Featherweight Java (typing) 🚧
20-1 Iso-recursive types (λμ)
22-1 Constraint typing rules ✅
22-2 Unification algorithm ✅
23-1 Polymorphic lambda-calculus (System F) ✅
24-1 Existential types
26-1 Bounded quantification (kernel F<:)
26-2 "Full" bounded quantification
26-3 Bounded existential quantification (kernel variant)
28-1 Exposure Algorithm for F<:
28-2 Algorithmic typing for F<:
28-3 Algorithmic subtyping for kernel F<:
28-4 Algorithmic subtyping for full F<:
28-5 Join and meet algorithms for kernel F<:
29-1 Type operators and kinding (λω)
30-1 Higher-order polymorphic lambda-calculus (Fω)
30-2 Higher-order existential types
30-3 Parallel reduction on types
32-1 Polymorphic update

Development

# build
$ stack build --fast --file-watch --ghc-options "-j4 +RTS -A128m -n2m -qg -RTS"

# test
$ stack test --fast --file-watch

## generate haddock document
$ stack clean && stack haddock

## benchmark
$ stack bench --benchmark-arguments "--small"

Other commands

# pedantic
$ stack clean && stack test --fast --pedantic --file-watch --no-run-tests

# hlint
$ make lint

# format
$ make fmt
$ make cabal-fmt

Japanese book information

型システム入門 プログラミング言語と型の理論