Add denotationFor

[isovector]

This PR adds denotationFor, which allows you to state that one function is the model of another.

As an example, I can write a Boehm-Berarducci-encoded boolean, and show that its and and not functions are modeled by the standard Bool-typed versions.

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 `denotationFor` not2
  , deno_and2 `denotationFor` and2
  ]

[conal]

Thanks very much for the contribution! Released to Hackage.