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 #-}moduleUwhereimportTest.Inspectioncu,id1,id2::(a->b->c)->(a->b->c)cu=curry.uncurryid1f=fid2fxy=fxyinspect$'cu=/='id1inspect$'cu==-'id2
Definitional lawfulness: proof by inspection testing
https://blog.poisson.chat/posts/2020-08-08-definitional-lawfulness.html
@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
wow, awesome
this is also used in polysemy to check that machinery is optimised away, for small examples - e.g. here
guess that's where a multi-module test is missing?