[Agda] Does Agda compiler read haskell's type information?

Станислав Черничкин schernichkin at gmail.com
Wed Apr 17 11:29:57 CEST 2013


Hi, Agda dev team.

I'm interested in creating some tools which mind help with Agda-Haskell
interoperation. In particular I interested in a tool for generating
signatures in Agda for compiled Haskell functions and algebraic datatypes.
For this purpose I need to extract type information from Haskell somehow,
and generate Agda code. I decided to use Agda compiler itself
(Agda.Syntax.Concrete) for code generation, but I still don’t know how to
read Haskell libraries. And I wondering, probably Agda compiler is already
able to extract type information from Haskell somehow? If it does, could
you point me corresponding place in Agda compiler’s code?
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130417/de601148/attachment.html


More information about the Agda mailing list