[Haskell] Quantified class constraints (& back-chaining)

[Simon Peyton-Jones]

See also the paper that Ralf and I wrote about "Derivable type classes" (on my pubs page) which uses quantified constraints.

Quantified constraints would be another perfectly sensible extension.  GHC does not support them at the moment though.  I'm really not too sure how much work it'd be to add them; quite significant I suspect.

Simon

From: haskell-bounces at haskell.org [mailto:haskell-bounces at haskell.org] On Behalf Of Conal Elliott
Sent: 02 August 2007 01:29
To: haskell at haskell.org
Subject: [Haskell] Quantified class constraints (& back-chaining)

I'm developing a type constructor class and want the constraint forall a. Monoid (m a) (where m :: * -> * ), which is neither legal Haskell, nor supported by GHC.

As a work-around, I used the first encoding suggested in "Simulating Quantified Class Constraints" (Valery Trifonov, Haskell Workshop '03).  Add a type class

    class Monoid_f m where
      mempty_f  :: forall a. m a
      mappend_f :: forall a. m a -> m a -> m a

and an instance *schema*

    -- instance Monoid_f f where { mempty_f = mempty ; mappend_f = mappend }

to instantiate manually wherever necessary. For instance,

    instance Monoid_f [] where { mempty_f = mempty ; mappend_f = mappend }


The paper's second approach is to replace the schema and multiple instantiations with a single instance.

    instance Monoid_f f => Monoid (f a) where
      { mempty = mempty_f ; mappend = mappend_f }

As the paper points out,
Unfortunately, due to the type variable f in the head of the instance type, this declaration is not in Haskell 98; however, at least two implementations support extensions allowing such declarations.

Sadly, this solution runs into the problem of instance selection based only on head-matching, not back-chaining into constraints.  For instance, I'd like also to use the following "conflicting" declaration.

    instance (Applicative f, Monoid a) => Monoid (f a) where
      mempty  = pure mempty
      mappend = liftA2 mappend

What's the state of thinking & doing with regard to universally quantified class constraints?

Note that hereditary Harrop formulas do include universally quantified goals.  Less ambitiously, I think GHC's type-checker already deals with universally-quantified variables, so perhaps quantified constraints are not a great reach (just guessing).

  Cheers,  - Conal
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell/attachments/20070802/454d4727/attachment-0001.htm