This package encodes a version of intuitionistic linear logic on top of linear Haskell, using a variation of the technique described by Michael Shulman in Linear Logic for Constructive Mathematics. Embedding a larger linear logic into the simple linear logic available to us in Linear Haskell means we are able to recover the full suite of linear unitors, not just two of them, meaning we model linear logic, rather than affine logic.

The central idea is to track for each type not just its type of proofs, but also its type of refutations.

Contributions and bug reports are welcome!

Please feel free to contact me through github or on the #haskell IRC channel on irc.freenode.net.

-Edward Kmett