[Agda] Typed Jigger in vanilla 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


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


-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180626/3ec7471e/attachment.sig>