skip links for text browsers skip to main | skip to sidebar Bloggy Badger Code and ideas in computer science. And maybe a short story or two. Home About Samuel Terms and conditions google_ad_section_start(name=default) Wednesday, July 31, 2013 The Commutativity monad I have released Commutative , a monadic combinator library for writing commutative functions. This post explains the theory behind how it works. Haskell's type system is quite precise and sophisticated, yet dependently-typed languages such as Agda and Idris manage to go even further. For example, using Agda, it is trivial to define the type of commutative functions: they are simply binary functions together with a proof that the function is commutative. record Commutative (a b : Set) : Set where field f : a → a → b prf : ∀ x y → f x y ≡ f y x ...