[Agda] reflection via FFI?

[Philipp Hausmann]

Just thinking out loud, but if there were a way to generate top-level 
definitions and datatypes from TC and if IO were possible in TC, one 
could implement Type Providers [1] that way. E.g. generate 
types+functions from a REST API definition at compile time. If its a 
good idea is another question....

Philipp

[1] 
https://docs.microsoft.com/en-us/dotnet/articles/fsharp/tutorials/type-providers/

On 10/14/2016 01:22 PM, Ulf Norell wrote:
> What's your use case? Agda IO is implemented using the FFI so calling 
> arbitrary IO functions from TC is not possible. Internally TC runs on 
> top of IO though, so if you have a particular IO function in mind it 
> could conceivably be added as a primitive.
>
> / Ulf
>
> On Fri, Oct 14, 2016 at 9:54 AM, Roman <effectfully at gmail.com 
> <mailto:effectfully at gmail.com>> wrote:
>
>     Sorry for the off-topic, but is it possible to run a TC computation
>     inside the IO monad? Would be nice to type check terms that come from
>     IO in IO.
>
>
>
>
> _______________________________________________
> 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/20161014/979a2d3a/attachment.html