Last week we went through the brainshitting list we produced in Durham early this year to see where we are and where we should go. A bit delayed here is the commented list:
ACTION
- with rule
abstractor, type checker>> needs more equipment, & more think. (MRF)
- elaborated TT API
>> more or less ready
- comments, bracket simplification
>> comments still to be decided, brackets improved.
- local undo = global redo + more info
>> Another MRF. Plan: minor refinement of global redo.
>> more precise tracking should be considered in the future.
>> (requires more funding).- elaborator api
. diagnostics>> There is an api. No essential difficulty – on the way.
>> line numbers have been done.. pig porn
>> i.e. latex or [XML generator + rendering].
- modules => namespace A.(x + y)
>> we have organized the machine namespace (to fix sharing).
>> This may also help for the user namespace but this requires further action.
>> Established better scope conventions (now last phase of the front end).- more predictable, even if more restricted implicit syntax
>> Design is done:
>> by default implicit args are only in the beginning, order never matters.
>> If you want to have them in the middle, you have to use nested rules.
>> See http://www.e-pig.org/epilogue/index.php?p=57- sigma types, records
>> more syntax for them.
>> design to be done, future research topic- eta expansion in binders
>> well in hand.
- from => to rhs
>> e.g. lam x y z < = case ...
>> in hand.
- elim
>> easy.
- stacked rhs
>> i.e. < = case x <= case y
>> no problem.
PLAN
- scoped comments
>> moved to ACTION
- batch interface
>> moved to ACTION
- standard library
>> in progress
- static & dynamic compiler (brady-style)
- simple context menus
- datatypes with interpretation fn
- Epigram in Epigram
- delayed rec by memoIDEA
- primitive types (what to do?)
>> move to plan, what to do with large enums?
>> e.g. a view: is it x?- bigint as an efficent implementation of nat
>> progress made, moved to ACTION
- interface to real world, foreign fns (Edwin compiler)
- Eclipse
- simultanous datatype and function defns (local & mutual)
- theorem prover view
- coinduction
- literate Epigram
- customizable elaboration
- universe polymorphism (consistent epi)
- partiality monad (general recursion)
- support for programming in any (idiomatic) cat
- observational equality
- subsets & quotients, Prop, Real
- (commercial) applications
. PCC
. embedded apps
. assessment
. MCS
- linear types
- subtypes
- refactoring, e.g. lists -> vecs
- small trusted base => inductive schemes
- tactics for proofs and programs