Zulip Chat Archive

Stream: general

Topic: type checker plug and play


view this post on Zulip Johan Commelin (Dec 20 2019 at 08:22):

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.

view this post on Zulip Tim Daly (Dec 20 2019 at 08:31):

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

view this post on Zulip Marc Huisinga (Dec 20 2019 at 08:48):

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

view this post on Zulip Johan Commelin (Dec 20 2019 at 08:48):

Cool, I'm going to watch this

view this post on Zulip Tim Daly (Dec 20 2019 at 09:01):

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

view this post on Zulip Johan Commelin (Dec 20 2019 at 09:02):

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

view this post on Zulip Sebastian Ullrich (Dec 20 2019 at 09:05):

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.

view this post on Zulip Tim Daly (Dec 20 2019 at 09:20):

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

view this post on Zulip Tim Daly (Dec 20 2019 at 09:28):

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

view this post on Zulip Tim Daly (Dec 20 2019 at 10:16):

Interesting points about humans using type assistants at about minute 35

view this post on Zulip Johan Commelin (Dec 20 2019 at 10:17):

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

view this post on Zulip Marc Huisinga (Dec 20 2019 at 10:25):

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

view this post on Zulip Tim Daly (Dec 20 2019 at 10:27):

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.

view this post on Zulip Tim Daly (Dec 20 2019 at 10:36):

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).

view this post on Zulip Tim Daly (Dec 20 2019 at 10:38):

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.

view this post on Zulip Mario Carneiro (Dec 20 2019 at 10:40):

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

view this post on Zulip Tim Daly (Dec 20 2019 at 11:05):

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.

view this post on Zulip Tim Daly (Dec 20 2019 at 11:50):

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

view this post on Zulip Mario Carneiro (Dec 20 2019 at 12:04):

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

view this post on Zulip Mario Carneiro (Dec 20 2019 at 12:05):

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

view this post on Zulip Mario Carneiro (Dec 20 2019 at 12:06):

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

view this post on Zulip Tim Daly (Dec 20 2019 at 12:09):

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.

view this post on Zulip Mario Carneiro (Dec 20 2019 at 12:15):

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

view this post on Zulip Tim Daly (Dec 20 2019 at 12:20):

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.

view this post on Zulip Tim Daly (Dec 20 2019 at 12:21):

The coercion code is essentially a Lean tactic.

view this post on Zulip Tim Daly (Dec 20 2019 at 12:23):

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

view this post on Zulip Tim Daly (Dec 20 2019 at 12:24):

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


Last updated: May 15 2021 at 02:11 UTC