[Agda] Help with stuck unification/intrinsic typing in general

[guillaume allais]

Hi all,

This is indeed the right move. An additional trick one can play is to
use an *inductive* 4-place relation `Θ ≡ q ** Γ₂ ++ Γ₁` instead of a mere
equality proof. With this extra structure, you will be able to perform
induction directly on the proof rather than having to do case analysis
on `Θ` and `Γ₂` and use the proof of equality to dismiss the impossible
cases. This should make the whole experience more pleasant.

Best,
gallais


On 01/10/2020 09:44, Neel Krishnaswami wrote:
>
> Dear Daniel.
>
> In general, intrinsically typed representations are definitely the way 
> to go when your object language does not have a conversion relation.
>
> If your language does have a conversion or judgemental equality 
> relation, then intrinsic representations are enormously harder to work 
> with. The basic issue is that the datatype representing typing will 
> have proof trees corresponding to derivations of judgemental equality, 
> and quotienting by the derivation of convertibility is giant PITA. 
> (This is still active research, and I'm not actually up to date on 
> where the state of the art here is -- probably Thorsten knows.)
>
> In your particular case, however, it looks like you have a different 
> problem. The _._ constructor in your screen shot has the type:
>
>     _·_ : ∀{Δ} {Γ₁ Γ₂ : Context Δ} {A B q}
>         → Γ₁ ⊢ A -⟨ q ⟩→ B
>         → Γ₂ ⊢ A
>         → (q ** Γ₂ ++ Γ₁) ⊢ B
>
> Here, the return type of the function has an index which has function 
> calls in it:
>
>         ... → (*q ** Γ₂ ++ Γ₁*) ⊢ B
>
> The Agda type inference algorithm uses unification, and unification 
> problems involving calls to arbitrary functions are, in general, 
> hopeless. *Unification and pattern match coverage will generally only 
> work reliably if the return type's indices contain expressions made 
> only from variables and data constructors. *
>
> If memory serves, Conor McBride calls indices containing function 
> calls "green slime", and warns people never to touch it. The way to 
> keep from being contaminated by green slime is to use an explicit 
> equality -- if you change your datatype declaration to the following:
>
>     _·_ : ∀{Δ} {Γ₁ Γ₂ Θ : Context Δ} {A B q}
>         → Γ₁ ⊢ A -⟨ q ⟩→ B
>         → Γ₂ ⊢ A
>         → Θ ≡ q ** Γ₂ ++ Γ₁
>         → Θ ⊢ B
>
> The case splitter will see the variable Θ and happily introduce a case 
> for the _·_ constructor. But in the case branch, you will possess the 
> equality Θ ≡ q ** Γ₂ ++ Γ₁ which you can use to do any necessary 
> reasoning yourself, thereby sparing the match coverage algorithm from 
> having to do arbitrary mathematical reasoning.
>
> Best,
> Neel
>
> On 01/10/2020 04:48, Daniel Lee wrote:
>> Hi all,
>>
>> I'm super new to Agda and the Agda community. Hopefully this is the right
>> place to ask something like this, but please call me out if it isn't.
>>
>>
>> I'm working on an Agda development for a QTT formalization. I'm trying to
>> use an intrinsically typed representation for terms, but run into
>> unification issues when trying to define substitution.
>>
>> Substitution:
>> [image: Screen Shot 2020-09-30 at 8.34.38 PM.png]
>>
>> Error message:
>> [image: Screen Shot 2020-09-30 at 8.34.50 PM.png]
>>
>> Application def:
>> [image: Screen Shot 2020-09-30 at 8.35.05 PM.png]
>>
>> I'm sort of at a loss for how to get around this. Is the issue because of
>> the functions in the return type?
>>
>> More broadly, it seems like intrinsic typing is the Agda way of doing
>> things, and gives a lot for free. And it works really well in the STLC
>> example given in the PLFA textbook. But for a more complicated type system
>> like this, I'm starting to think it might be easier to use extrinsic
>> typing? I've also had to rely on the REWRITE pragma which I just learned
>> isn't allowed in --safe due to potential non-convergence.
>> Does someone maybe have experience with this and could speak to pros/cons
>> of using intrinsic vs extrinsic typing here?
>>
>> Thanks,
>> Daniel
>>
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
> -- 
> Neel Krishnaswami
> nk480 at cl.cam.ac.uk
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Flists.chalmers.se%2Fmailman%2Flistinfo%2Fagda&data=02%7C01%7Cguillaume.allais%40strath.ac.uk%7Cec25fc40f26f43e1903108d865e62ade%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637371386947907230&sdata=%2FZY4zKWoYjDwh0yDY%2BO0S76IWk9WC5caow98WgTuBxw%3D&reserved=0

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20201001/f7a3b082/attachment.html>