[Agda] Typed Jigger in vanilla Agda.

[Roman]

Guillaume, that's a good point. I tend to define

    _◅▻_ : Con -> Con -> Con
    Γ ◅▻  ε       = Γ
    Γ ◅▻ (Δ ▻ σ) = Γ ◅▻ Δ ▻ σ

    wkᵛ : ∀ {Δ Γ σ} -> σ ∈ Γ -> σ ∈ Δ ◅▻ Γ
    wkᵛ  vz    = vz
    wkᵛ (vs v) = vs (wkᵛ v)

    wk : ∀ {Δ Γ σ} -> Γ ⊢ σ -> Δ ◅▻ Γ ⊢ σ
    wk (var v) = var (wkᵛ v)
    wk (ƛ b  ) = ƛ (wk b)
    wk (f · x) = wk f · wk x

    wk⁽⁾ : ∀ {Γ σ} -> ε ⊢ σ -> Γ ⊢ σ
    wk⁽⁾ = wk

and then use it like

    I⁺ : ∀ {Γ} -> Γ ⊢ ⋆ ⇒ ⋆
    I⁺ = wk⁽⁾ $ lam λ x -> x

(I guess the definitions of `_◅▻_` and `_ ▻▻_` should be swapped)

For my use cases it was enough and I'm fine with a bit of boilerplate
if it saves me from relying on instance resolution.

2018-06-26 22:58 GMT+03:00, Guillaume Allais <gallais at cs.ru.nl>:
> Hi Roman,
>
> That's a nice trick! I wouldn't quite throw [3] away yet though:
> unlike [4] it also works for terms whose context & type are not
> concrete! Case in point:
>
> Id : ∀ {Γ σ} → Γ ⊢ σ ⇒ σ
> Id = lam λ x → x
>
> Something similar in Haskell:
> https://github.com/gallais/potpourri/blob/master/haskell/stlc/Bidirectional.hs#L294
>
> Cheers,
> --
> gallais
>
>
> On 26/06/18 18:58, Roman wrote:
>> Hi guys. A while ago Conor McBride presented "A little hack to make de
>> Bruijn syntax more readable": [1]
>>
>> To save a click, it allows to use host language binders like in HOAS,
>> but get first-order terms:
>>
>>     data Tm (n : Nat) : Set where
>>       V : Fin n -> Tm n
>>       _$_ : Tm n -> Tm n -> Tm n
>>       L : Tm (suc n) -> Tm n
>>
>>     l : {m : Nat} -> (({n : Nat} -> Tm (suc (m + n))) -> Tm (suc m)) -> Tm
>> m
>>     l {m} f = L (f \{n} -> V (var m {n}))
>>
>>     myTest : Tm zero
>>     myTest = l \ f -> l \ x -> f $ (f $ x)
>>
>> But those terms are well-scoped and not well-typed. Conor found a way
>> to do the same in a well-typed setting and described it in his
>> DataData lecture notes [2]. But this new trick relies on the instance
>> resolution algorithm and became broken at some point if I recall
>> correctly. Then it was fixed, but instance resolution is still a
>> rather heavy tool to use. And using instance arguments one can write a
>> simpler thing: [3] (was broken previously as well)
>>
>> However since Agda is so amazing, we can write a typed Jigger
>> machinery without relying on instance arguments: [4]
>>
>> [1] https://personal.cis.strath.ac.uk/conor.mcbride/fooling/Jigger.agda
>> [2] https://github.com/pigworker/SSGEP-DataData
>> [3]
>> https://github.com/effectfully/random-stuff/blob/master/TypedJigger.agda
>> [4]
>> https://github.com/effectfully/random-stuff/blob/master/VanillaTypedJigger.agda
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>
>
>