type class instance selection & search
I keep running into situations in which I want more powerful search in selecting type class instances. One example I raised in June, in which all of the following instances are useful.
instance (Functor g, Functor f) => Functor (O g f) where fmap h (O gf) = O (fmap (fmap h) gf)
instance (Cofunctor g, Cofunctor f) => Functor (O g f) where fmap h (O gf) = O (cofmap (cofmap h) gf)
instance (Functor g, Cofunctor f) => Cofunctor (O g f) where cofmap h (O gf) = O (fmap (cofmap h) gf)
instance (Cofunctor g, Functor f) => Cofunctor (O g f) where cofmap h (O gf) = O (cofmap (fmap h) gf)
My understanding is that this sort of instance collection doesn't work together because instance selection is based only on the matching the head of an instance declaration (part after the "=>"). I'm wondering why not use the preconditions as well, via a Prolog-like, backward-chaining search for much more flexible instance selection? Going further, has anyone investigated using Prolog as a model for instance selection? Better yet, how about LambdaProlog ( http://www.lix.polytechnique.fr/Labo/Dale.Miller/lProlog), which generalizes from Horn clauses to (higher-order) hereditary Harrop formulas, including (restricted but powerful) universals, implication, and existentials? Once search is in there, ambiguity can arise, but perhaps the compiler could signal an error in that case (i.e., if the ambiguity is not eliminated by further search pruning). My motivation: I've been playing with a programming style in which my type formulation leads to automatic construction of much of the code, thanks to use of Functor, Applicative, Monoid, and type composition. An example is http://haskell.org/haskellwiki/Applicative_data-driven_programming, and I'm trying now to do the same to create a much simpler implementation of Eros ( http://conal.net/papers/Eros). I think this programming style is what Conor was alluding to recently as "types don't just contain data, types explain data" (http://article.gmane.org/gmane.comp.lang.haskell.cafe/26520). (Conor: I hope you chime in.) My hunch is that this programming style tends to run up against the head-only instance matching mechanism and would work much better with a more powerful means of selecting instances. - Conal
Conal Elliott <conal@conal.net> wrote in article <ea8ae9fb0707311208j9f3fcf7m92bef8f54aea3dd8@mail.gmail.com> in gmane.comp.lang.haskell.general:
I keep running into situations in which I want more powerful search in selecting type class instances.
I agree that it's quite useful for instance search to backtrack, if not desirable in all cases. Proof search is program search, after all. Of course, allowing undecidable instances, we can build backtracking into instance search ourselves by representing the state of a backtracking machine as a type. http://okmij.org/ftp/Haskell/poly2.txt -- Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig And if thou gaze into the abyss, the abyss...actually finds you pretty creepy.
Thanks for these pointers, Ken. And belated thanks to Oleg for his reply in June. Impressive tricks! Perhaps I'm not the only person who'd prefer a more straightforward formulation of backtracking search? Cheers, - Conal On 7/31/07, Chung-chieh Shan <ccshan@post.harvard.edu> wrote:
Conal Elliott <conal@conal.net> wrote in article < ea8ae9fb0707311208j9f3fcf7m92bef8f54aea3dd8@mail.gmail.com> in gmane.comp.lang.haskell.general:
I keep running into situations in which I want more powerful search in selecting type class instances.
I agree that it's quite useful for instance search to backtrack, if not desirable in all cases. Proof search is program search, after all.
Of course, allowing undecidable instances, we can build backtracking into instance search ourselves by representing the state of a backtracking machine as a type. http://okmij.org/ftp/Haskell/poly2.txt
-- Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig And if thou gaze into the abyss, the abyss...actually finds you pretty creepy.
_______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Here are some other instances that could work with backward chaining: \begin{code} instance Monad m => Applicative m where pure = return (<*>) = ap instance (Applicative f, Monoid a) => Monoid (f a) where mempty = pure mempty mappend = liftA2 mappend instance (Applicative f, Num a) => Num (f a) where (+) = liftA2 (+) fromInteger = pure . fromInteger -- etc \end{code} Currently, I place such instance declarations in comments as boilerplate to be instantiated manually. - Conal On 7/31/07, Conal Elliott <conal@conal.net> wrote:
I keep running into situations in which I want more powerful search in selecting type class instances. One example I raised in June, in which all of the following instances are useful.
instance (Functor g, Functor f) => Functor (O g f) where fmap h (O gf) = O (fmap (fmap h) gf)
instance (Cofunctor g, Cofunctor f) => Functor (O g f) where fmap h (O gf) = O (cofmap (cofmap h) gf)
instance (Functor g, Cofunctor f) => Cofunctor (O g f) where cofmap h (O gf) = O (fmap (cofmap h) gf)
instance (Cofunctor g, Functor f) => Cofunctor (O g f) where cofmap h (O gf) = O (cofmap (fmap h) gf)
My understanding is that this sort of instance collection doesn't work together because instance selection is based only on the matching the head of an instance declaration (part after the "=>"). I'm wondering why not use the preconditions as well, via a Prolog-like, backward-chaining search for much more flexible instance selection? Going further, has anyone investigated using Prolog as a model for instance selection? Better yet, how about LambdaProlog ( http://www.lix.polytechnique.fr/Labo/Dale.Miller/lProlog), which generalizes from Horn clauses to (higher-order) hereditary Harrop formulas, including (restricted but powerful) universals, implication, and existentials? Once search is in there, ambiguity can arise, but perhaps the compiler could signal an error in that case ( i.e., if the ambiguity is not eliminated by further search pruning).
My motivation: I've been playing with a programming style in which my type formulation leads to automatic construction of much of the code, thanks to use of Functor, Applicative, Monoid, and type composition. An example is http://haskell.org/haskellwiki/Applicative_data-driven_programming, and I'm trying now to do the same to create a much simpler implementation of Eros ( http://conal.net/papers/Eros). I think this programming style is what Conor was alluding to recently as "types don't just contain data, types explain data" (http://article.gmane.org/gmane.comp.lang.haskell.cafe/26520). (Conor: I hope you chime in.) My hunch is that this programming style tends to run up against the head-only instance matching mechanism and would work much better with a more powerful means of selecting instances.
- Conal
Hello,
My understanding is that this sort of instance collection doesn't work together because instance selection is based only on the matching the head of an instance declaration (part after the "=>"). I'm wondering why not use the preconditions as well, via a Prolog-like, backward-chaining search for much more flexible instance selection? Going further, has anyone investigated using Prolog as a model for instance selection?
I have also wanted more powerful, Prolog-like search for instance selection; it would be particularly convenient to think of type variables as logic variables. I think the main argument against this is that it fundamentally changes the interpretation of constraints; in particular, if you really used a Prolog-style search, the order in which you place constraints can affect type checking. Is there a sensible way for instance selection to depend on the "body" which doesn't result in this?
Better yet, how about LambdaProlog ( http://www.lix.polytechnique.fr/Labo/Dale.Miller/lProlog), which generalizes from Horn clauses to (higher-order) hereditary Harrop formulas, including (restricted but powerful) universals, implication, and existentials?
Having hereditary Harrop formulas at the type level would be cool. It would also probably require type level lambdas. There was a recent discussion about type level lambdas in Haskell which ended with the observations that 1) it would mess up unification (i.e. make it undecidable and/or too hard) to have explicit type level lambdas; and 2) they are already implicitly there (this was pointed out by Oleg) since one can define a type level application and type level functions. I think 1) is a bit of a cop-out since you could always restrict to pattern unification (L-lamda unification) which is decidable and has MGUs. 2) is true, but these implicit lambdas don't play very well with instance selection and require that all reductions are spelled out via an Apply type class. I think it might be useful/interesting to have type level lambdas, and pattern unification, even without turning instance selection into proof search.
Once search is in there, ambiguity can arise, but perhaps the compiler could signal an error in that case ( i.e., if the ambiguity is not eliminated by further search pruning).
This seems like a slippery slope to me. Although I would like having a full fledged (higher-order) logic programming language in which to write type level programs, I am not sure it's a good idea for Haskell in general. I tend to get concerned when type class constraints get too big/complicated to be obviously correct-- what good is the type checker saying something satisfies a constraint if we're not sure that the specification of the constraint itself is correct? -Jeff
If only for those watching from home, here are some references. jeff p <mutjida@gmail.com> wrote in article <a6403bb90707312018t7ab9409enb0999b043e01f992@mail.gmail.com> in gmane.comp.lang.haskell.general:
Better yet, how about LambdaProlog ( http://www.lix.polytechnique.fr/Labo/Dale.Miller/lProlog), which generalizes from Horn clauses to (higher-order) hereditary Harrop formulas, including (restricted but powerful) universals, implication, and existentials? Having hereditary Harrop formulas at the type level would be cool. It would also probably require type level lambdas.
On that note: Trifonov, Valery. 2003. Simulating quantified class constraints. In Proceedings of the 2003 Haskell workshop, 98-102. New York: ACM Press. http://flint.cs.yale.edu/trifonov/papers/sqcc.pdf http://flint.cs.yale.edu/trifonov/papers/sqcc.ps.gz
There was a recent discussion about type level lambdas in Haskell which ended with the observations that 1) it would mess up unification (i.e. make it undecidable and/or too hard) to have explicit type level lambdas; and 2) they are already implicitly there (this was pointed out by Oleg) since one can define a type level application and type level functions. I think 1) is a bit of a cop-out since you could always restrict to pattern unification (L-lamda unification) which is decidable and has MGUs.
On that note: Neubauer, Matthias, and Peter Thiemann. 2002. Type classes with more higher-order polymorphism. In ICFP '02: Proceedings of the ACM international conference on functional programming. New York: ACM Press. http://www.informatik.uni-freiburg.de/~neubauer/papers/icfp02.pdf http://www.informatik.uni-freiburg.de/~neubauer/papers/icfp02.ps.gz -- Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig "Injustice is happening now; suffering is happening now. We have choices to make now. To insist on absolute certainty before starting to apply ethics to life decisions is a way of choosing to be amoral." -Richard Stallman
On 7/31/07, jeff p <mutjida@gmail.com> wrote:
Hello,
My understanding is that this sort of instance collection doesn't work together because instance selection is based only on the matching the head of an instance declaration (part after the "=>"). I'm wondering why not use the preconditions as well, via a Prolog-like, backward-chaining search for much more flexible instance selection? Going further, has anyone investigated using Prolog as a model for instance selection?
I have also wanted more powerful, Prolog-like search for instance selection; it would be particularly convenient to think of type variables as logic variables.
I think the main argument against this is that it fundamentally changes the interpretation of constraints; in particular, if you really used a Prolog-style search, the order in which you place constraints can affect type checking. Is there a sensible way for instance selection to depend on the "body" which doesn't result in this?
How could constraint order affect type checking? Via "cut" ("!")? I'd omit cut. I see how order of constraints or instance declarations might determine order of solutions produced (as in Prolog). If the compiler rejects ambiguity (existence of multiple solutions), then I'd wouldn't expect the order to have any visible effect.
Better yet, how about LambdaProlog ( http://www.lix.polytechnique.fr/Labo/Dale.Miller/lProlog), which generalizes from Horn clauses to (higher-order) hereditary Harrop formulas, including (restricted but powerful) universals, implication, and existentials?
Having hereditary Harrop formulas at the type level would be cool. It would also probably require type level lambdas.
Type level lambdas may not be necessary for HHFs. For simplicity, LambdaProlog encodes its universals and existentials via lambdas. I think we could use type lambdas if we wanted but wouldn't have to. Personally, I'd like to have type level lambdas, assuming we can implement them soundly.
There was a recent discussion about type level lambdas in Haskell which ended with the observations that 1) it would mess up unification (i.e. make it undecidable and/or too hard) to have explicit type level lambdas; and 2) they are already implicitly there (this was pointed out by Oleg) since one can define a type level application and type level functions. I think 1) is a bit of a cop-out since you could always restrict to pattern unification (L-lamda unification) which is decidable and has MGUs. 2) is true, but these implicit lambdas don't play very well with instance selection and require that all reductions are spelled out via an Apply type class.
I think it might be useful/interesting to have type level lambdas, and pattern unification, even without turning instance selection into proof search.
Agreed. And vice versa.
Once search is in there, ambiguity can arise, but perhaps the compiler could signal an error in that case ( i.e., if the ambiguity is not eliminated by further search pruning).
This seems like a slippery slope to me.
Although I would like having a full fledged (higher-order) logic programming language in which to write type level programs, I am not sure it's a good idea for Haskell in general. I tend to get concerned when type class constraints get too big/complicated to be obviously correct-- what good is the type checker saying something satisfies a constraint if we're not sure that the specification of the constraint itself is correct?
-Jeff
I like this goal of and motivation for simplicity in type specifications. My hope is that a Lambda-Prolog (or some such, and minus cut) would provide a simpler (and more expressive) basis than the very tricky encodings available now (type level function application, backtracking with type-level numeral annotations, etc). - Conal
Conal It certainly makes sense to do backward chaining, but I don't know any Haskell implementation that's tried it. It'd be more complicated in the presence of functional dependencies, since we must "undo" any unifications done as a result of discarded searches, much like the "trail" in a Prolog implementation. To be honest I can't see myself trying this anytime soon. Because of the unification part, it'd be a significant structural change. And one would need to dig into the theory to make sure that the algorithm was both sound and complete (finds all solutions). Simon From: haskell-bounces@haskell.org [mailto:haskell-bounces@haskell.org] On Behalf Of Conal Elliott Sent: 31 July 2007 20:09 To: haskell@haskell.org Subject: [Haskell] type class instance selection & search I keep running into situations in which I want more powerful search in selecting type class instances. One example I raised in June, in which all of the following instances are useful.
instance (Functor g, Functor f) => Functor (O g f) where fmap h (O gf) = O (fmap (fmap h) gf)
instance (Cofunctor g, Cofunctor f) => Functor (O g f) where fmap h (O gf) = O (cofmap (cofmap h) gf)
instance (Functor g, Cofunctor f) => Cofunctor (O g f) where cofmap h (O gf) = O (fmap (cofmap h) gf)
instance (Cofunctor g, Functor f) => Cofunctor (O g f) where cofmap h (O gf) = O (cofmap (fmap h) gf)
My understanding is that this sort of instance collection doesn't work together because instance selection is based only on the matching the head of an instance declaration (part after the "=>"). I'm wondering why not use the preconditions as well, via a Prolog-like, backward-chaining search for much more flexible instance selection? Going further, has anyone investigated using Prolog as a model for instance selection? Better yet, how about LambdaProlog ( http://www.lix.polytechnique.fr/Labo/Dale.Miller/lProlog), which generalizes from Horn clauses to (higher-order) hereditary Harrop formulas, including (restricted but powerful) universals, implication, and existentials? Once search is in there, ambiguity can arise, but perhaps the compiler could signal an error in that case ( i.e., if the ambiguity is not eliminated by further search pruning).
|My understanding is that this sort of instance collection doesn't work together because instance selection is based only on the matching the head of an instance declaration (part after the "=>"). I'm wondering why not use the preconditions as well, via a Prolog-like, backward-chaining search for much more flexible instance selection?
It certainly makes sense to do backward chaining, but I don't know any Haskell implementation that's tried it. It'd be more complicated in the presence of functional dependencies, since we must "undo" any unifications done as a result of discarded searches, much like the "trail" in a Prolog implementation.
there was some discussion of this on the haskell-prime list some time ago, indicating that there is some room for exploration between the current no-context and a full backtrack-over-all-contexts. in particular, since type class semantics these days are based on constraint handling rules, it would be useful to provide haskell-syntax access to chr guards. one could then, as in chr, restrict the kind of type predicates permitted in guards (no backtracking, no unification), and take guards into account for instance selection, but still "ignore" the full context. that way, one remains in a committed-choice language, with no unification before commit, so no need to undo unifications (chr implementations tend to provide 'unifiable' as well as 'unify', and the former may be used in guards). in many of the cases i'd like to use the context for instance selection, the decision comes down to a simple 'unifiable'/'not unifiable', which could be handled via guards. that is why TypeCast is so central in HList, or why a more cumbersome encoding via newtypes is often possible. claus
Conal Elliott wrote:
I keep running into situations in which I want more powerful search in selecting type class instances. One example I raised in June, in which all of the following instances are useful.
instance (Functor g, Functor f) => Functor (O g f) where fmap h (O gf) = O (fmap (fmap h) gf)
instance (Cofunctor g, Cofunctor f) => Functor (O g f) where fmap h (O gf) = O (cofmap (cofmap h) gf)
instance (Functor g, Cofunctor f) => Cofunctor (O g f) where cofmap h (O gf) = O (fmap (cofmap h) gf)
instance (Cofunctor g, Functor f) => Cofunctor (O g f) where cofmap h (O gf) = O (cofmap (fmap h) gf)
My understanding is that this sort of instance collection doesn't work together because instance selection is based only on the matching the head of an instance declaration (part after the "=>"). I'm wondering why not use the preconditions as well, via a Prolog-like, backward-chaining search for much more flexible instance selection?
There are some fundamental problems/design choices for type classes in conjunction with separate compilation/modularity that need to be researched before trying anything like that. In particular, any ad-hoc Prolog, CHR or -fallow-undecidable-instances just ignores these problems and doesn't solve them. The problem with the Functor/Cofunctor instances is that they are ambiguous as soon as a type constructor X is made an instance of both Functor and Cofunctor . Of course, such an X cannot exist in a mathematically useful way (really ?) but the current system doesn't allow to tell this to the compiler. Alas, we can always say instance Functor F where fmap = undefined instance Cofunctor F where cofmap = undefined The problem is not so much that there might be ambiguities, but how to detect and when to report them. Consider: module F where class Functor f class Cofunctor f module O where import F data O f g a instance (Functor g, Functor f ) => Functor (O g f) instance (Cofunctor g, Cofunctor f) => Functor (O g f) module X where import F data X a instance Functor X instance Cofunctor X module Unsound where import F import O import X type Unsound a = O X X a The current design rejects module O. - Another possible design choice is to reject only module Unsound, i.e. when the conflicting instance declarations both come into scope. But it may be tricky/undecidable to to detect such conflicting instances. - A third possibility is to reject module X based on hypothetical information from module F that states that the instances of Functor and Cofunctor are disjoint. - The fourth choice is to not reject any module but to wait until a function really uses the type Unsound a and to reject this function. This is probably a bad idea since this may delay the error even further to modules that import Unsound. While we're at it, another rather often requested feature of type classes that needs considerable thinking is explicit instance import/export. With this one, we could make module X "locally sound" by simply not exporting either the Functor or the Cofunctor instance. module X (X, instance Functor X) where ... Currently, all instances are globally visible. The problem with explicit import/export is that program correctness depends on global visibility! Consider the following example (due to Bertram Felgenhauer): module A where newtype A = A Int deriving (Eq) module OrdA1 (lookup1) where import A import Data.Map -- don't export this instance instance Ord A where compare (A x) (A y) = compare x y lookup1 :: A -> Data.Map A a -> Maybe a lookup1 = Data.Map.lookup module OrdA2 (lookup2, m) where import A import Data.Map -- don't export this instance instance Ord A where compare (A x) (A y) = compare y x lookup2 :: A -> Data.Map A a -> Maybe a lookup2 = Data.Map.lookup m = Data.Map.fromList $ zip [1..] [1,2,3,4] module Wrong where import Data.Map import OrdA1 import OrdA2 wrong = lookup1 1 m == lookup2 1 m Here, the module Wrong has two lookup functions with different invariants on one and the same map type. In other words, the different Ord instances for A will mess up the invariants of the Map A a implementation and will eventually even lead to pattern match failures. Being able to mess up invariants by class export/import is quite dangerous. Regards, apfelmus
Am Mittwoch, 1. August 2007 14:41 schrieb apfelmus:
[…]
The problem with the Functor/Cofunctor instances is that they are ambiguous as soon as a type constructor X is made an instance of both Functor and Cofunctor . Of course, such an X cannot exist in a mathematically useful way (really ?)
I think, it can: newtype Const a b = MkConst a instance Functor (Const a) where fmap fun (MkConst a) = MkConst a instance Cofunctor (Const a) where cofmap fun (MkConst a) = MkConst a
[…]
Best wishes, Wolfgang
On 8/1/07, apfelmus <apfelmus@quantentunnel.de> wrote:
There are some fundamental problems/design choices for type classes in conjunction with separate compilation/modularity that need to be researched before trying anything like that. In particular, any ad-hoc Prolog, CHR or -fallow-undecidable-instances just ignores these problems and doesn't solve them.
The problem with the Functor/Cofunctor instances is that they are ambiguous as soon as a type constructor X is made an instance of both Functor and Cofunctor . Of course, such an X cannot exist in a mathematically useful way (really ?) but the current system doesn't allow to tell this to the compiler. Alas, we can always say
instance Functor F where fmap = undefined instance Cofunctor F where cofmap = undefined
The problem is not so much that there might be ambiguities, but how to detect and when to report them.
I agree: and my intent is that the compiler would detect and report the ambiguity as an error.
Consider:
module F where class Functor f class Cofunctor f
module O where import F
data O f g a instance (Functor g, Functor f ) => Functor (O g f) instance (Cofunctor g, Cofunctor f) => Functor (O g f)
module X where import F
data X a instance Functor X instance Cofunctor X
module Unsound where import F import O import X
type Unsound a = O X X a
The current design rejects module O. - Another possible design choice is to reject only module Unsound, i.e. when the conflicting instance declarations both come into scope. But it may be tricky/undecidable to to detect such conflicting instances. - A third possibility is to reject module X based on hypothetical information from module F that states that the instances of Functor and Cofunctor are disjoint. - The fourth choice is to not reject any module but to wait until a function really uses the type Unsound a and to reject this function. This is probably a bad idea since this may delay the error even further to modules that import Unsound.
I'd be much happier with any of the latter three options than with the current design. - Conal
participants (7)
-
apfelmus -
Chung-chieh Shan -
Claus Reinke -
Conal Elliott -
jeff p -
Simon Peyton-Jones -
Wolfgang Jeltsch