Anti-Instance Doctest Example

UnsafeFirst.hs

-- Uses `Unsatisfiable` for anti-instance, doctest for statically-checked counterexample, and quickcheck-classes-base for testing of laws
-- See https://www.heneli.dev/blog/anti-instances for more context

{-# LANGUAGE GHC2021, DataKinds #-}

module UnsafeFirst where

import Data.Semigroup (First (..))
import GHC.TypeError (ErrorMessage (Text), Unsatisfiable)
import Test.QuickCheck
import Test.QuickCheck.Classes.Internal

---------------------------------------------------------------------------------------------------
-- `First` `Monoid` Anti-Instance with proof of left-identity violation --
---------------------------------------------------------------------------------------------------

-- |>>> lawsCheck firstMonoidLaws
-- First Monoid: Associative +++ OK, passed 100 tests.
-- First Monoid: Left Identity *** Failed! Falsified (after 1 test):
--   Description: (monoidDictAppend firstMonoidDict) (monoidDictEmpty firstMonoidDict) a = a
--   a = First {getFirst = 0}
--   (monoidDictAppend firstMonoidDict) (monoidDictEmpty firstMonoidDict) a = First {getFirst = 999}
-- First Monoid: Right Identity +++ OK, passed 100 tests.
-- First Monoid: Concatenation +++ OK, passed 100 tests.
instance
  (Unsatisfiable (Text "First lacks an identity element")) =>
  Monoid (First a)

-- For `quickcheck-classes` testing of monoid laws
instance (Arbitrary a) => Arbitrary (First a) where
  arbitrary = First <$> arbitrary
  shrink = shrinkNothing

---------------------------------------------------------------------------------------------------
-- Explicit Dictionaries --
---------------------------------------------------------------------------------------------------

data MonoidDict a = MonoidDict
  { monoidDictAppend :: a -> a -> a, -- Associative
    monoidDictEmpty :: a -- Identity element
  }

firstMonoidDict :: MonoidDict (First Int)
firstMonoidDict =
  MonoidDict
    { monoidDictAppend = (<>),
      monoidDictEmpty = First 999 -- garbage value
      -- ^NOTE: Specifying our own false identity makes this a very weak test. 
      -- It would be MUCH BETTER to use PBT to generate for possible empty values to ensure none exist.
    }

---------------------------------------------------------------------------------------------------
-- Explicit Dictionary Laws --
---------------------------------------------------------------------------------------------------

-- Note: Modified `monoidLaws` from `quickcheck-classes` with inlined concrete dictionary methods.
-- There are definitely better ways to do all this

firstAssociative :: Property
firstAssociative =
  myForAllShrink @(First Int, First Int, First Int)
    True
    (const True)
    (\(a, b, c) -> ["a = " ++ show a, "b = " ++ show b, "c = " ++ show c])
    "(monoidDictAppend firstMonoidDict) a ((monoidDictAppend firstMonoidDict) b c)"
    (\(a, b, c) -> (monoidDictAppend firstMonoidDict) a ((monoidDictAppend firstMonoidDict) b c))
    "(monoidDictAppend firstMonoidDict) ((monoidDictAppend firstMonoidDict) a b) c"
    (\(a, b, c) -> (monoidDictAppend firstMonoidDict) ((monoidDictAppend firstMonoidDict) a b) c)

firstLeftIdentity :: Property
firstLeftIdentity =
  myForAllShrink @(First Int)
    False
    (const True)
    (\(a :: a) -> ["a = " ++ show a])
    "(monoidDictAppend firstMonoidDict) (monoidDictEmpty firstMonoidDict) a"
    (\a -> (monoidDictAppend firstMonoidDict) (monoidDictEmpty firstMonoidDict) a)
    "a"
    (\a -> a)

firstRightIdentity :: Property
firstRightIdentity =
  myForAllShrink @(First Int)
    False
    (const True)
    (\(a :: a) -> ["a = " ++ show a])
    "(monoidDictAppend firstMonoidDict) a (monoidDictEmpty firstMonoidDict)"
    (\a -> (monoidDictAppend firstMonoidDict) a (monoidDictEmpty firstMonoidDict))
    "a"
    (\a -> a)

firstConcatenation :: Property
firstConcatenation =
  myForAllShrink @(SmallList (First Int))
    True
    (const True)
    (\(SmallList (as :: [a])) -> ["as = " ++ show as])
    "mconcat as"
    (\(SmallList as) -> foldr (monoidDictAppend firstMonoidDict) (monoidDictEmpty firstMonoidDict) as)
    "foldr (monoidDictAppend firstMonoidDict) (monoidDictEmpty firstMonoidDict) as"
    (\(SmallList as) -> foldr (monoidDictAppend firstMonoidDict) (monoidDictEmpty firstMonoidDict) as)

firstMonoidLaws :: Laws
firstMonoidLaws =
  Laws
    "First Monoid"
    [ ("Associative", firstAssociative),
      ("Left Identity", firstLeftIdentity),
      ("Right Identity", firstRightIdentity),
      ("Concatenation", firstConcatenation)
    ]

{-
λ> lawsCheck firstMonoidLaws
First Monoid: Associative +++ OK, passed 100 tests.
First Monoid: Left Identity *** Failed! Falsified (after 1 test):
  Description: (monoidDictAppend firstMonoidDict) (monoidDictEmpty firstMonoidDict) a = a
  a = First {getFirst = 0}
  (monoidDictAppend firstMonoidDict) (monoidDictEmpty firstMonoidDict) a = First {getFirst = 999}
First Monoid: Right Identity +++ OK, passed 100 tests.
First Monoid: Concatenation +++ OK, passed 100 tests.
-}