atennapel / deplang-jvm Goto Github PK

ARCHIVED: see https://github.com/atennapel/tynka for a new implementation of this idea

Experimental implementation of a "dysfunctional" programming language. The idea originates from this presentation by Andras Kovacs: https://www.youtube.com/watch?v=ai4vU1Naopk .

We have a language with two layers, one compile-time layer with full dependent types and a runtime-layer with a simply-typed language without higher-order functions or closures. We can get back higher-order functions and polymorphism in the compile-time layer, but after staging we get a very simple language that is easy to compile.

Try it out:

sbt "run examples/Test"
javac jvmstd/Pair.java
javac jvmstd/List.java
java Test

TODO:

• Surface syntax
• Parsing
• Core syntax
• Values
• Evaluation
• Unification
• Globals
• Elaboration
• Pretty printing
• Staging
• IR syntax
• Metas, zonking and unification
• Meta insertion
• Sigmas
  • Syntax
  • Parsing
  • Elaboration
• IR simplifier
• IR lambda removal: eta expansion, closure conversion, lambda lifting
• Bytecode generation
  • Primitives
  • Boxing/unboxing
  • main method
  • Definitions without parameters to static properties
• Named sigma projection
• Bool type with if expression
• Allow if to return lambdas
• Fixpoint
• Add Int and primitive binops
• Remove Nat
• Tail recursion
• Primitive polymorphic list datatype
  • Type
  • Constructors
  • Elimination
• More simplification: case-of-case, app and case commutation
• Better inlining (inline linear lambdas, constants, globals)
• Combine jumps (for example if+comparisons)