#5927: A type-level "implies" constraint on Constraints
----------------------------------------+-----------------------------------
Reporter: illissius | Owner:
Type: feature request | Status: new
Priority: normal | Milestone: 7.6.1
Component: Compiler (Type checker) | Version: 7.4.1
Keywords: | Os: Unknown/Multiple
Architecture: Unknown/Multiple | Failure: None/Unknown
Difficulty: Unknown | Testcase:
Blockedby: | Blocking:
Related: |
----------------------------------------+-----------------------------------
Comment(by illissius):
The canonical example of what #2893 lets you write is something like:
{{{
instance (Monad m, forall a. Monoid (m a)) => MonadPlus m where ...
}}}
The example from the paper is:
{{{
instance (Binary a, forall b. Binary b => Binary (f b)) => Binary (GRose f
a) where ...
}}}
And the example here was:
{{{
instance (forall a. c a => Show a) => Show (Exists c) where ...
}}}
The way I have it in my head it's not clear to me that #2893 would, on its
own, let you write the latter two examples. To put it simplistically it
would you write the {{{forall}}}, but not the {{{=>}}}.
The way I'm reading the second example above is, "if (Binary a), and also
(Binary (f b)) follows from (Binary b) for any b, then Binary (GRose f
a)". The first example is saying, "if (Monad m), and also (Monoid (m a))
for any a, then (!MonadPlus m)". The difference is that in the !MonadPlus
example and all existing Haskell there's noplace where you say "if b
follows from a, then c", you only say "if b, then c". But the latter two
examples do also have this "if b follows from a, then c" construct. And I
think #2893 is what would let you say the "for any a" part of it, while
the feature described by this ticket is what would let you say the "if b
follows from a, then" part.
If we look at three simple examples:
{{{
instance forall a. C (A a) => D A where ...
}}}
{{{
instance (C a => C (A a)) => E (A a) where ...
}}}
{{{
instance (forall a. C a => C (A a)) => D A where ...
}}}
then #2893 (let's call it !QuantifiedConstraints) would let you write the
first example, this ticket (let's call it !ImplicationConstraints) would
let you write the second example, but only their combination would let you
write the third example.
I'm imagining that, with !ImplicationConstraints, (=>) would be a type
level operator similar to (~):
{{{
(~) :: forall k. k -> k -> Constraint
(=>) :: Constraint -> Constraint -> Constraint
}}}
and you would need !QuantifiedConstraints to be able to use (=>) to also
talk about {{{k1...kN -> Constraint}}}s.
I hope this is clearer. Don't hesitate to holler at me if I'm talking
nonsense.
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/5927#comment:4>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
