blog post image
12 Oct

"A formal approach to distributed systems: implementing a pi-calculus interpreter in Haskell"

It has never been easier to do type-level programming in Haskell to capture precise invariants of the values as we are working with. Thanks to extensions such as DataKinds and TypeFamilies, many value-level definitions translate directly to type-level definitions. However, once we have them at the type-level, you often find that GHC's type checker complains about two "obviously" similar expressions not being equal. It may not see that x + 0 and 0 + x are the same for any natural number x.

Read More
blog post image
11 Oct

Write your own GHC type checker plugins

It has never been easier to do type-level programming in Haskell to capture precise invariants of the values as we are working with. Thanks to extensions such as DataKinds and TypeFamilies, many value-level definitions translate directly to type-level definitions. However, once we have them at the type-level, you often find that GHC's type checker complains about two "obviously" similar expressions not being equal. It may not see that x + 0 and 0 + x are the same for any natural number x.

Read More