Coder Social home page Coder Social logo

brendanzab / language-garden Goto Github PK

View Code? Open in Web Editor NEW
162.0 5.0 5.0 1000 KB

A garden of small programming language implementations šŸŖ“

OCaml 93.46% Nix 0.98% Lean 0.74% GLSL 0.36% Standard ML 0.14% Prolog 2.19% Rust 2.14%
compilers dependent-types elaboration programming-languages compilation l-systems typechecking

language-garden's Introduction

Language garden šŸŒ±

Some toy programming language implementations, mostly implemented in OCaml.

These projects are mostly my attempt to understand different techniques and approaches to implementing programming languages. Perhaps from these seedlings something new and interesting might germinate?

Implementations

Elaboration

Elaboration is an approach to implementing language front-ends where a complicated, user friendly surface language is type checked and lowered to a simpler, typed core language. This approach to type checking is particularly popular and useful for implementing dependently typed programming languages, but is more widely applicable as well.

Simply typed:

  • elab-stlc-bidirectional: An elaborator for a simply typed lambda calculus that uses bidirectional typing to allow some type annotations to be omitted.
  • elab-stlc-bidirectional-stratify: An elaborator that partially stratifies a combined type and term language into a simply typed core language.
  • elab-stlc-abstract: An LCF-style elaborator that moves the construction of well-typed terms behind a trusted interface.
  • elab-stlc-unification: An elaborator for a simply typed lambda calculus where type annotations can be omitted.
  • elab-stlc-letrec-unification: Extends the simply typed lambda calculus with recursive let bindings.
  • elab-variant-unification: Extends the simply typed lambda calculus with structural variant types, inferring types eagerly using constraint based unification.

Dependently typed:

  • elab-dependent: An elaborator for a small dependently typed lambda calculus.
  • elab-dependent-sugar: An elaborator for a small dependently typed lambda calculus with syntactic sugar.
  • elab-record-patching: An elaborator of a dependently typed lambda calculus with singletons and record patching.

Compilation

These are related to compilation. Mainly to stack-machines, but Iā€™m interested in exploring more approaches in the future, and other compilation passes related to compiling functional programming languages.

  • compile-arith: Compiling arithmetic expressions to stack machine instructions and A-Normal Form.
  • compile-arithcond: Compiling arithmetic and conditional expressions to stack machine instructions and A-Normal Form.
  • compile-closure-conv: Typed closure conversion and lambda lifting for a simply typed lambda calculus with booleans and integers.

Languages

Miscellaneous programming language experiments.

  • lang-datalog: A simple Datalog interpreter.
  • lang-doc-templates: A programmable document template language that elaborates to a typed lambda calculus.
  • lang-fractal-growth: Experiments with using grammars and rewriting systems to model fractal growth.
  • lang-lc-interpreters: A comparison of lambda calculus interpreters using different approaches to name binding.
  • lang-shader-graphics: An embedded DSL for describing procedural graphics, based on signed distance functions. These can be rendered on the CPU or compiled to GLSL shaders.

Work in progress projects

While most of the above projects need more work put into them, the following projects need more work put into them and a more incomplete in comparison.

Background

As Iā€™ve been working in the area of programming languages Iā€™ve often found myself in the position of:

  • Explaining the same idea or technique over and over, but not having a minimal example I can point to.
  • Re-implementing an existing technique (either from a paper, or based on some other existing code Iā€™ve seen) in my own way, as a way of learning and understanding it more deeply.
  • Wanting a place to testing out an approach before committing to using it in a larger project (which can take time and may amount to nothing).
  • Trying to remember a technique I had spent time learning a long time ago.
  • Having an idea for a small language experiment that does not need to be part of a standalone project, but may require some build system setup.

My hope is that by collecting some of these projects and experiments together into a single repository they might be useful to others and my future self. Iā€™ve been particularly inspired by Mark Barboneā€™s small, self-contained gists implementing small type systems and solvers, and Andras Kovacsā€™ excellent elaboration-zoo (which was instrumental in helping me get my head around how to implement elaborators).

If you like this repository, you might find these interesting as well:

Development setup

With Nix

Using Nix is not required, but can be useful for setting up a development shell with the packages and tools used in this project. With Nix flakes enabled:

nix run .#arith -- compile --target=anf <<< "1 + 2 * 27"

nix-direnv can be used to load development tools into your shell automatically. Once itā€™s installed, run the following commands to enable it in the project directory:

echo "use flake" > .envrc
direnv allow

Youā€™ll want to locally exclude the .envrc, or add it to your global gitignore.

After that, dune can be used to build, test, and run the projects:

dune build
dune test
dune exec arith -- compile --target=anf <<< "1 + 2 * 27"

With opam

Alternatively, opam package definitions are provided in the ./opam directory. They drive the Nix flake, so should be up to date. I donā€™t use opam however, so Iā€™m not sure what the workflow is.

language-garden's People

Contributors

brendanzab avatar

Stargazers

 avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar

Watchers

 avatar  avatar  avatar  avatar  avatar

language-garden's Issues

On desugaring before/during type checking

Hi, thank you for your great code examples with nice documentation. One thing I was wondering when looking into elab-dependent is that we could instead perform desugaring before the actual type checking; for example, it seems that you have a list of function parameters that are desugared by the elaborator (type checker) into curried single-argument functions. However, the downside is that the type checker becomes quite involved even for this simplistic type theory without fancy extensions, such as unification or subtyping.

Is there any real example that desugaring during type checking is preferred? We could desugar some syntactic forms beforehand (e.g., during parsing or shortly before feeding the surface syntax to the type checker) and gain drastic simplification of the type system implementation.

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    šŸ–– Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. šŸ“ŠšŸ“ˆšŸŽ‰

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google ā¤ļø Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.