Study of language design and implementation.

The aim of this repository is to quickly make prototypes for language design ideas.

This repository contains a series of language implementations,
and some general supporting libraries (such as parsing and command line interface).

Remember,
an engineer solve problem,
an engineer does not want just a religion about how to solve a problem.
-- Gerry Sussman

• partech
  A parser generator, with various parsing techniques.
  • Earley parser
    Its time complexity is O(n^3) in general for context free grammar.

• eopl/lang_let
  
  • Basic scope.
• eopl/lang_proc
  
  • Lexical scope and closure.
• eopl/lang_letrec
  
  • Recursive scope, implemented by a trick during variable lookup.
• eopl/lang_nameless
  
  • Nameless scope, a.k.a. De Bruijn index.

• eopl/lang_explicit_refs
  
  • Explicit reference (address)
• eopl/lang_implicit_refs
  
  • We need to distinguish denoted value from expressed value for mutable variable.
    This is also called call-by-value parameter passing.
• eopl/lang_mutable_pairs
  
  • Lisp's cons, car and cdr, with set-car! and set-cdr!
• eopl/lang_call_by_reference
  
  • Marking an variable ref when passing it to a function,
    will not create new ref and reuse the ref of the variable,
    thus make callee be able to set caller's variable.
• eopl/lang_call_by_need
  
  • When an expression occurs as argument of an application,
    do not eval it, but make it into a thunk.
    and only eval it when needed (during variable lookup).
  • This is also called lazy-eval.

• barendregt/de_bruijn
  
  • De Bruijn style simple type lambda calculus,
    implemented by term rewriting.

• eopl/lang_checked
  
  • A type-checked language derived from lang_letrec.

• eopl/lang_infered
  
  • A type-infered language derived from lang_letrec.

• nbe/lambda
  
  • The untyped lambda calculus.
• nbe/syst
  
  • Kurt Gödel's system T.
  • Simply typed lambda calculus with natural number.
• nbe/tartlet
  
  • "Checking Dependent Types with Normalization by Evaluation: A Tutorial",
    by David Thrane Christiansen (the original tutorial).
  • Since tartlet is little pie, recursion is also not an option here.
• nbe/minitt
  
  • "A simple type-theoretic language: Mini-TT",
    by Thierry Coquand, Yoshiki Kinoshita, Bengt Nordström, Makoto Takeyama.
    
  • No termination check, thus when viewed as logic it is unsound.

• adventure/jojo_untyped
  
  • De Bruijn notation extended by function composition,
    implemented by stack machine and threaded code techniques,
    which is commonly used for Forth (programming language).
• adventure/jojo_simple
  
  • Two level of compositions -- exe and cut, where cut is simple.

• "Parsing Techniques -- A Practical Guide"
  • by Dick Grune and Ceriel J.H. Jacobs.
• "Essentials of Programming Languages" (a.k.a. EOPL)
  • by Daniel P. Friedman and Mitchell Wand.
• "Lambda Calculus with Types"
  • by Henk Barendregt, Wil Dekkers and Richard Statman. 2010.
• "Do-it-yourself Type Theory"
  • by Roland Backhouse, Paul Chisholm, Erik Saaman and Grant Malcolm, 1988.
• "Computation and Reasoning -- A Type Theory for Computer Science"
  • by Zhaohui Luo, 1994.

• Build: sbt stage
  • Then you can find executable files in ./target/universal/stage/bin/
• Test: ./dev t
• Example code at: example

Contributions are welcome, see current TODO list for tasks.
(Please add yourself to the AUTHORS list if you made any contributions.)

• We enforce C4 as collaboration protocol.
  • The C4 RFC
• Style Guide
  • Observe the style of existing code and respect it.
• Code of Conduct
• Travis CI

• GPLv3