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
On Wed, Aug 01, 2007 at 05:29:19PM -0700, Conal Elliott wrote:
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
No quotes - [] is both Applicative and Monoid. Should [String] ["ab","cd"] `mappend` ["ef","gh"] give ["ab","cd","ef","gh"] or ["abef","abgh","cdef","cdgh"]?
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).
It's something I've wanted... Got a link for hereditary Harrop formulas so I can add them to my to-implement-when-Qhc-is-good-enough list? Google isn't telling me much about them except how to add support for constaints, which isn't terribly helpful. Stefan
Hello,
It's something I've wanted... Got a link for hereditary Harrop formulas so I can add them to my to-implement-when-Qhc-is-good-enough list? Google isn't telling me much about them except how to add support for constaints, which isn't terribly helpful.
This paper has a good description; it focuses on how to make a logic programming language based on them. http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/apal91.pdf -Jeff
On Wed, Aug 01, 2007 at 05:29:19PM -0700, Conal Elliott wrote:
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
No quotes - [] is both Applicative and Monoid. Should [String] ["ab","cd"] `mappend` ["ef","gh"] give ["ab","cd","ef","gh"] or ["abef","abgh","cdef","cdgh"]?
Sure enough - a genuine conflict. Thanks for the simple counter-example, Stefan.
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).
It's something I've wanted... Got a link for hereditary Harrop formulas so I can add them to my to-implement-when-Qhc-is-good-enough list? Google isn't telling me much about them except how to add support for constaints, which isn't terribly helpful.
In addition to the "uniform proofs" paper Jeff P mentioned, here's a paper that describes a progression of interpreters in ML, including HHFs. The culmination is a somewhat efficient implementation of a language very like LambdaProlog. http://citeseer.ist.psu.edu/elliott90semifunctional.html Cheers, - Conal
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@haskell.org [mailto:haskell-bounces@haskell.org] On Behalf Of Conal Elliott Sent: 02 August 2007 01:29 To: haskell@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
participants (4)
-
Conal Elliott -
jeff p -
Simon Peyton-Jones -
Stefan O'Rear