broom-lang / broom

A programming language with first-class modules and algebraic effects.

Broom

A programming language with first-class modules and algebraic effects. Still very much a work in progress (i.e. not yet usable).

(Planned) Features

• Functional-first, with strict evaluation
• ML-style module system with higher-order, recursive and first-class modules
  • Records and modules are the same, à la 1ML
  • First-class ML-modules also provide higher-ranked and higher kinded types
    • with impredicative instantiation
  • Modular implicits support ad-hoc polymorphism and type level programming
• Algebraic effects and effect handlers
• Row typed modules, records, polymorphic variants and effects
• Conventional and simplified syntax
  • extensible with procedural hygienic macros
• Optimizing whole-program compilation to Javascript or (later) native code

(Abstract) Syntax

program ::= defs
repl_input ::= stmts

stmt ::= def | expr
stmts ::= (stmt (";" stmt)*)? ";"?
alts ::= (stmt ("|" stmt)*)? "|"?

def ::= pat "=" expr
defs ::= (def (";" def)*)? ";"?

exprs ::= types ::= (expr ("," expr)*)? ","?

expr ::=
pat ::=
type ::= 
    | type ("-!" type)? "->" type
    | type "=>" type

    | expr ":" type
    | expr "||" expr
    | expr "&&" expr
    | expr ("==" | "<" | "<=" | ">" | ">=") expr
    | expr ("+" | "-") expr
    | expr ("*" | "/") expr
    | expr OTHER_INFIX expr
    | expr expr+
    | PREFIX expr
    | expr POSTFIX
    | expr "." ID

    | "{" ("|" pat ("," pat)* "->" expr)+ "}" (* function literal *)
    | "{" "|" "->" stmts "}" (* thunk *)
    | "{" "|" "}" (* empty function (uncallable) *)
    | "{" ("|" pat ("," pat)* "=>" expr)+ "}" (* implicit function literal *)
    | "{" stmts "}"
    | "[" exprs "]"
    | "(" exprs ")"
    | "(" ( "||" | "&&"
          | "==" | "<" | "<=" | ">" | ">="
          | "+" | "-"
          | "*" | "/" | "%" ) ")"
    | "{" ":" stmts ")"
    | "[" "|" alts "]"
    | "(" "|" alts ")"
    | "(" ":" types ")"

    | ID
    | "_"
    | CONST

See the intro for a slightly more detailed exposition.

broom's Issues

Replace Nipo with ml-lpt

Typechecker should prevent duplicate definitions in block scopes

E.g. val foo = 1 val foo = 2 should not be accepted (because forward and recursive references are allowed).

CPS IR and conversion

It would be cool to do something like Thorin and Guile's "CPS Soup".

Build on sml/nj

NJ uses its own CM format instead of MLB files. For extra points, generate the CM and MLB from the same source with cm2mlb or similar.

Reduce pattern matching to switching and letting

Segregated-fits Allocation for Major Heap

Grammar spec

Register allocation

Instruction selection

Mostly-concurrent Major GC

"Marketing" documentation

Add some exposition of goals/features/syntax so that people can decide whether they want to contribute to or (eventually) use this.

Complect lambdas

Fn and TFn should be fused as in 1ML so that type lambdas have no runtime component that the compiler needs to reason about (closures, passing continuation to calls etc.).

Single-threaded semispace collector

Prevent name capture in polymorphic types

Effect rows and handlers

ATM we just have the pure/impure distinction of 1ML. I would like something like Koka or Multicore OCaml. There will be nontrivial interactions with 'large' (higher-rank etc.) types and functor generativity.

Prevent duplicate fields with implicit 'lacks' constraints

Emit JS

Refactor Main module

It is repetitive spaghetti.

Shrinking optimizations

So that e.g. subtyping coercions can produce sloppy code. See Shrinking Lambda Expressionsin Linear Time and Shrinking Reductions in SML.NET. #12 should make this a lot easier.

Fixed set of infix operators

Unlike #16, just requires parser support.

Report type errors in surface syntax

I.e. back-convert types to Cst.typ.

Include `Def.Id.t` and `Pos.t` in defs

So that defs are unique and error-reportable, respectively.

Use literate programming (at least for type rules)

Polymorphic intrinsics

(Parametrically) polymorphic intrinsics for e.g. arrays.

• Higher-kinded primitive array type
• Array ops (new, length, index, initialize)
• Array type op
• Evaluation

Refactor well-foundedness analysis

Simplify it until it can be formalized.

Closure conversion

Generational collector with mark and sweep major heap

With lazy sweep using wraparound counter mark bytes.

Make unification return a coercion type

Convenient variable representation for FAst

Some sort of use-def/def-use pointers and stuff like in the imperative version of "Shrinking Lambda Expressions in Linear Time" and "Shrinking Reductions in SML.NET" would be convenient for optimization. Alphatization is not as convenient and mangles the names, which is bad for debugging and especially error messages.

E.g. ATM the well-foundedness analysis must construct scope trees to deal properly with scoping without mangling the names (to keep error messages intelligible).

Build on Windows

Use `DefId`:s in `WellFounded`

Should help correctness of WellFounded tremendously. Can also remove ScopeId:s from FAst.

Remove Pos.t from types

It isn't useful in error reporting because types flow around.

`do` vs. `begin`/`module` distinction

• begin and module (and toplevel) contain recursive, unique definitions. Runtime effects are forbidden because of the continuation capturing variable initialization trainwreck, but it also makes sense on a higher level to demand purity. The 'dynamically determined implementation of static type' effect should be allowed though. Could even ban expression-statements here is since they are useless anyway.
• do contains sequential statements that can have side effects and shadow names.

• Change do -> begin
• Add sequential do
• Ban effects in recursive contexts

Build on OSX

HAMT data structure for CPS

Elaborate forward refs to `__boxNew`, `__boxInit` and `__boxGet`

It should be convenient to integrate this to WellFounded.

• Add box type and intrinsics
• Make WellFounded elaborating, adding the functionality of lex-straighten.

GC Block Layer

Just plagiarize GHC's setup.

Clarify (and extend) record (type) constructs' syntax and implementations

Empty, extension (with), update (where), restriction (without) for records, modules, record types, interfaces. Also field access and patterns for records and modules.

• Spec
• with and where for records
• with and where for record types
• extends and override syntax for modules and interfaces
• without for records and record types, exclude for modules and interfaces

Add intrinsics

Use __iAdd syntax like e.g. C and Python.

Trivial contification

Obviously local functions should not cause closure allocation. With a bit more effort this can also subsume conversion of (self) tail recursion to loops.

Algebraic datatypes

Support for your favorite editor

Vim and Emacs have their own issues since we should at least have those.

Multi-param functor types

pi a b -> a = pi a -> pi b -> a and pi a b => a = pi a => pi b => a.

Emacs mode

String literals

Add string literals with \-escapes.

Modular implicits

The 'anti-modularity' of type classes is even more awkward with first-class modules than regular ones. Plus we don't have generalization so type class parameters can't be inferred any more than implicit parameters. Obviously the challenge with implicits is that implicit search must be exhaustive, which is potentially very slow.

• Enable backtracking wrt. unification variables
• Match implicit fn codomains before domains in subtyping and unification
• Schedule resolutions for when unification variables go out of scope
• Ensure termination of resolution

Vim mode

We do have some rudimentary highlighting support in /vim.

Flatten matches and check coverage (and redundancy)

'Zero-cost' functor fixpointing support

I.e. the box trickery from "A Type System for Well-Founded Recursion", except that we would only use it for functor parameters (and not local recursion as that paper does also).

Custom infix operators

Much as in Haskell, except we need to deal with more advanced modules which I've heard can get tedious.