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

[Chris Moline]

I forgot to mention that I would like it to be user extensible. So I'm now
thinking I should just pass in a set and check for membership.


On Sat, Aug 24, 2013 at 4:09 PM, Chris Moline <blackredtree at gmail.com>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?
>
> For example, 'actionConnectProxy :: (ActionClass self, WidgetClass proxy) =>
> self -> proxy -> IO ()'
>
> This is easily exported with
>
>
>
> postulate
>   actionConnectProxy : {A, B : Set} -> A -> B -> IO Unit
>
> {-# COMPILED actionConnectProxy Graphics.UI.Gtk.actionConnectProxy #-}
>
>
>
> But how do I restrict A to ActionClass and B to WidgetClass? I could go
>
>
> postulate WidgetClass : {A : Set} -> A -> A
>
> {-# COMPILED_TYPE WidgetClass (WidgetClass a => a) #-}
>
>
>
> But  I would like the data type to be somehow restricted to "instances" of
> the type. Any help would be appreciated.
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130824/f3262c56/attachment.html