History

[SkySkimmer]

My current understanding of the history of Andromeda design is basically as follows:

• let's have equality reflection!

• reductions can behave strangely => add annotations to applications (not sure when this came up)

• type checking is undecidable => plan to use handlers so the user can deal with it (eg work with some decidable equations and their own decision procedure); hints and Ocaml equality checking were used in the meantime

• at some point the bracket types were invented. They would later leave for another galaxy.

• handlers can conjure variables (eg the #mafia operation in https://github.com/Andromedans/andromeda/blob/6a592963adc586cf9926f7c21d9c26110031e235/tests/error-handle-change-type.m31) => separation of runtime environment and context (~ 2015/10)

• separate contexts need join, can provide substitution

• messing around with structure types, which ended up leaving for another galaxy (starts 2015/11)

• become more ML like with "tags" (untyped data constructors) and matching (mid 2015/11) (first test: 68ed650), used for the toy "auto" (also recursive ML functions!)

• the first attempt to use handlers for equality solving 83e4822

• using handlers for internally generated operations like #equal led to wanting default handlers => top-level handlers. Externals also came in around this time for printing things. Syntax changes like ?x in patterns instead of pre declaring pattern variables, or the yield keyword.

• (2015/12) with matching getting used, the need for assumptions became apparent. The first change in that direction 42c935f , merged bde4a47

• constants had dynamic behavior, so env got a dynamic component (containing the constant signature and the equality hints)

• (2016/01) bracket types and hints departed. Syntax changes to be more Ocaml like, with infixes and parentheses for binders. Tags changed from arbitrary arity ['tag] to declaring [tag] with a specific arity. Operations changed from arbitrary arity [#op] to declared [op].

• equality checking was able to give more work to the user with the [as_prod] etc operations

• the AML equality checker and whnf algorithm was created (merged f567d28 2016/01/12) with crazy C preprocessor style hacks to update hints in the toplevel.

• hints got less hacky by being passed around as state, but this prevented using top-level handlers with hints. Also the simultaneous ban on top-level variable shadowing made the new [let hints = add_hint hint hints] system immediately obsolete.

• [ref] got added. At the same time the environment got abstracted into the computation monad and the new toplevel monad (which is just the reader monad for env).

• "config" external ("time" appeared some time before), and primitive strings to make it work. Also the [fail] command.

• 2016/01/19: the day Andromedans lost their spines (39c8f47)

• also stopped simplifying when printing, and renamed [check] to [do]

• 5752cb1: AML equality checker understood eta hints

• 0410b99: constants lost their parameters

• 2016/02: before 1771733 the assumptions on the top node of a term were not all the assumptions that were necessary to type it, you had to gather assumptions from all subterms too. Doing this gathering on term construction was a significant speedup, plus it makes thinking about assumptions easier.

• before cd7e90a we tried to give the user a chance to massage the context before abstracting a term. For instance in [lambda T, assume x : T in x], the system would say "please give me a replacement for x whose non-T variables do not depend on T, since I want to abstract T". Then the user would say "assume y : forall T' : Type, T'; then replace x by (y T) in the term to be abstracted". The code for this was hard to understand so it was decided to make the user just assume properly quantified variables in the first place.

• signature types had to be named (like records in ocaml). I forgot what the point of this was. Maybe something about checking mode?

• 6e88d3d: ability to know if an operation was emitted in checking mode for some type. Useful for stuff like implicit arguments or the hippy handler (28b005c)

• 1a92883: sharing constraints on signature types (eg [Semigroup using G = nat]). This left the galaxy later.

• 397e04e: mutually recursive ML functions

• 11f760f: equality checker understands reduction annotations

• 2016/03: b358774: Dynamic variables, and hints use them.

• started working on AML types

• 80b13ae: structures left us, 46cebdc: simplify left us

• ff2b9aa: the nucleus becomes fully abstract and safe

• 2016/04: continued AML types, merged in 394a5c7

• cfab059 inferred argument system all in AML

What did I miss?

[andrejbauer]

There's a bit of prehistory. The whole things started as an attempt to implement Voevodsky's HTS. Chris and I implemented something that had types, fibered types, intensional identity type and an extensional identity type, a la HTS. It also had universe levels. It was very hairy. And we had equality hints built in, except that we did not know exactly what they were or how they should be used.

BTW, thanks for this overview. We might want to move it to the wiki.

[andrejbauer]

And some afterhistory: we realized it's no more difficult to implement generic type theory with user-definable rules than it is to implement type theory with equality reflection. So, in Andromeda 2 that's what we have.

I should also say that we could not have done it without understanding what a general type theory is, thanks to the theoretical work done with @peterlefanulumsdaine and @haselwarter.

[JasonGross]

reductions can behave strangely => add annotations to applications (not sure when this came up)

Does anyone remember where this was discussed? I'm trying to recall what the reasoning for this was.

[JasonGross]

Ah, I guess it was in http://math.andrej.com/2015/05/19/the-troublesome-reflection-rule-types-2015-slides/ and https://groups.google.com/forum/m/#!msg/homotopytypetheory/qydSwbvj1uE/ELiFEqtXBwAJ

[mikeshulman]

thanks to the theoretical work done with @peterlefanulumsdaine and @haselwarter.

So when are you going to publish that? (-: