Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Compiler backend #9

Open
1 of 6 tasks
brendanzab opened this issue Mar 29, 2018 · 5 comments
Open
1 of 6 tasks

Compiler backend #9

brendanzab opened this issue Mar 29, 2018 · 5 comments

Comments

@brendanzab
Copy link
Member

brendanzab commented Mar 29, 2018

It would be nice to actually compile Pikelet programs!

Initial sketch of passes

We'll probably want some intermediate representations like MLton to get the higher level Pikelet code to be in better shape for passing to a back-end.

  • Raw - check/infer/elaborate -> Core
    • fill in holes
    • pass instances and implicit args explicitly
    • add explicit coercions
  • Core - A-Normalize -> A-Normal Form (Implement a pass to compile Core terms to A-Normal Form #91)
    • make evaluation order and control flow explicit
  • A-Normal Form - Closure Conversion -> Closure Converted
    • separate anonymous functions into a pair of:
      • a function pointer
      • the data containing the environment
  • Closure Converted - ??? -> SSA
  • SSA - ??? -> ...
  • ... - Codegen -> LLVM/Cretonne/Bytecode

Unresolved questions

We would like to do more work on the type system to make efficient code-gen easier. For example tracking coeffects such as usage mutliplicities (#7), and data flow annotations (allowing us to partially evaluate code at compile time). Regions would also be handy at some stage.

Another issue we'll have to face at some time is garbage collection. Ultimately it would be nice to not have to force users to use a specific allocation strategy, but figuring out how this interacts with multiplicities might be tricky. Until we have a better idea it might be be easier just to use something like the Boehm-Demers-Weiser GC in the interim.

Possible codegen targets

Some possible targets for codegen are as follows:

  • LLVM (the inkwell crate looks handy!)
  • Cretonne
  • Web Assembly (could be covered by Cretonne or LLVM)
  • Some sort of Typed Assembly Language (TAL)?
  • Custom JIT (see runtimes-WG for some ideas)

A JIT might be handy as it would allow us to embed Pikelet in existing Rust codebases. This could help us gain adoption without needing to convince folks to switch to an entirely new language in the mid-term.

Resources:

Example compilers in Rust

Sixten is another functional language with dependent types and unboxed data types. Might be worth looking there for inspiration too!

@aatxe
Copy link

aatxe commented Apr 23, 2018

Edwin Brady's thesis, Practical Implementation of a Dependently Typed Functional
Programming Language
, may also prove a useful resource here.

@brendanzab
Copy link
Member Author

I'd definitely want to have some nice documentation about the compiler like MLton's at some stage! This would make contributing easier for newcomers.

@brendanzab
Copy link
Member Author

Nice advice from @evincarofautumn:

A good way to build a compiler in my experience is to start with a simple program, like “hello world”, and make sure that end-to-end compilation works and produces the right output for just that literal program, then incrementally add stuff to the program—change the string from “hello world” to something else, add computations, take advantage of each language feature in turn and get it through the whole pipeline

So yeah, very much “one thing at a time”; at each step you have a full working (simple) compiler

@typesanitizer
Copy link

Minor correction: Sixten has unboxed types but not dependent types (at least the Readme doesn't say so).

@brendanzab
Copy link
Member Author

brendanzab commented Aug 19, 2018

It actually does have dependent types! @ollef just isn't promoting it that way (yet?). If you have a look at the core syntax, you'll see that it describes a dependently typed lambda calculus.

-- | Expressions with meta-variables of type @m@ and variables of type @v@.
data Expr m v
  = Var v
  | Meta m (Vector (Plicitness, Expr m v))
  | Global QName
  | Con QConstr
  | Lit Literal
  | Pi !NameHint !Plicitness (Type m v) (Scope1 (Expr m) v)
  | Lam !NameHint !Plicitness (Type m v) (Scope1 (Expr m) v)
  | App (Expr m v) !Plicitness (Expr m v)
  | Let (LetRec (Expr m) v) (Scope LetVar (Expr m) v)
  | Case (Expr m v) (Branches Plicitness (Expr m) v) (Type m v)
  | ExternCode (Extern (Expr m v)) (Type m v)
  | SourceLoc !SourceLoc (Expr m v)
  deriving (Foldable, Functor, Traversable)


-- | Synonym for documentation purposes
type Type = Expr

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

3 participants