[Agda] Typed Jigger in vanilla Agda.

[Roman]

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

[Guillaume Allais]

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

Post by Roman
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,
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
https://lists.chalmers.se/mailman/listinfo/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.

Post by Guillaume Allais
Hi Roman,
unlike [4] it also works for terms whose context & type are not
Id : ∀ {Γ σ} → Γ ⊢ σ ⇒ σ
Id = lam λ x → x
https://github.com/gallais/potpourri/blob/master/haskell/stlc/Bidirectional.hs#L294
Cheers,
--
gallais

Post by Roman
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,
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
https://lists.chalmers.se/mailman/listinfo/agda