<div dir="ltr"><div>Hi Alexander,</div><div><br></div><div>In this particular case, the easiest solution is to bind to encode for the Value type and apply toJSON on the Agda side:</div><div><br></div><div style="margin-left:40px"><span style="font-family:monospace">postulate<br>  encodeValue : Value → ByteString<br>{-# COMPILE GHC encodeValue = encode #-}<br><br>encode : ⦃ ToJSON A ⦄ → A → ByteString<br>encode x = encodeValue (toJSON x)</span></div><div><br></div><div>A slightly more general approach is to define a type that packs up an element with its toJSON function, define the ToJSON</div><div>instance for that in Haskell, and specialize encode to that type:</div><div><br></div><div style="margin-left:40px"><span style="font-family:monospace">data WithToJSON (A : Set) : Set where<br>  mkWithToJSON : (A → Value) → A → WithToJSON A<br></span></div><div style="margin-left:40px"><span style="font-family:monospace"><br></span></div><div style="margin-left:40px"><span style="font-family:monospace">{-# FOREIGN GHC<br>data WithToJSON a = WithToJSON (a -> Value) a<br>instance ToJSON (WithToJSON a) where toJSON (WithToJSON f x) = f x<br>#-}<br><br>{-# COMPILE GHC WithToJSON = data WithToJSON (WithToJSON) #-}<br><br>withToJSON : ⦃ ToJSON A ⦄ → A → WithToJSON A<br>withToJSON x = mkWithToJSON toJSON x<br><br>postulate encodeDyn : WithToJSON A → ByteString<br>{-# COMPILE GHC encodeDyn = \ _ -> encode #-}<br><br>encode : ⦃ ToJSON A ⦄ → A → ByteString<br>encode x = encodeDyn (withToJSON x)</span></div><div><br></div><div>Complete example: <a href="https://gist.github.com/UlfNorell/bb7b807e7de013a7daca310da123c834">https://gist.github.com/UlfNorell/bb7b807e7de013a7daca310da123c834</a></div><div><br></div><div>/ Ulf<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Mon, Oct 5, 2020 at 5:02 PM Alexander Ben Nasrallah <me@abn.sh> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Hi there,<br>
<br>
I'm currently playing around with Agdas FFI. I know that "There is<br>
(currently) no way to map a Haskell type with type class constraints to<br>
an Agda type." The manual describes a workaround for how to pass<br>
postulated Haskell types to postulated functions with type class<br>
contraints in Agda.<br>
<br>
<a href="https://agda.readthedocs.io/en/v2.6.1.1/language/foreign-function-interface.html#handling-typeclass-constraints" rel="noreferrer" target="_blank">https://agda.readthedocs.io/en/v2.6.1.1/language/foreign-function-interface.html#handling-typeclass-constraints</a><br>
<br>
I was wondering if it is possible to modify the<br>
workaround, so I can pass a non-postulated Agda type to postulated<br>
functions with constraints.<br>
<br>
Concrete I would like to (de)serialize JSON using Aeson. Therefore I<br>
defined a record `ToJSON` which shall resemble the `ToJSON` type class.<br>
Now I would like to pass `ToJSON` instance arguments to postulated<br>
functions with `ToJSON` type class contraints.<br>
<br>
I unsuccessfully tried a few approaches. Here is my current work in progress:<br>
<br>
<a href="https://gitlab.com/neosimsim/verified-parsing/-/blob/aeson/src/Foreign/Haskell/Data/Aeson.agda#L34" rel="noreferrer" target="_blank">https://gitlab.com/neosimsim/verified-parsing/-/blob/aeson/src/Foreign/Haskell/Data/Aeson.agda#L34</a><br>
<br>
Does anyone have any ideas, how to make this work or is it just not<br>
possible (yet)?<br>
<br>
Kind regards<br>
Alex<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>