Miscellaneous #7
Description
Just a place to record my unorganized todo list:
- (Recursive) zippers for Expr
- Directed zippers: first/last, next/prev (or just use traversable for that? seems inefficient ...)
- 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 atraverseargument to allow batching requests) - WIP: Pretty printing 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?
-
InjectandInterprethttps://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
Containerfunctors that support just what we need ...
- Maybe we're going to have to construct a DSL of finite
- 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.