<p style="margin:0px;font-size:11px;line-height:normal;font-family:'Helvetica Neue'"><br></p>
<p style="margin:0px;font-size:11px;line-height:normal;font-family:'Helvetica Neue'"><span style="font-size:11pt">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].</span></p>
<p style="margin:0px;font-size:11px;line-height:normal;font-family:'Helvetica Neue';min-height:13.1px"><span style="font-size:11pt"></span><br></p>
<p style="margin:0px;font-size:11px;line-height:normal;font-family:'Helvetica Neue'"><span style="font-size:11pt">Consider modelling the logic for somewhat-injective type functions. Take type-level Boolean `And` [5].</span></p>
<p style="margin:0px;font-size:11px;line-height:normal;font-family:'Helvetica Neue';min-height:13.1px"><span style="font-size:11pt"></span><br></p>
<p style="margin:0px;font-size:11px;line-height:normal;font-family:'Helvetica Neue'"><span style="font-size:11pt">`And` is not fully injective but:</span></p>
<p style="margin:0px;font-size:11px;line-height:normal;font-family:'Helvetica Neue'"><span style="font-size:11pt">* If the result is True, the two arguments must be True.</span></p>
<p style="margin:0px;font-size:11px;line-height:normal;font-family:'Helvetica Neue'"><span style="font-size:11pt">* If the result is False and one argument is True, the other must be False.</span></p>
<p style="margin:0px;font-size:11px;line-height:normal;font-family:'Helvetica Neue';min-height:13.1px"><span style="font-size:11pt"></span><br></p>
<p style="margin:0px;font-size:11px;line-height:normal;font-family:'Helvetica Neue'"><span style="font-size:11pt"> class ( b3 ~ True => (b1 ~ True, b2 ~ True),</span></p>
<p style="margin:0px;font-size:11px;line-height:normal;font-family:'Helvetica Neue'"><span style="font-size:11pt"> (b3 ~ False, b1 ~ True) => b2 ~ False ) -- etc</span></p>
<p style="margin:0px;font-size:11px;line-height:normal;font-family:'Helvetica Neue'"><span style="font-size:11pt"> => And (b1 :: Bool) (b2 :: Bool) (b3 :: Bool) | b1 b2 -> b3 where …</span></p>
<p style="margin:0px;font-size:11px;line-height:normal;font-family:'Helvetica Neue';min-height:13.1px"><span style="font-size:11pt"></span><br></p>
<p style="margin:0px;font-size:11px;line-height:normal;font-family:'Helvetica Neue'"><span style="font-size:11pt">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.)</span></p>
<p style="margin:0px;font-size:11px;line-height:normal;font-family:'Helvetica Neue';min-height:13.1px"><span style="font-size:11pt"></span><br></p>
<p style="margin:0px;font-size:11px;line-height:normal;font-family:'Helvetica Neue';min-height:13.1px"><span style="font-size:11pt"></span><br></p>
<p style="margin:0px;font-size:11px;line-height:normal;font-family:'Helvetica Neue'"><span style="font-size:11pt">Come to that, can we capture the logic of the FunDep? (The hs2017 paper hints we might.)</span></p>
<p style="margin:0px;font-size:11px;line-height:normal;font-family:'Helvetica Neue';min-height:13.1px"><span style="font-size:11pt"></span><br></p>
<p style="margin:0px;font-size:11px;line-height:normal;font-family:'Helvetica Neue'"><span style="font-size:11pt"> class ( {- as before -},</span></p>
<p style="margin:0px;font-size:11px;line-height:normal;font-family:'Helvetica Neue'"><span style="font-size:11pt"> ( forall b3’. And b1 b2 b3’ => b3’ ~ b3 ) )</span></p>
<p style="margin:0px;font-size:11px;line-height:normal;font-family:'Helvetica Neue'"><span style="font-size:11pt"> => And (b1 :: Bool) (b2 :: Bool) (b3 :: Bool) | b1 b2 -> b3 where …</span></p>
<p style="margin:0px;font-size:11px;line-height:normal;font-family:'Helvetica Neue';min-height:13.1px"><span style="font-size:11pt"></span><br></p>
<p style="margin:0px;font-size:11px;line-height:normal;font-family:'Helvetica Neue'"><span style="font-size:11pt">This might come closer to the logic of FunDeps as originally specified by Mark P Jones, which ghc doesn’t quite reach to [6].</span></p>
<p style="margin:0px;font-size:11px;line-height:normal;font-family:'Helvetica Neue';min-height:13.1px"><span style="font-size:11pt"></span><br></p>
<p style="margin:0px;font-size:11px;line-height:normal;font-family:'Helvetica Neue'"><span style="font-size:11pt">OTOH we now have a cyclical superclass constraint, which ain’t allowed.</span></p>
<p style="margin:0px;font-size:11px;line-height:normal;font-family:'Helvetica Neue';min-height:13.1px"><span style="font-size:11pt"></span><br></p>
<p style="margin:0px;font-size:11px;line-height:normal;font-family:'Helvetica Neue';min-height:13.1px"><span style="font-size:11pt"></span><br></p>
<p style="margin:0px;font-size:11px;line-height:normal;font-family:'Helvetica Neue';min-height:13.1px"><span style="font-size:11pt"></span><br></p>
<p style="margin:0px;font-size:11px;line-height:normal;font-family:'Helvetica Neue'"><span style="font-size:11pt">[1] <a href="https://github.com/ghc-proposals/ghc-proposals/pull/109"><span style="font-size:11pt">https://github.com/ghc-proposals/ghc-proposals/pull/109</span></a></span></p>
<p style="margin:0px;font-size:11px;line-height:normal;font-family:'Helvetica Neue'"><span style="font-size:11pt">[2] <a href="https://ghc.haskell.org/trac/ghc/wiki/QuantifiedConstraints">https://ghc.haskell.org/trac/ghc/wiki/QuantifiedConstraints</a></span></p>
<p style="margin:0px;font-size:11px;line-height:normal;font-family:'Helvetica Neue'"><span style="font-size:11pt">[3] <a href="https://ghc.haskell.org/trac/ghc/ticket/2893">https://ghc.haskell.org/trac/ghc/ticket/2893</a></span></p>
<p style="margin:0px;font-size:11px;line-height:normal;font-family:'Helvetica Neue'"><span style="font-size:11pt">[4] <a href="https://mail.haskell.org/pipermail/libraries/2017-December/028377.html">https://mail.haskell.org/pipermail/libraries/2017-December/028377.html</a></span></p>
<p style="margin:0px;font-size:11px;line-height:normal;font-family:'Helvetica Neue'"><span style="font-size:11pt">[5] <a href="https://mail.haskell.org/pipermail/ghc-devs/2017-November/015073.html"><span style="font-size:11pt">https://mail.haskell.org/pipermail/ghc-devs/2017-November/015073.html</span></a>, continued at</span></p>
<p style="margin:0px;font-size:11px;line-height:normal;font-family:'Helvetica Neue'"><span style="font-size:11pt"> <a href="https://mail.haskell.org/pipermail/glasgow-haskell-users/2017-November/026650.html"><span style="font-size:11pt">https://mail.haskell.org/pipermail/glasgow-haskell-users/2017-November/026650.html</span></a></span></p>
<p style="margin:0px;font-size:11px;line-height:normal;font-family:'Helvetica Neue'"><span style="font-size:11pt">[6] <a href="https://ghc.haskell.org/trac/ghc/ticket/10675">https://ghc.haskell.org/trac/ghc/ticket/10675</a></span></p>
<p style="margin:0px;font-size:11px;line-height:normal;font-family:'Helvetica Neue';min-height:13.1px"><span style="font-size:11pt"></span><br></p>
<p style="margin:0px;font-size:11px;line-height:normal;font-family:'Helvetica Neue'"><span style="font-size:11pt">AntC</span></p>
<p style="margin:0px;font-size:11px;line-height:normal;font-family:'Helvetica Neue';min-height:13.1px"><span style="font-size:11pt"></span><br></p>