type checker plug and play

Stream: general

[Johan Commelin]

Call me type checker curious. Is there some sort of framework where you can easily build your own type checker, by just writing some simple specs. E.g., you specify the judgment rules in some variant of BNF + epsilon and the framework spits out a type checker.

[Tim Daly]

I would dearly love to see this. I have tried to reverse engineer the judgement rules without success.

[Marc Huisinga]

andrej bauer recently gave a talk on a future tool like this at icfp 2019 https://youtube.com/watch?v=YZqOVsuyQyQ

[Johan Commelin]

Cool, I'm going to watch this

[Tim Daly]

Bauer also gave a talk on Vimeo "How to Implement Type Theory in an Hour (https://vimeo.com/286652934) but I need the rules rules implemented by Lean

[Johan Commelin]

Bauer also gave a talk on Vimeo "How to Implement Type Theory in an Hour (https://vimeo.com/286652934) but I need the rules rules implemented by Lean

Those rules are in Mario's thesis

[Sebastian Ullrich]

As for perhaps more mature tools, redex is quite popular. You need to know a bit of Lisp/Racket, but... the good thing about Lisp is that there isn't much to know about it.

[Tim Daly]

Has anyone tried to implement Lean's rules in Andromeda?

[Tim Daly]

Meta-theoriy of type theories.... let the recursion begin :-)

[Tim Daly]

Interesting points about humans using type assistants at about minute 35

[Johan Commelin]

@Marc Huisinga Thanks for the link to the talk about Andromeda. It's really cool.

[Marc Huisinga]

no problem! @Olli posted it here once before for the comments on itp in general.

[Tim Daly]

It is interesting that these ideas from the proof community show up (in different words) in the computer algebra area. His comment about implicit coercions (especially since Axiom has first class dependent types) has to be handled on an ad-hoc basis in Axiom since it isn't decidable.

[Tim Daly]

Around minute 46 he talks about "callbacks", where the "User code" (in my case Axiom) is used as an Oracle (my term) for things like judgement equality.Equality checking can be "computed" in Axiom. Computer algebra allows computing equality in many special contexts (e.g. "Is this equal to that" in the current context of a non-abelian domain (e.g. matrix).

[Tim Daly]

You might have a type A as a polynomial with fractional coefficients and need to see if it is equal to type B which is a fraction of polynomials with integer coefficients. Axiom can do this.

[Mario Carneiro]

Note that in Andrej's case, the callback for equal(A,B) is supposed to use functions from the kernel to produce a proof of |- A = B. I don't think your Axiom computations will do this

[Tim Daly]

The andromeda kernel (nucleus) isn't involved in the equal(A,B) interaction with user code, at least from what I can see from his talk. I will be reading his papers.

[Tim Daly]

Even more interesting is his distinction between proof relevant and proof irrelevant rules, such as equality. A conjecture would be that Oracle systems (i.e. computer algebra) are ideal for answering proof irrelevant questions

[Mario Carneiro]

The kernel is the only thing that produces elements of the abstract data type "judgment". This is what ensures soundness and a "small trusted kernel" mentioned earlier in the talk

[Mario Carneiro]

So user code that wants to return a proof of |- A = B has to call kernel functions in order to construct the data, that's the whole point

[Mario Carneiro]

you can't just respond "yes" to the query equal(A,B)

[Tim Daly]

The question equal(A,B) question becomes "Is there a (proven) coercion between A and B?". Given a proof of the coercion code in Axiom (already provided by a prior Lean proof) the answer to the question equal(A,B) where A is POLY(FRAC(INT)) and B is FRAC(POLY(INT)) is decideable and proof irrelevant.

[Mario Carneiro]

In Andrej's system, equal(A,B) means "please provide a proof of the convertibility of A and B, i.e. |- A = B". This proof can go by any means, including equality reflection on some theorem that you have lying around if the theory supports it, but it needs an actual proof; trusted code doesn't work for this purpose

[Tim Daly]

The Axiom Sane effort is using Lean to prove the coercion code. So the coercion becomes an axiom in Lean. There is an "actual proof" in Lean which is a proof of the Axiom code, the proof can be provided as it is carried with the code.

[Tim Daly]

The coercion code is essentially a Lean tactic.

[Tim Daly]

Ultimately the Axiom algorithms can all be used as Lean tactics or Lean axioms once they are proven.

[Tim Daly]

One could compute a GCD by calling the Axiom code rather than using Peano