Blogpost: proving monad laws by inspection testing - Haskell

Welcome to the Functional Programming Zulip Chat Archive. You can join the chat here.

Asad Saeeduddin

@Lysxia interesting, i hadn't heard of inspection-testing before. Would it be able to prove that curry . uncurry = id for example?


You can try yes, and find that the LHS is actually lazier than id, and instead a more precise RHS is \f x y -> f x y

{-# LANGUAGE TemplateHaskell #-}
module U where

import Test.Inspection

cu, id1, id2 :: (a -> b -> c) -> (a -> b -> c)
cu = curry . uncurry
id1 f = f
id2 f x y = f x y

inspect $ 'cu =/= 'id1
inspect $ 'cu ==- 'id2
Georgi Lyubenov // googleson78

this is also used in polysemy to check that machinery is optimised away, for small examples - e.g. here

:gemini: higher-order, no-boilerplate monads. Contribute to polysemy-research/polysemy development by creating an account on GitHub.
Torsten Schmits

guess that's where a multi-module test is missing?