Improving Haskell Types with SMT
Improving Haskell Types with SMT - Diatchki
We present a technique for integrating GHC’s type-checker with an SMT solver. The technique was developed to add support for reasoning about type-level functions on natural numbers, and so our implementation uses the theory of linear arithmetic
The social network of the future: No ads, no corporate surveillance, ethical design, and decentralization! Own your data with Mastodon!