brainshitting reviewed

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 memo

IDEA

- 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

Leave a Reply