[Agda] Suspicious normalisation

[Guillaume Brunerie]

Den sön 27 sep. 2020 kl 21:25 skrev Marko Dimjašević <marko at dimjasevic.net>:
>
> Hi Guillaume,
>
> On Fri, 2020-09-25 at 13:21 +0200, Guillaume Brunerie wrote:
> > It seems perfectly reasonable to me that it reduces.
> > The thing is that it has an unsolved implicit argument of type
> > Data.Empty.⊥, so there would be unsolvable yellow if you try to use this
> > term in a consistent context, but there is no reason why that should
> > prevent it from normalizing.
>
>
> Why is it an unsolved argument?
>
> Perhaps I could use some reading on solving (implicit) arguments, but my
> understanding is that the type becomes either Data.Empty.⊥ or Data.Unit.⊤
> and at that point it should be clear if the first explicit argument to
> function ƛ′_⇒_ is valid or not.

You seem to be confusing the value and the type of an implicit
argument. It is true that the type of the implicit argument becomes
either ⊥ or ⊤, but in order for it to be solved you need an actual
*value* (of type either ⊥ or ⊤). In the case of ⊤, Agda knows that
there is a unique (up to definitional equality) value of that type,
and therefore solves it for you. But in the case of ⊥, Agda is waiting
for a element of type ⊥ but doesn’t know which one you mean, so it is
unsolved.

You do get yellow if you write the following (which was your initial
question, except that you don’t see yellow when doing C-c C-n)

t : Term
t = ƛ′ two ⇒ two

And note that having an (implicit or not) argument of type ⊥ is not
"invalid" in any way. In an inconsistent context, you could find a
term of type ⊥ and use it for your implicit argument, for instance
(same as before but in an inconsistent context and without yellow):

u : ⊥ → Term
u abs = ƛ′_⇒_ two {abs} two

> I don't have anything highlighted in yellow due to the definition of ƛ′_⇒_.

Yes, that’s because you only use it in "valid" cases, and therefore
Agda automatically solves the implicit argument because it has type ⊤.

> The only place where it is actually used is in a definition of plus′, for
> which you'd need the full version of Term [1]:
>
> plus′ : Term
> plus′ = μ′ + ⇒ ƛ′ m ⇒ ƛ′ n ⇒
>           case′ m
>             [zero⇒ n
>             |suc m ⇒ `suc (+ · m · n) ]
>   where
>   +  =  ` "+"
>   m  =  ` "m"
>   n  =  ` "n"
>
>
> This type-checks and loads just fine.
>
>
> > Depending on your use case, maybe you can use an instance argument
> > instead of an implicit argument, this way it will fail instead of
> > reducing, but work when the first argument is a variable.
>
>
> Thank you for the suggestion! I tried using an instance argument, but the
> outcome is the same: everything type-checks just fine and there are no
> yellow highlights.

If you try to normalize  ƛ′ two ⇒ two  when using an instance argument
you will get an error, which is what I thought you were trying to get.
I’m not quite sure anymore which problem you are trying to solve.

Best,
Guillaume

> [1] Use the definition of Term as in https://plfa.github.io/Lambda/
>
>
> --
> Regards,
> Marko Dimjašević <marko at dimjasevic.net>
> https://dimjasevic.net/marko
> Mastodon: https://mamot.fr/@mdimjasevic
> PGP key ID:       056E61A6F3B6C9323049DBF9565EE9641503F0AA
> Learn email self-defense! https://emailselfdefense.fsf.org