[Agda] Using Haskell type class constraints with Agda types

[Ulf Norell]

Hi Alexander,

In this particular case, the easiest solution is to bind to encode for the
Value type and apply toJSON on the Agda side:

postulate
  encodeValue : Value → ByteString
{-# COMPILE GHC encodeValue = encode #-}

encode : ⦃ ToJSON A ⦄ → A → ByteString
encode x = encodeValue (toJSON x)

A slightly more general approach is to define a type that packs up an
element with its toJSON function, define the ToJSON
instance for that in Haskell, and specialize encode to that type:

data WithToJSON (A : Set) : Set where
  mkWithToJSON : (A → Value) → A → WithToJSON A

{-# FOREIGN GHC
data WithToJSON a = WithToJSON (a -> Value) a
instance ToJSON (WithToJSON a) where toJSON (WithToJSON f x) = f x
#-}

{-# COMPILE GHC WithToJSON = data WithToJSON (WithToJSON) #-}

withToJSON : ⦃ ToJSON A ⦄ → A → WithToJSON A
withToJSON x = mkWithToJSON toJSON x

postulate encodeDyn : WithToJSON A → ByteString
{-# COMPILE GHC encodeDyn = \ _ -> encode #-}

encode : ⦃ ToJSON A ⦄ → A → ByteString
encode x = encodeDyn (withToJSON x)

Complete example:
https://gist.github.com/UlfNorell/bb7b807e7de013a7daca310da123c834

/ Ulf

On Mon, Oct 5, 2020 at 5:02 PM Alexander Ben Nasrallah <me at abn.sh> wrote:

> Hi there,
>
> I'm currently playing around with Agdas FFI. I know that "There is
> (currently) no way to map a Haskell type with type class constraints to
> an Agda type." The manual describes a workaround for how to pass
> postulated Haskell types to postulated functions with type class
> contraints in Agda.
>
>
> https://agda.readthedocs.io/en/v2.6.1.1/language/foreign-function-interface.html#handling-typeclass-constraints
>
> I was wondering if it is possible to modify the
> workaround, so I can pass a non-postulated Agda type to postulated
> functions with constraints.
>
> Concrete I would like to (de)serialize JSON using Aeson. Therefore I
> defined a record `ToJSON` which shall resemble the `ToJSON` type class.
> Now I would like to pass `ToJSON` instance arguments to postulated
> functions with `ToJSON` type class contraints.
>
> I unsuccessfully tried a few approaches. Here is my current work in
> progress:
>
>
> https://gitlab.com/neosimsim/verified-parsing/-/blob/aeson/src/Foreign/Haskell/Data/Aeson.agda#L34
>
> Does anyone have any ideas, how to make this work or is it just not
> possible (yet)?
>
> Kind regards
> Alex
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20201006/4f062003/attachment.html>