Using dependent types to write proofs in Haskell | Ascetic Slug

I wrote a blog where I explain how one can use GHC’s type system to write mathematical proofs.

https://janmasrovira.gitlab.io/ascetic-slug/post/haskell-proofs/

2 Likes