Constraint implication

[Andrew Martin]

I agree that this would be cool. Here is some other discussion of this
topic:

   - A research paper proving its soundness:
   http://i.cs.hku.hk/~bruno/papers/hs2017.pdf
   - Responses on reddit:
   https://www.reddit.com/r/haskell/comments/6me3sv/quantified_class_constraints_pdf/
   - A very dated GHC issue: https://ghc.haskell.org/trac/ghc/ticket/2893

Many people seem to want this, but to my knowledge, no one has any plans to
work on it any time soon. I would not be surprised if it actually ended up
getting implemented one day. It could replace everything in
Data.Functor.Classes as well as half of the stuff from Data.Exists in my
`quantification` package.

On Wed, Dec 27, 2017 at 2:50 AM, Ryan Reich <ryan.reich at gmail.com> wrote:

> The Constraint kind appears to lack an interface to an important
> capability that is already part of the type checker: constraint
> implication.  Namely, the ability to provide a witness for the statement
> "constraint c1 implies constraint c2" or, more importantly, "for all a,
> constraint (c1 a) implies constraint (c2 a)", where c1 and c2 are now
> constraint-valued type functions (and possibly even for constraint
> functions with multiple parameters).  It seems to me that this can follow
> the pattern of the "magic" Coercible type class and the (non-magic)
> Coercion data type; it provides the programmer with an analogous value to
> this example that can be obtained in apparently no other way.
>
> _______________________________________________
> Libraries mailing list
> Libraries at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>
>


-- 
-Andrew Thaddeus Martin
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20171228/f0eed815/attachment.html>