Lean cannot prove `partial def` inhabitable.

Stream: new members

[Kitsune-Violet]

Lean is giving me the error:

failed to compile 'partial' definition 'Parser.least_until', could not prove that the type
  ...
is nonempty.

Despite me seemingly inhabiting the type myself!

/--
    Parses the least amount of the original term until the specified end.
    Will only provide the error of the expected end.
-/
partial def Parser.least_until [Monad m]
    (mx: Parser t e m a)
    (my: Parser t e' m b)
    : (Parser t e' m (List a × b))
    := my
        <&> (fun y => ([], y))
        <?> fun err => do
            let x <- mx ?> err
            let (xs, y) <- mx.least_until my
            return (x :: xs, y)

I am really unsure where I am supposed to go from here, from what I can tell the type signature is perfectly sensible for partial parser combinator code, notably Parser.most does not give this error.

The file is hosted at https://github.com/Vi-Kitten/Bloom/blob/00baa16/Bloom/Parser.lean and should work without context!

[Aaron Liu]

Kitsune-Violet said:

Despite me seemingly inhabiting the type myself!

if you mean that the body of the partial is supposed to serve as evidence for the type being inhabited, then that's a circular argument since it references itself

[Aaron Liu]

you should try writing an Inhabited instance for Parser t e m a

[Kitsune-Violet]

Aaron Liu said:

Kitsune-Violet said:

Despite me seemingly inhabiting the type myself!

if you mean that the body of the partial is supposed to serve as evidence for the type being inhabited, then that's a circular argument since it references itself

Well yes, it does reference itself, that is why I am working within the partial system so I can write general recursive functions!

[Aaron Liu]

consider this partial definition which is clearly unsound

/-
failed to compile 'partial' definition 'notgood', could not prove that the type
  Nat → Empty
is nonempty.
-/
partial def notgood (n : Nat) : Empty := notgood (n + 1)

[Aaron Liu]

would you consider the body of this definition as "evidence" that the type is inhabited

[Kitsune-Violet]

Aaron Liu said:

consider this partial definition which is clearly unsound

/-
failed to compile 'partial' definition 'notgood', could not prove that the type
  Nat → Empty
is nonempty.
-/
partial def notgood (n : Nat) : Empty := notgood (n + 1)

In a partial system I would consider it inhabited with the bottom instance.

[Aaron Liu]

but Lean is not a partial system!

[Aaron Liu]

what partial does is it makes an opaque definition, and then it overrides the implementation in the compiler

[Kitsune-Violet]

Aaron Liu said:

but Lean is not a partial system!

Is partial not a true subsystem?

[Aaron Liu]

and it needs a value to inhabit the opaque with

[Aaron Liu]

Kitsune-Violet said:

Aaron Liu said:

but Lean is not a partial system!

Is partial not a true subsystem?

the thing with partial def is that you use them in your theorems

[Aaron Liu]

so if Lean allowed me to write partial def notgood then I could use it in a theorem

[Eric Paul]

Here's some explanation in the reference that you might find helpful

[Kitsune-Violet]

Aaron Liu said:

Kitsune-Violet said:

Aaron Liu said:

but Lean is not a partial system!

Is partial not a true subsystem?

the thing with partial def is that you use them in your theorems

Is that a typo, or are they actually valid in theorems?

[Kitsune-Violet]

oh god they are!?

[Aaron Liu]

and it's a theorem that there are no functions Nat → Empty, but I've just constructed one here with the partial system

[Aaron Liu]

and that would be really bad

[Aaron Liu]

which is why it rejects this

[Kitsune-Violet]

This is quite the headache! Does lean have a partial subsystem then with fun things like y combintors and whatnot?

[Aaron Liu]

well you can do unsafe

[Aaron Liu]

which doesn't require proofs that your types are nonempty

[Aaron Liu]

but you can't use those in proofs

[Kitsune-Violet]

Aaron Liu said:

well you can do unsafe

that sounds so much dirtier then it is, if you don't mind specifying, how would you go about solving this issue, because I honestly have no clue!

[Aaron Liu]

Kitsune-Violet said:

oh god they are!?

you can use them in theorems, but you can't replace them with their definition

[Aaron Liu]

Kitsune-Violet said:

Aaron Liu said:

well you can do unsafe

that sounds so much dirtier then it is, if you don't mind specifying, how would you go about solving this issue, because I honestly have no clue!

I recommend just writing the docs#Inhabited instance

[Aaron Liu]

this is what they do in Core for monads like docs#Lean.Meta.MetaM

[Kitsune-Violet]

Just before I go to sleep, am I supposed to instance something like Inhabited inductively on a bunch of families of things like parsers and functions between parsers? Because in the general case a parser isn't inhabited, only functions between parsers are!

[Aaron Liu]

wait parsers aren't generally inhabited?

[Aaron Liu]

there's not some error value you can always return?

[Kitsune-Violet]

Aaron Liu said:

there's not some error value you can always return?

I am polymorphic over error types, and don't want to make assumptions about said types!

[Kitsune-Violet]

I have DefaultErr but thats for when its actually needed, not it situations like this where, intuitively, its sound (in a partial system) but just not garunteed to halt.

[Aaron Liu]

make an instance assuming certain types are inhabited

[Aaron Liu]

see for example docs#EStateM.instInhabited

[Kitsune-Violet]

I could only assume the erorr was inhabited or the instance, not both, both would be too restricting

[Kitsune-Violet]

I also worry that such constraints would be viral

[Aaron Liu]

then this might be a bit difficult

[Kitsune-Violet]

What confuses me most is that:

/--
    Repeaedly parses until failure.
-/
partial def Parser.most [Monad m]
    (mx: Parser t e m a)
    : (Parser t e' m (List a))
    := mx
        >>= (fun x => List.cons x <$> mx.most)
        <?> fun _ => return []

/--
    Parses the least amount of the original term until the specified end.
    Will only provide the error of the expected end.
-/
partial def Parser.least_until [Monad m]
    (mx: Parser t e m a)
    (my: Parser t e' m b)
    : (Parser t e' m (List a × b))
    := my
        <&> (fun y => ([], y))
        <?> fun err => do
            let x <- mx ?> err
            let (xs, y) <- mx.least_until my
            return (x :: xs, y)

Parser.most is fine and Parser.least_until is angry!

[Aaron Liu]

well Parser.most doesn't call itself recursively it looks like

[Aaron Liu]

no it does how did I miss that

[Kitsune-Violet]

oh it does! >>= (fun x => List.cons x <$> mx.most)

[Aaron Liu]

well I wouldn't know why unless you provide something I can run on my end

[Kitsune-Violet]

Kitsune-Violet said:

Lean is giving me the error:

failed to compile 'partial' definition 'Parser.least_until', could not prove that the type
  ...
is nonempty.

Despite me seemingly inhabiting the type myself!

/--
    Parses the least amount of the original term until the specified end.
    Will only provide the error of the expected end.
-/
partial def Parser.least_until [Monad m]
    (mx: Parser t e m a)
    (my: Parser t e' m b)
    : (Parser t e' m (List a × b))
    := my
        <&> (fun y => ([], y))
        <?> fun err => do
            let x <- mx ?> err
            let (xs, y) <- mx.least_until my
            return (x :: xs, y)

I am really unsure where I am supposed to go from here, from what I can tell the type signature is perfectly sensible for partial parser combinator code, notably Parser.most does not give this error.

The file is hosted at https://github.com/Vi-Kitten/Bloom/blob/00baa16/Bloom/Parser.lean and should work without context!

I provided the code in the post on github, the file should work with no context, just a copy paste!

[Kitsune-Violet]

My guess is that lean knows something about combinatros like >>= and <$> that it doesn't know / I haven't told it for my error recovery combinator <?>.

[Aaron Liu]

ok it sees that Parser t e' m is a monad and List a is nonempty

[Kitsune-Violet]

Alternatively, it might be that the value y in the inductive step:

            let (xs, y) <- mx.least_until my
            return (x :: xs, y)

Isn't pushed arbitrarily deep like in

        >>= (fun x => List.cons x <$> mx.most)

[Aaron Liu]

so monads applied to nonempty types are always nonempty, because of pure

[Kitsune-Violet]

I am struggling to follow in all honesty, none of this maps to something concrete I can understand in terms of leans analysis of my logic.

[Kitsune-Violet]

At least, I don't see how it maps :sweat_smile:

[Aaron Liu]

so in particular Parser t e' m (List a) is nonempty because it is a monad (Parser t e' m) applied to a nonempty type (List a) and this is all done automatically by typeclass

[Kitsune-Violet]

Aaron Liu said:

so in particular Parser t e' m (List a) is nonempty because it is a monad (Parser t e' m) applied to a nonempty type (List a) and this is all done automatically by typeclass

I was hoping the reason would be something that could help me in the genreal case :(

[Kitsune-Violet]

I have a feeling I can solve this by making an inductive ListEndingWith a b I am hoping these semantics map cleanly onto the potential issue I saw here:

Kitsune-Violet said:

Alternatively, it might be that the value y in the inductive step:

            let (xs, y) <- mx.least_until my
            return (x :: xs, y)

Isn't pushed arbitrarily deep like in

        >>= (fun x => List.cons x <$> mx.most)

Althogh I am unsure.

[Aaron Liu]

I don't think it matters to the partial compiler what the contents of your definition are

[Kitsune-Violet]

how does the type being inhabitable with some default value even matter when your not using that default value for your least fixed point?

[Kitsune-Violet]

Sorry for only asking now, it just kind occured to me that that doesn't make sense

[Aaron Liu]

if the type is not inhabitable and I have a proof that it's not inhabitable then I can combine it with the partial definition (which is an inhabitant) to get a contradiction

[Aaron Liu]

which is really bad

[Kitsune-Violet]

so all I have to do is show that you can't disprove it then? (MyType -> Empty) -> Empty

[Aaron Liu]

if you can get a (MyType -> Empty) -> Empty then you can use classical logic to prove Nonempty MyType

[Kitsune-Violet]

Aaron Liu said:

if the type is not inhabitable and I have a proof that it's not inhabitable then I can combine it with the partial definition (which is an inhabitant) to get a contradiction

Does this mean that partial is essentially saying:
Those code runs and you can't tell me it isn't valid.

[Aaron Liu]

see docs#Nonempty for a description for how it's different from Inhabited (but partial can use either Nonempty or Inhabited)

[Kitsune-Violet]

all of this is well and good but how do I handle the fact that I am only going to be able to instantiate this for functions of parsers and not parsers themselves?

[Kitsune-Violet]

After learning more about this I can say that this is rather cool, although a bit unintuitive at first, its nice to know that the functions get to be consistent.

[Aaron Liu]

Kitsune-Violet said:

Aaron Liu said:

if the type is not inhabitable and I have a proof that it's not inhabitable then I can combine it with the partial definition (which is an inhabitant) to get a contradiction

Does this mean that partial is essentially saying:
Those code runs and you can't tell me it isn't valid.

iirc what partial does is, it adds an opaque constant to the environment (containing a dummy inhabitant), and it adds an unsafe constant to the environment (containing the actual implementation), and it tells the compiler "this constant is implemented_by that constant" and this lets the compiler use the actual implementation instead of the dummy value when running your code

[Aaron Liu]

The opaque constant is what gets the name of the partial def

[Kitsune-Violet]

As a side note, I have recently been torn up about if I should weaken strong normalisation or not in my language and this knowledge came along right in time, thank you!

[Kitsune-Violet]

Thank you for all the help!

[Robert Maxton]

Oh hey, fancy seeing you here.

To my understanding, partial def is really just a shortcut to let you say "trust me this thing has the properties I claim it does, now let me write proofs about it assuming I'm right"; it's at most half a step above unsafe. If you really want to reason strictly about partial functions, you probably want to be using either docs#Part and docs$PFun, or partial_fixpoint

[Aaron Liu]

actually, since you have to prove your type is inhabited, partial is actually completely safe

[Robert Maxton]

It's safe, but it's also completely opaque and only interacts with the rest of Lean in a minimal way, through its type signature; the only proofs you can do with a partial def are proofs that only use its type

[Robert Maxton]

I suppose that makes it a bit more then half a step above unsafe, but

[Kitsune-Violet]

Robert Maxton said:

Oh hey, fancy seeing you here.

To my understanding, partial def is really just a shortcut to let you say "trust me this thing has the properties I claim it does, now let me write proofs about it assuming I'm right"; it's at most half a step above unsafe. If you really want to reason strictly about partial functions, you probably want to be using either docs#Part and docs$PFun, or partial_fixpoint

My intention is to use lean as a FP lang with the added upside that I can prove things about my programs later, but the keyword there is later, I was hoping that leans own ability to detect strong normalisation or partial signatures would be a bit stronger so I wouldn't have to resort to unsafe this quickly but that seems like what I have to do to maintain velocity (accounting for the time it would take me to learn)

I think partial will probably be where I leave a lot of things eventually because lean doesn't seem to be set up for tracking monad state for recursion (I am not even sure how much research tehre is on this), with that being said thank you for the advice adn I will see if I can apply that after I have an MVP working!

[Kitsune-Violet]

If anyone has any research into a generalisation of monads using some dependent parameters that can help to prove things like halting I would be very interested as I think this is relevent to doing this erganomically!