[Agda] Running the TC monad

[Ulf Norell]

I'm not sure I understand why you think your runTC is a complicated
solution (it's certainly not an abuse of the unify function). Adding a
built-in runTC and special handling for macros would surely be more
complicated.

Something that's on my list of things to do is an Emacs mode command to run
TC computations. This would make it a lot easier to debug tactics. Would
that address your problems?

/ Ulf

On Sat, Feb 6, 2016 at 5:26 PM, Yorick Sijsling <yoricksijsling at gmail.com>
wrote:

> Hi everyone,
>
> I'm experimenting with the new reflection stuff in 2.5.1. These changes
> are quite exciting!
>
> I noticed that all the unquoting operations
> (unquote/unquoteDecl/unquoteDef) take a TC ⊤, making it hard to return
> results of a computation in this monad. Let's say we want to count the
> number of constructors of a datatype:
>
> ---
> open import Prelude
> open import Builtin.Reflection
>
> data Foo : Set where
>   foo1 : Foo
>   foo2 : Foo
>
> countConstructors : Name → TC Nat
> countConstructors dt = length <$> getConstructors dt
> ---
>
> Now i believe in an ideal situation one would have a way to run this
> computation and return the result:
>
> ---
> -- test-countConstructors : runquote (countConstructors (quote Foo)) ≡ 2
> -- test-countConstructors = refl
> ---
>
> As it turns out, it is possible to abuse the unify function to return
> arbitrary results by quoting them to a Term first. So we can define a
> function which takes a TC A and gives us a tactic which puts the value in
> the hole:
>
> ---
> runTC : ∀ {a} {A : Set a} → TC A → Tactic
> runTC c hole =
>   do v ← c
>   =| `v ← quoteTC v
>   =| unify hole `v
>
> test-countConstructors : unquote (runTC (countConstructors (quote Foo))) ≡
> 2
> test-countConstructors = refl
> ---
>
> This is usable, but the notation is awkward. I used the new macro
> functionality to clean it up:
>
> ---
> macro
>   countConstructors′ : Name → Tactic
>   countConstructors′ dt = runTC (countConstructors dt)
>
> test-countConstructors′ : countConstructors′ Foo ≡ 2
> test-countConstructors′ = refl
> ---
>
> All of this took quite a while for me to figure out, so i thought it was
> worth sharing. But i also think this is a complicated solution to something
> which should be quite simple. Is this the right way to do it or am i
> missing something here?
>
> Would it maybe make sense to have runTC as a built-in, and extend the
> macro's to allow result types of something else than TC ⊤ in which case
> runTC is used? I imagine something like this would be possible:
>
> ---
> -- macro
> --   countConstructors : Name → TC Nat
> --   countConstructors dt = length <$> getConstructors dt
>
> -- test-countConstructors : countConstructors Foo ≡ 2
> -- test-countConstructors = refl
> ---
>
> I would like to hear your opinions on this,
>
> Yorick
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160208/a81cdecc/attachment.html