Quantified Constraints and Injectivity

[Anthony Clayden]

I’m looking at the flurry of activity around Quantified Constraints [1, 2,
3], suggestion of uses for implication logic [4], and comments in the
hs2017 paper “raise the expressive power of type classes … to first-order
logic. … more expressive modelling …”[Abstract].


Consider modelling the logic for somewhat-injective type functions. Take
type-level Boolean `And` [5].


`And` is not fully injective but:

* If the result is True, the two arguments must be True.

* If the result is False and one argument is True, the other must be False.


    class ( b3 ~ True => (b1 ~ True, b2 ~ True),

               (b3 ~ False, b1 ~ True) => b2 ~ False )    -- etc

              => And (b1 :: Bool) (b2 :: Bool) (b3 :: Bool)  | b1 b2 -> b3
  where …


None of this is relying on `Bool` being a closed type AFAICT. (That’s the
usual downfall of trying to capture application logic in constraints.)



Come to that, can we capture the logic of the FunDep? (The hs2017 paper
hints we might.)


    class ( {- as before -},

               ( forall b3’. And b1 b2 b3’ => b3’ ~ b3 )   )

              => And (b1 :: Bool) (b2 :: Bool) (b3 :: Bool)  | b1 b2 -> b3
  where …


This might come closer to the logic of FunDeps as originally specified by
Mark P Jones, which ghc doesn’t quite reach to [6].


OTOH we now have a cyclical superclass constraint, which ain’t allowed.




[1] https://github.com/ghc-proposals/ghc-proposals/pull/109

[2] https://ghc.haskell.org/trac/ghc/wiki/QuantifiedConstraints

[3] https://ghc.haskell.org/trac/ghc/ticket/2893

[4] https://mail.haskell.org/pipermail/libraries/2017-December/028377.html

[5] https://mail.haskell.org/pipermail/ghc-devs/2017-November/015073.html,
continued at


https://mail.haskell.org/pipermail/glasgow-haskell-users/2017-November/026650.html

[6] https://ghc.haskell.org/trac/ghc/ticket/10675


AntC
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/glasgow-haskell-users/attachments/20180212/958c82ba/attachment.html>