Skip to content

Instantly share code, notes, and snippets.

@UlfNorell
Last active October 6, 2020 09:08
Show Gist options
  • Save UlfNorell/bb7b807e7de013a7daca310da123c834 to your computer and use it in GitHub Desktop.
Save UlfNorell/bb7b807e7de013a7daca310da123c834 to your computer and use it in GitHub Desktop.
Working with type class functions in the Agda's Haskell FFI
open import Agda.Builtin.Nat
open import Agda.Builtin.List
open import Agda.Builtin.String
open import Agda.Builtin.IO
open import Agda.Builtin.Unit
{-# FOREIGN GHC
import Data.Text
import qualified Data.Text.IO as Text
data Value = Number Integer | String Text
deriving (Show)
class ToJSON a where
toJSON :: a -> Value
data WithToJSON a = WithToJSON (a -> Value) a
instance ToJSON (WithToJSON a) where
toJSON (WithToJSON f x) = f x
instance ToJSON Value where
toJSON = id
encode :: ToJSON a => a -> Text
encode = pack . show . toJSON
#-}
data Value : Set where
number : Nat → Value
string : String → Value
{-# COMPILE GHC Value = data Value (Number | String) #-}
variable
A : Set
data WithToJSON (A : Set) : Set where
mkWithToJSON : (A → Value) → A → WithToJSON A
{-# COMPILE GHC WithToJSON = data WithToJSON (WithToJSON) #-}
record ToJSON (A : Set) : Set where
field
toJSON : A → Value
open ToJSON ⦃ ... ⦄
withToJSON : ⦃ ToJSON A ⦄ → A → WithToJSON A
withToJSON x = mkWithToJSON toJSON x
postulate
encodeDyn : WithToJSON A → String
{-# COMPILE GHC encodeDyn = \ _ -> encode #-}
encode : ⦃ ToJSON A ⦄ → A → String
encode x = encodeDyn (withToJSON x)
instance
toJSONNat : ToJSON Nat
toJSONNat .toJSON = number
postulate
putStrLn : String → IO ⊤
{-# COMPILE GHC putStrLn = Text.putStrLn #-}
main : IO ⊤
main = putStrLn (encode 17)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment