[Agda] Running the TC monad

[Yorick Sijsling]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160206/f57bae69/attachment.html