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

Wolfgang Jeltsch g9ks157k at acme.softbase.org
Sun Apr 28 15:00:43 CEST 2013


Am Mittwoch, den 17.04.2013, 13:29 +0400 schrieb Станислав Черничкин:
> 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 think you can use GHC as a library for this purpose:

    <http://www.haskell.org/haskellwiki/GHC/As_a_library>

Best wishes,
Wolfgang





More information about the Agda mailing list