Skip to content

Instantly share code, notes, and snippets.

@hkailahi
Last active August 2, 2023 21:23
Show Gist options
  • Save hkailahi/ccad605dcf79daf426305e58b4d92359 to your computer and use it in GitHub Desktop.
Save hkailahi/ccad605dcf79daf426305e58b4d92359 to your computer and use it in GitHub Desktop.
Anti-Instance Doctest Example
-- 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.
-}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment