[GHC] #2893: Implement "Quantified contexts" proposal

GHC ghc-devs at haskell.org
Sat Aug 20 21:37:10 UTC 2016


#2893: Implement "Quantified contexts" proposal
-------------------------------------+-------------------------------------
        Reporter:  porges            |                Owner:
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:  ⊥
       Component:  Compiler          |              Version:  6.10.1
      Resolution:                    |             Keywords:  proposal
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by Iceland_jack):

 This functionality does my head in so bear with me.

 In the definition of
 [https://www.reddit.com/r/haskell/comments/2ag8h2/recovering_preconditions_from_dataconstraint/civ9tm2
 Fmt], constraints of `(p a, p b, p (a, b))` are assumed for `:&`

 {{{#!hs
 data Fmt :: (* -> Constraint) -> (* -> *) -> * -> * where
   Int  :: p Int               => Fmt p r Int
   (:&) :: (p a, p b, p (a,b)) => Fmt p r a -> Fmt p r b -> Fmt p r (a,b)
   Lift :: p (r a)             => r a       -> Fmt p r a
 }}}

 `(p a, p b)` often implies `p (a, b)`, would this be captured by
 `QuantifiedConstraints`?

 {{{#!hs
   (:&) :: (p a, p b, forall xx yy. (p xx, p yy) => p (xx, yy))
        => Fmt p r a
        -> Fmt p r b
        -> Fmt p r (a,b)
 }}}

 Does this even give us any additional power? Is this more or less powerful
 than the `:=>` class from [https://hackage.haskell.org/package/constraints
 constraints]?

 {{{#!hs
 class b :=> h | h -> b where
   ins :: b :- h

 instance (Eq      a, Eq      b) :=> Eq      (a, b) where ins = Sub Dict
 instance (Ord     a, Ord     b) :=> Ord     (a, b) where ins = Sub Dict
 instance (Show    a, Show    b) :=> Show    (a, b) where ins = Sub Dict
 instance (Read    a, Read    b) :=> Read    (a, b) where ins = Sub Dict
 instance (Bounded a, Bounded b) :=> Bounded (a, b) where ins = Sub Dict
 instance (Monoid  a, Monoid  b) :=> Monoid  (a, b) where ins = Sub Dict
 ...
 }}}

 What if we assume that GHC generates instances of `:=>`?

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/2893#comment:18>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler


More information about the ghc-tickets mailing list