Last active
August 2, 2023 21:23
-
-
Save hkailahi/ccad605dcf79daf426305e58b4d92359 to your computer and use it in GitHub Desktop.
Anti-Instance Doctest Example
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- 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