This compiler can lower a type theoretic lambda calculus into efficient LLVM IR code. Each expression is strictly evaluated, and functions are call-by-value. The languages provide primitives for pointers, arrays, and c-strings. It even includes stack and heap managment, and allows for mutation and unchecked side-effects. These are dangerous, but the theories provided are intented as compiler targets for more advanced theories, which can type-check on usages and side-effects. So far, the theories provided are Simply-Typed Lambda Calculus (STLC) and SystemF.
This code is in active development, and many features are unimplemented. In the future, we hope to have a dependent type theory of some kind, which is capable of checking resource usage. The current candidate theory is Quantitative Type Theory (QTT). Another subject of interest is laziness. We may look into an alternate backend which will compile to lazy, garbage collected code. Linear languages may also be a possible future target. Currently, it's not clear how languages should interact.
You will need llvm-8 and the latest ghc/cabal for compiling haskell.
Also, you should run cabal update to ensure you have the freshest
set of packages for haskell.
To run tests, run the command cabal new-test ttc-golden.
Currently, only .stlc files are supported. To build files,
use the command:
cabal new-run ttc -- [-o outfile] infile..
If the build succeeds, you may execute the outfile.
The default outfile is a.out.
We have a family of languages:
- LLTT: Low Level Type Theory, a calculus that easily compiles to llvm ir code.
- STLC: Simply Type Lambda Calculus
- SystemF: STLC + type variables and polymorphism
Some links to help with development
https://www.haskell.org/alex/doc/html/index.html
https://www.haskell.org/happy/doc/html/index.html (anyone have a link for v1.19 docs?)
http://l-lang.org/blog/Compiling-pattern-matching/
http://hackage.haskell.org/package/llvm-hs
http://hackage.haskell.org/package/llvm-hs-pure
https://mapping-high-level-constructs-to-llvm-ir.readthedocs.io/en/latest/README.html
https://www.microsoft.com/en-us/research/wp-content/uploads/2016/11/dps-fhpc17.pdf
https://reasonablypolymorphic.com/blog/algorithmic-sytc/
https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/putting.pdf
https://github.com/namin/higher-rank
https://github.com/garyb/infer-rank-n-types
https://www.cl.cam.ac.uk/~nk480/bidir.pdf
https://github.com/ollef/Bidirectional
http://davidchristiansen.dk/tutorials/bidirectional.pdf
https://github.com/sweirich/pi-forall