broom-lang / broom Goto Github PK

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

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

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).

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

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

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

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.

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

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

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

With lazy sweep using wraparound counter mark bytes.

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).

It should be convenient to integrate this to WellFounded.

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

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

We do have some rudimentary highlighting support in /vim.

Simplify it until it can be formalized.

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

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.

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

Just plagiarize GHC's setup.

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

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

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

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.

• 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

It is repetitive spaghetti.

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

Unlike #16, just requires parser support.

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

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.).

Add string literals with \-escapes.