[Agda] Agda as an embedded language

[Ertugrul Söylemez]

Hello there,

yesterday I was experimenting with using Agda as an embedded language in
a Haskell project -- sort of like a scripting language.  Motivated by
the fact that Agda is great at expressing EDSLs the idea was that you
could load an Agda module, type- and terminate-check it and finally
evaluate some top level definitions.  You could then use the result in
your Haskell program.  This is of course about application programming,
not proofs, so type-checking alone won't be enough.

Unfortunately this wasn't as easy as I had hoped.  The Agda API is very
complicated and seems to be very specific to agda-mode and the agda
command line executable.

Are there any plans to make the library more accessible or provide a
wrapper library?  Something like Haskell's 'hint' library would be
great.  Or perhaps there is already an easy way to embed Agda and I
didn't see it?  Are there any other Agda users who would be interested
in such a feature?


Greets,
Ertugrul

-- 
nightmare = unsafePerformIO (getWrongWife >>= sex)
http://ertes.de/
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 836 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20111223/ed9eef75/signature-0001.bin