Paper talk: # Elaborator Reflection: Extending Idris in Idris By Edwin Brady and David Christiansen @cyberglot | November, 2021 --- In summary: - It introduces the `Elab` monad, that provides an interface to the *primitive* tactic language in Idris, plus `%runElab` which is a handler of sorts for the monad.  --- - Most (all?) Idris's higher-level features are implemented in terms of the `Elab` monad: + typeclasses + implicit arguments + type-driven disambiguation of names + local definitions + monomorphisation + (potentially others not mentioned by name) --- - More powerful tactics à la Coq can be derived from `Elab`, eg `crush` ```haskell mush : Elab () mush = do attack x <- gensym "x" intro x try intros induction (Var x) `andThen` auto solve ``` --- # Important details - Idris's TT, the tactics language and the proof state together form the development calculus, TT$$_{dev}$$ (implemented in Haskell for Idris1, implemented in Idris1 for Idris2) --- - The proof state is **not** implemented as a state effect, but rather as binders within the code that behaves similarly to `let` bindings: + `? x : t` for hole binding + `? x ~~ t : t` for guess binding - Quasi-quotation is included in TT$_{dev}$ + quoted code has type `Raw`, ie non-typecked terms + unquoted code has type `TT`, ie well typed, de Bruijn indexed terms --- - Tactics: + gensym : (hint : String) -> Elab TTName + focus : (h : TTName) -> Elab () + unfocused : (h : TTName) -> Elab () + fill : (e : Raw) -> Elab () + solve : Elab () + claim : (n : TTName) -> (t : Raw) -> Elab () + apply : (op : Raw) -> (argSpec : List Bool) -> Elab (List TTName) --- - Tactics (cont.): + compute : Elab () + rewriteWith : (rule : Raw) -> Elab () + intro : (n : TTName) -> Elab () + forall : (n : TTName) -> (t : Raw) -> Elab () + patbind : (v : TTName) -> Elab () + letbind : (n : TTName) -> (v : Raw) -> (t : Raw) -> Elab () + attack : Elab () --- - Tactics (cont.): + getEnv : Elab (List (TTName, Binder TT)) + lookupTy : (n : TTName) -> Elab (List (TTName, NameType, TT)) + lookupDatatype : (n : TTName) -> Elab (List Datatype) + lookupFunDefn : (n : TTName) -> Elab (List (FunDefn TT)) + lookupArgs : (n : TTName) -> Elab (List (TTName, List FunArg, Raw)) --- - Tactics (cont.): + normalise : (env : List (TTName, Binder TT)) -> (tm : TT) -> Elab TT + declareType : TyDecl -> Elab () + defineFunction : FunDefn Raw -> Elab () + declareDatatype : TyDecl -> Elab () + defineDatatype : DataDefn -> Elab () + metavar : TTName -> Elab () + search' : Int -> List TTName -> Elab () --- - Tactics (cont.): + debug : Elab a + debugMessage : List ErrorReportPart -> Elab a + runElab : Raw -> Elab () -> Elab (TT, TT) - Requires TypeProviders for more complex elaborations, such as records --- # Problems - Staging becomes a nightmare: + they don't specify how it is handled + they suggest looking at Racket's approach to staging - Coq-style tactics are also a nightmare - Reliance on Type Providers