Zulip Chat Archive

Stream: general

Topic: lean internals


view this post on Zulip VinothKumar Raman (Mar 13 2018 at 15:31):

Is there any good reference to learn how to elaborate implicit arguments to a coc like core? Like how lean does? I am trying to build a coc like language
http://godel.yellowflash.in/
I want to introduce implicit arguments, I have some idea in my head but I couldn't put it down clearly, Its mostly based on resolution in simple basic types. But I have a feeling that it won't work

view this post on Zulip VinothKumar Raman (Mar 13 2018 at 15:32):

The idea is more like completely apply the explicit arguments and run unification of simple basic types to infer the missing arguments.

view this post on Zulip Andrew Ashworth (Mar 13 2018 at 16:16):

is godel your effort?

view this post on Zulip Gabriel Ebner (Mar 13 2018 at 16:36):

The idea is more like completely apply the explicit arguments and run unification of simple basic types to infer the missing arguments.

This is almost exactly how Lean's elaborator works. Essentially you keep around a unification state ("metavar_context", basically a partial assignment of metavariables to expressions). Now you go recursively through the pre-expression (abstract syntax tree, without implicit arguments) and convert it to an expression. For every application you fill in the implicit arguments as metavariables, and solve the appropriate unfication constraints so that the application type-checks. At the end, hopefully all metavariables are filled in and you can instantiate all metavariables in the produced expression.

view this post on Zulip Gabriel Ebner (Mar 13 2018 at 16:37):

Except that unification of simple basic types is more like first-order unification + several pages of heuristics.

view this post on Zulip VinothKumar Raman (Mar 14 2018 at 08:39):

is godel your effort?

Yea it is my effort. I read a bit about COC and built it

view this post on Zulip VinothKumar Raman (Mar 14 2018 at 08:43):

I was reading a bit about the unification on COC. Some claim it might be undecidable. But it seem really possible to have implicit arguments and really decide on it right? I don't understand how it could be undecidable.

view this post on Zulip Mario Carneiro (Mar 14 2018 at 08:44):

Higher order unification is undecidable

view this post on Zulip VinothKumar Raman (Mar 14 2018 at 08:44):

What kind of heuristics does lean use? Is it in general not decidable? Is there any reference to read about tha?

view this post on Zulip Mario Carneiro (Mar 14 2018 at 08:45):

Lean doesn't do full higher order unification, it uses a few simpler strategies and mostly sticks to first order unification

view this post on Zulip VinothKumar Raman (Mar 14 2018 at 08:54):

So lean's type checking is guaranteed to terminate? I have a noob question, does making the type checking semi-decidable, affects the soundness in any way?

view this post on Zulip Mario Carneiro (Mar 14 2018 at 09:00):

Lean's typechecker is guaranteed to halt, but is not complete - some definitional equalities will not be discovered by the typechecker, and it is impossible for it to do so without becoming undecidable.

view this post on Zulip Mario Carneiro (Mar 14 2018 at 09:01):

The guarantee is of soundness only - if lean verifies a type derivation, then it is correct, but it may error on a correct type derivation

view this post on Zulip VinothKumar Raman (Mar 14 2018 at 09:02):

So its also possible to take the alternate route to have soundness intact by doing a higher order unification, which might not halt but if it did its correct type derivation.

view this post on Zulip VinothKumar Raman (Mar 14 2018 at 09:03):

Thanks, I would read about higher order unification, Is Huet algorithm the only one?

view this post on Zulip Mario Carneiro (Mar 14 2018 at 09:05):

Note that unification is irrelevant to type checking; there is no unifier in the kernel

view this post on Zulip Mario Carneiro (Mar 14 2018 at 09:06):

it is definitional equality itself that is undecidable, due to some complications with subsingleton elimination and proof irrelevance

view this post on Zulip VinothKumar Raman (Mar 14 2018 at 09:07):

If the core language doesnt have the notion of implicit how do you know that certain arguments are marked implicit?

view this post on Zulip Mario Carneiro (Mar 14 2018 at 09:08):

The actual type of expressions expr has an annotation field on lambda and pi that marks implicitness, but the kernel ignores it

view this post on Zulip Mario Carneiro (Mar 14 2018 at 09:09):

unification and implicit parameters are all the domain of the elaborator, which is a giant untrusted piece of code

view this post on Zulip VinothKumar Raman (Mar 14 2018 at 09:09):

Ah it makes sense. I have one more trivial question which I faced
How do you rewrite definition x = y where x is not annotated with type to some (\x:A,Z)y?

view this post on Zulip Mario Carneiro (Mar 14 2018 at 09:10):

I don't quite follow your notation

view this post on Zulip Mario Carneiro (Mar 14 2018 at 09:11):

are you asking how to infer the type of an expression y?

view this post on Zulip VinothKumar Raman (Mar 14 2018 at 09:11):

so any let x = y in z can be rewritten to (\lambda x, z) y so definition is very similar to let right?

view this post on Zulip Mario Carneiro (Mar 14 2018 at 09:12):

a definition doesn't have a scope

view this post on Zulip Mario Carneiro (Mar 14 2018 at 09:12):

also let is not the same as a lambda application

view this post on Zulip VinothKumar Raman (Mar 14 2018 at 09:12):

But how do you rewrite your definitions to core calculus with just lambda abstraction, when you dont have type annotation

view this post on Zulip Mario Carneiro (Mar 14 2018 at 09:12):

there is a type annotation

view this post on Zulip Mario Carneiro (Mar 14 2018 at 09:13):

the syntax is let x : t := p in e

view this post on Zulip VinothKumar Raman (Mar 14 2018 at 09:13):

definition x = y is allowed right? Not just definition x: z = y right?

view this post on Zulip VinothKumar Raman (Mar 14 2018 at 09:13):

That type annotation is not optional?

view this post on Zulip Mario Carneiro (Mar 14 2018 at 09:13):

no, it's only def x : t := e. If you leave out the t it is inferred and filled in

view this post on Zulip VinothKumar Raman (Mar 14 2018 at 09:14):

So elaborator runs type checking before it turns to core calculus?

view this post on Zulip Mario Carneiro (Mar 14 2018 at 09:14):

Many type annotations are "optional" in the sense that you don't have to write them, but they are inserted by the elaborator

view this post on Zulip VinothKumar Raman (Mar 14 2018 at 09:15):

I was thinking elaborator writes out a new lambda term in the core calculus and type checking is completely different step.

view this post on Zulip Mario Carneiro (Mar 14 2018 at 09:15):

the parser produces a pexpr, this is a representation that roughly follows the AST of the user's input, all missing type information is absent, and the elaborator inserts metavariables in the holes, performs unification, and results an expr that has all type information filled in

view this post on Zulip Mario Carneiro (Mar 14 2018 at 09:16):

After this is done, the expr is sent to the kernel where it is typechecked (again, since the elaborator also has a typechecker that does other stuff on the side)

view this post on Zulip VinothKumar Raman (Mar 14 2018 at 09:17):

Its not very linear as I imagined it to be.

view this post on Zulip VinothKumar Raman (Mar 14 2018 at 09:17):

I think I understand the complexity very well now after trying to implement one :)

view this post on Zulip Mario Carneiro (Mar 14 2018 at 09:18):

Writing an elaborator is no joke

view this post on Zulip VinothKumar Raman (Mar 14 2018 at 09:18):

There is no concrete theory to it? Like lambda calculus substitution.

view this post on Zulip Mario Carneiro (Mar 14 2018 at 09:19):

That's what the kernel does

view this post on Zulip VinothKumar Raman (Mar 14 2018 at 09:19):

Its very messy in lot of ways.

view this post on Zulip VinothKumar Raman (Mar 14 2018 at 09:19):

I mean the elaborator doesnt have concrete theory?

view this post on Zulip Mario Carneiro (Mar 14 2018 at 09:20):

Parts of it do, I'm sure

view this post on Zulip Mario Carneiro (Mar 14 2018 at 09:20):

like the first order unification algorithm is pretty well understood at this point

view this post on Zulip VinothKumar Raman (Mar 14 2018 at 09:21):

Yea, I tried implementing first order unification on simple basic types with let polymorphism once
https://github.com/yellowflash/hindley

view this post on Zulip Mario Carneiro (Mar 14 2018 at 09:21):

Most of the complication has to do with when to unfold definitions, I think

view this post on Zulip VinothKumar Raman (Mar 14 2018 at 09:21):

Its was super clear

view this post on Zulip VinothKumar Raman (Mar 14 2018 at 09:22):

But definitions are normalizing right? Which mean you could find normal form and unify them

view this post on Zulip Mario Carneiro (Mar 14 2018 at 09:22):

lol sure if you want to wait until the end of the universe

view this post on Zulip VinothKumar Raman (Mar 14 2018 at 09:22):

Ah wait, I understand. It could go both directions on beta reduction

view this post on Zulip Mario Carneiro (Mar 14 2018 at 09:22):

DTT "terminates", but it's not remotely practical

view this post on Zulip Mario Carneiro (Mar 14 2018 at 09:23):

so there are lots of heuristics for when to unfold something

view this post on Zulip VinothKumar Raman (Mar 14 2018 at 09:26):

Oh ok


Last updated: May 13 2021 at 17:42 UTC