ilya-klyuchnikov / Tapl Scala
Code from the book "Types and Programming Languages" in Scala
Stars: β 157
Programming Languages
scala
5932 projects
Labels
Projects that are alternatives of or similar to Tapl Scala
infrared
β¨π Blazing fast, inferred static type checker for JavaScript.
Stars: β 46 (-70.7%)
Mutual labels: type-checking
Objectmodel
Strong Dynamically Typed Object Modeling for JavaScript
Stars: β 415 (+164.33%)
Mutual labels: type-checking
Dilate
Nearly zero runtime object allocation powered by scalameta. Value class and Unboxed Tagged Type generation at compile-time.
Stars: β 80 (-49.04%)
Mutual labels: type-checking
mps-coderules
Type checking and logical inference for JetBrains MPS
Stars: β 24 (-84.71%)
Mutual labels: type-checking
Hammox
π automated contract testing via type checking for Elixir functions and mocks
Stars: β 289 (+84.08%)
Mutual labels: type-checking
Tl
The compiler for Teal, a typed dialect of Lua
Stars: β 716 (+356.05%)
Mutual labels: type-checking
floweret
Runtime type annotations for CoffeeScript (and JavaScript too!)
Stars: β 20 (-87.26%)
Mutual labels: type-checking
Babel Plugin Runtyper
β‘οΈ Runtime type-checker for JavaScript
Stars: β 117 (-25.48%)
Mutual labels: type-checking
Elixir Type check
TypeCheck: Fast and flexible runtime type-checking for your Elixir projects.
Stars: β 80 (-49.04%)
Mutual labels: type-checking
typical
Isomorphic, functional type-checking for Javascript
Stars: β 17 (-89.17%)
Mutual labels: type-checking
Write You A Haskell
Building a modern functional compiler from first principles. (http://dev.stephendiehl.com/fun/)
Stars: β 3,064 (+1851.59%)
Mutual labels: type-checking
Bazel Mypy Integration
ππΏπ Integrate MyPy type-checking into your Python Bazel builds
Stars: β 40 (-74.52%)
Mutual labels: type-checking
progge.rs
Program analysis playground for a simple, imperative language
Stars: β 29 (-81.53%)
Mutual labels: type-checking
Predicates
Predicates for type checking, assertions, filtering etc
Stars: β 89 (-43.31%)
Mutual labels: type-checking
Typology
Swift type checking and semantic analysis for developer tools
Stars: β 68 (-56.69%)
Mutual labels: type-checking
Caer
High-performance Vision library in Python. Scale your research, not boilerplate.
Stars: β 452 (+187.9%)
Mutual labels: type-checking
Typeis
Typeis. it's the smart and simple javaScript type checker
Stars: β 100 (-36.31%)
Mutual labels: type-checking
TAPL in Scala
This project is an attempt to port very nice companion code (written by Pierce in OCaml) for the book "Types and Programming Languages" by Benjamin C. Pierce into Scala.
Roadmap
-
tapl.arith
- (chapters 3, 4) -
tapl.untyped
(chapters 5 - 7) -
tapl.fulluntyped
(chapters 5 - 7) -
tapl.tyarith
(chapter 8) -
tapl.simplebool
(chapter 10) -
tapl.fullsimple
(chapter 9 and 11) -
tapl.fullref
(chapter 13, 18, based ontapl.fullsimple
) -
tapl.fullerror
(chapter 14, based ontapl.simplebool
) -
tapl.rcdsubbot
(chapter 15, rcd=record) -
tapl.fullsub
(chapters 15 - 17, based ontapl.fullsimple
) (The only addition is Top type) -
tapl.joinsub
(chapter 16) - Not yet done. This is a subset oftapl.bot
. -
tapl.bot
(chapter 16) - simplification oftapl.rcdsubbot
. -
tapl.fullequirec
(chapter 20). -
tapl.fullisorec
(chapter 20). -
tapl.equirec
(chapter 21). The subtyping was not implemented in original code. But there is a code in the Book. -
tapl.recon
(chapter 22). -
tapl.fullrecon
(chapter 22). -
tapl.fullpoly
(chapters 23, 24). -
tapl.fullomega
(chapters 23, 29, 30). -
tapl.fullfsub
(chapters 26, 28) - based ontapl.fullsimple
(additions: Top type and subtyping). -
tapl.fullfomsub
(chapters 26, 31). -
tapl.fullfsubref
(chapter 27) - original (a bit wrong) implementation. Not yet ported. -
tapl.fullfomsubref
(chapter 27) combination of all systems from the book. -
tapl.purefsub
(chapter 28) - a subset oftapl.fullfsub
. Not yet ported. -
tapl.fomsub
(chapter 31) - simplification oftapl.fullfomsub
. Not yet ported. -
tapl.fullupdate
(chapter 32) - simplification oftapl.fullfomsub
. Not yet ported. -
tapl.fomega
(solution to 30.3.20) - not yet ported. -
tapl.letexercise
- not yet ported. -
tapl.joinexercise
- not yet ported.
Code structure.
The code structure for each implementation follows original code structure and consists of 4 files:
-
syntax.scala
- AST, contexts, commands, pretty-printing. -
parser.scala
- parsing. -
core.scala
- evaluator and typer. -
demo.scala
- the main application for processing input files.
Start playing with me
sbt
> run
Multiple main classes detected, select one to run:
[1] tapl.fullisorec.FullIsorecDemo
[2] tapl.rcdsubbot.RcdSubBotDemo
[3] tapl.arith.ArithDemo
[4] tapl.simplebool.SimpleBoolDemo
[5] tapl.equirec.EquirecDemo
[6] tapl.tyarith.TyArithDemo
[7] tapl.untyped.UntypedDemo
[8] tapl.fullfsub.FullFSubDemo
[9] tapl.fullpoly.FullPolyDemo
[10] tapl.recon.ReconDemo
[11] tapl.fullfomsub.FullFomSubDemo
[12] tapl.fullerror.FullErrorDemo
[13] tapl.fulluntyped.UntypedDemo
[14] tapl.fullsub.FullSubDemo
[15] tapl.fullequirec.FullEquirecDemo
[16] tapl.fullrecon.FullReconDemo
[17] tapl.fullref.FullRefDemo
[18] tapl.fullomega.FullOmegaDemo
[19] tapl.fullsimple.FullSimpleDemo
[20] tapl.fullfomsubref.FullFomSubRefDemo
[21] tapl.bot.BotDemo
Enter number: 21
[info] Running tapl.bot.BotDemo
====================
(lambda x: Top. x): Top -> Top;
||
\/
(lambda x: Top. x): Top -> Top;
====================
((lambda x: Top. x) (lambda x: Top. x)): Top;
||
\/
(lambda x: Top. x): Top -> Top;
====================
((lambda x: Top -> Top. x) (lambda x: Top. x)): Top -> Top;
||
\/
(lambda x: Top. x): Top -> Top;
====================
(lambda x: Bot. x): Bot -> Bot;
||
\/
(lambda x: Bot. x): Bot -> Bot;
====================
(lambda x: Bot. x x): Bot -> Bot;
||
\/
(lambda x: Bot. x x): Bot -> Bot;
> run-main tapl.fulluntyped.UntypedDemo progs/fulluntyped.tapl
[info] Running tapl.fulluntyped.UntypedDemo progs/fulluntyped.tapl
====================
tru;
||
\/
(lambda t. lambda f. t);
====================
fls;
||
\/
(lambda t. lambda f. f);
====================
(tru tru);
||
\/
(lambda f. lambda t. lambda f'. t);
====================
(tru fls);
||
\/
(lambda f. lambda t. lambda f'. f');
====================
(test tru v w);
||
\/
((lambda m. lambda n. (lambda t. lambda f. t) m n) v w);
...
Notes.
There was some incompleteness in the original OCaml code that was ported into Scala code:
-
tapl.equirec
- subtyping was not implemented - For subtyping for References, Sources and Sinks (scattered across many implementations) there is a comment in the original code that implementation is incomplete.
See code for calculation of
meet
andjoin
of two references. - It will be interesting to add implementation of dependent types from the sequel book "Advanced Topics in Types and Programming Languages".
The book mentions OCaml implementation
deptypes
but I did not find this implementation on the web. - I have noticed that some cases (in typers and evaluators) were omitted in the original code.
Note that the project description data, including the texts, logos, images, and/or trademarks,
for each open source project belongs to its rightful owner.
If you wish to add or remove any projects, please contact us at [email protected].