denotations.hs

{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE UndecidableInstances  #-}

module Deno where

import Control.Applicative
import Test.QuickCheck.Checkers
import Test.QuickCheck.Classes
import Test.QuickCheck


-- machinery

instance Model b b' => Model (a -> b) (a -> b') where
  model f = model . f

models
    :: (Model b b', Arbitrary a, EqProp b', Show a)
    => (a -> b')
    -> (a -> b)
    -> TestBatch
models g f =
  ( "denotation"
  , [("semantic eq", model . f =-= g)]
  )


-- an implementation

data Bool2 = Bool2
  { runBool2 :: forall r. r -> r -> r
  }

instance Show Bool2 where
  show b2 = runBool2 b2 "false" "true"

instance Eq Bool2 where
  a == b = runBool2 a 0 1 == runBool2 b 0 1

instance Arbitrary Bool2 where
  arbitrary = oneof $ fmap pure [ Bool2 const, Bool2 $ flip const ]

not2 :: Bool2 -> Bool2
not2 b2 = Bool2 $ \f t -> runBool2 b2 t f

and2 :: Bool2 -> Bool2 -> Bool2
and2 a b = Bool2 $ \f t -> runBool2 a f (runBool2 b f t)


-- denotations

instance Model Bool2 Bool where
  model b2 = runBool2 b2 False True

deno_not2 :: Bool2 -> Bool
deno_not2 = not . model

deno_and2 :: Bool2 -> Bool2 -> Bool
deno_and2 x y = model x && model y



-- test it

main :: IO ()
main = quickBatch $ mconcat
  [ deno_not2 `models` not2
  , deno_and2 `models` and2
  ]