[Agda] How do I handle haskell type contexts from agda when using the ffi?

Nils Anders Danielsson nad at cse.gu.se
Tue Aug 27 13:25:25 CEST 2013

On 2013-08-25 00:09, Chris Moline wrote:
> Hi, I'm making a binding to gtk to help me gain some familiarity with
> the language but I don't know how to reflect type constraints within
> agda. How can I make "instances" of a type?

The Haskell FFI doesn't have any special support for classes and
instances. I suggest that you add record types ActionClassR and
WidgetClassR on the Haskell side, along with a function

   actionConnectProxyR :: ActionClassR self -> WidgetClassR proxy ->
                          self -> proxy -> IO ()

that calls actionConnectProxy.


More information about the Agda mailing list