Miscellaneous

[MonoidMusician]

Just a place to record my unorganized todo list:

• [x] (Recursive) zippers for Expr
• [x] Directed zippers: first/last, next/prev (or just use traversable for that? seems inefficient ...)
• [x] Import resolution algorithm forall f m s a void. (a -> f (Expr m s a)) -> Expr m s a -> ?f (Expr m s void) (what monad (transformer) will this run in?? it needs to ensure it is acyclic; maybe it will take a traverse argument to allow batching requests)
• [ ] WIP: Pretty printing #8
• [ ] Just need to figure out how to do interact with ints better ...
• [ ] Basic interactive editing (using change structures?)
  • [ ] Do we need to record focus of Strings?
• [ ] Normalizing and typechecking incomplete ASTs (I guess this is just unification of metavariables)
  • [ ] What's the minimal checking we need to do to make sure normalizing is safe, i.e. finite? Maybe typechecking with unification will be good enough, since holes will unify with anything (but have to make sure it is consistent)
  • [ ] Should those algorithms happen in an incremental computational monad that bounds recursion?
• [x] Inject and Interpret https://github.com/dhall-lang/dhall-haskell/blob/master/dhall/src/Dhall.hs#L553-L1460 (now with row types! 😄)

Stretch goals:

• [ ] Use dhall itself to configure interactive commands/UI elements
  • [ ] Maybe we're going to have to construct a DSL of finite Container functors that support just what we need ...
• [ ] Need to find some way to integrate comonadic UIs, obviously.
• [ ] Incrementalize things
  • [ ] Related: need a datatype (and printer!) for change structures that could be used to pretty-print diffs like the Haskell lib.
• [ ] Prove things
• [ ] Interactive normalization stepper (this could be the basis for interactive rewrite proofs too)
• [ ] Interactive type checking judgments/algorithms and such, to tell the user why it’s wrong.

[MonoidMusician]

Known bugs ATM:

• [x] SetSelection does not seem to work on deeper selections
• [x] Typing (Lam : Pi) App with (Pi -> Lam) App might result in wrong universe level

[MonoidMusician]

Generalize everything!

• [ ] Extensible locations
• [ ] Let Oxpr take outside annotations too (monoidal?)
• [ ] Let typechecking occur in any bind+applicative (hmm I'm not entirely sure this one is necessary …)