[Agda] Running the TC monad

[Yorick Sijsling]

Thanks Ulf. Maybe complicated is not entirely the right word.

If i use unify to return a value it is always being unquoted, so in order
to do that i have to quote it first. That's the step that seemed odd to me.
I already have the exact thing i need but it always has to be quoted and
unquoted to escape TC. It feels a bit like i am working against the system.
I don't know how this is implemented, but wouldn't this become slow if i
want to return big things?

An emacs mode command to run TC computations would spare me some repetitive
typing, though i think i can already use the evaluate command on something
like 'unquote (runTC (countConstructors (quote Foo)))' to get the same
result.

I do agree that this is not a huge issue. It took me a while to find the
right method but once i had it it is obvious enough.

Yorick


On Mon, Feb 8, 2016 at 9:09 AM, Ulf Norell <ulf.norell at gmail.com> wrote:

> 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/3d2061b7/attachment.html