newt/TODO.md

TODO

I may be done with U - I keep typing Type.

• Generate some programs that do stuff

• import

• consider making meta application implicit in term, so its more readable when printed

  • Currently we have explicit App surrounding Meta when inserting metas. Some people leave that implicit for efficiency. I think it would also make printing more readable.

• eval for case (see order.newt)

• dynamic pattern unification (add test case first)

• switch from commit/mustWork to checking progress

• type constructors are no longer generated? And seem to have 0 arity.

• raw let is not yet implemented (although define used by case tree building)

• there is some zero argument application in generated code

• get equality.newt to work

  • broken again because I added J, probably need to constrain scrutinee to value

• inline metas. Maybe zonk after TC/elab

• implicit patterns

• operators

• pair syntax (via comma operator)

• matching on operators

  • top level
  • case statements

• SKIP list syntax

  • Agda doesn't have it, clashes with pair syntax

• autos / typeclass resolution

  • We need special handling in unification to make this possible
  • options
    • keep as implicit and do auto if the type constructor is flagged auto
    • keep as implicit and mark auto, behavior overlaps a lot with implicit
    • have separate type of implict with {{}}

• do blocks

• some solution for + problem (classes? ambiguity?)

• show compiler failure in the editor (exit code != 0)

• write output to file

  • uses -o option

• detect extra clauses in case statements

• add test framework

• decide what to do for erasure

• type at point in vscode

• repl

• LSP

• don't match forced constructors at runtime

  • I think we got this by not switching for single cases

• magic nat (codegen as number with appropriate pattern matching)

• magic tuple? (codegen as array)

• magic newtype? (drop in codegen)

• records / copatterns

• Read Ulf Norell thesis