Re: Local evidence and type class instances
Hello, Now that the Glorious New type checker can handle local evidence seamlessly, is it a big implementation burden to extend it to deal with local *type class instances* in addition to local *equality constraints*? For example, you could write this: f :: Bool f = id id where instance Ord (a - b) where _ `compare` _ = LT I dislike the fact that you can produce incoherent instances with that extension. How about a restricted version that only works on fresh types? f :: Bool - Bool f b = N id N id where -- N is a fresh type, unique to a particular application of f. newtype N = N (a - b) instance Ord N where _ `compare` _ = LT This is sufficient for implicit configurations, and avoids the overlap of the new instances with existing instances. I don't know how much extra burden local type definitions like these would add. Bertram ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
RE: Local evidence and type class instances
| Now that the Glorious New type checker can handle local evidence | seamlessly, is it a big implementation burden to extend it to deal | with local *type class instances* in addition to local *equality | constraints*? ... | Are there big theoretical problems with this extension, or is it just | a lack of engineering effort that has prevented its implementation? The issues I know about are a) overlap (of course) b) coherence (two different instances in two places) c) if you add associated types, then soundness too d) completeness Concerning (c) you can't define (type instance F Int = Bool) in one place and (type instance F Int = Char) somewhere else, or you'll have seg faults. GHC checks that you don't, but it can only do that because the instances are global. Perhaps most important Concerning (d) we only have a theory for local *constraints*, not for local *constraint schemes* (ie with foralls in them). To get complete inference with assumptions like (F (G x) ~ G x) was tricky enough. Adding schemes would make it harder. But yes, it'd be useful. As well as Oleg and Ken's paper, the Derivable type classes paper that Ralf and I wrote some time ago argues for local constraint schemes. Simon ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Local evidence and type class instances
On Sat, Oct 16, 2010 at 7:11 AM, Max Bolingbroke batterseapo...@hotmail.com wrote: Hi GHC users, Now that the Glorious New type checker can handle local evidence seamlessly, is it a big implementation burden to extend it to deal with local *type class instances* in addition to local *equality constraints*? For example, you could write this: f :: Bool f = id id where instance Ord (a - b) where _ `compare` _ = LT Along similar lines as my last post, would I be able to write the following type signature: myFunct :: Ord Int = Int - (...) and have it always use the local instance for Ord Int? Is this the type that the type checker would infer for my function? Antoine ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Local evidence and type class instances
HI Antoine, I didn't know UHC already had this - thanks for the pointer! It seems they have read about implicit configurations too, as the example they use is very similar to the paper. In fact, they also have another extension to the concept that I was intentionally avoiding mentioning - they ensure that the lexically most closely bound instance is used to satisfy a demand for a type class operation. This means that you can sensibly have local instances that overlap global ones. I'm not sure how I feel about this feature, though I certainly see the motivation. On 16 October 2010 15:47, Antoine Latter aslat...@gmail.com wrote: Substituting f for f' in this example will change the meaning of the operation significantly, which is, in my mind, hard to explain and reason about. That's the behaviour I had in mind. There is no doubt that local instances are a big complexity increase, but IMHO this behaviour is relatively easy to reason about as long as you know about the dictionary passing translation. Indeed, it's practically mandatory to use dictionary-passing to implement this behaviour. Local instances would probably never get added to a compiler (like JHC) that doesn't use that technique. RE your later point: Along similar lines as my last post, would I be able to write the following type signature: myFunct :: Ord Int = Int - (...) and have it always use the local instance for Ord Int? Is this the type that the type checker would infer for my function? To my mind, if you have that signature, then myFunct would use whatever Ord Int instance was available at the use site of myFunct (i.e. wherever it was mentioned syntactically). It is certainly interesting to note that adding a context like this might be useful if you were using local instances. Cheers, Max ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Local evidence and type class instances
On Sat, Oct 16, 2010 at 11:41 AM, Max Bolingbroke batterseapo...@hotmail.com wrote: On 16 October 2010 15:47, Antoine Latter aslat...@gmail.com wrote: Substituting f for f' in this example will change the meaning of the operation significantly, which is, in my mind, hard to explain and reason about. That's the behaviour I had in mind. There is no doubt that local instances are a big complexity increase, but IMHO this behaviour is relatively easy to reason about as long as you know about the dictionary passing translation. Indeed, it's practically mandatory to use dictionary-passing to implement this behaviour. Local instances would probably never get added to a compiler (like JHC) that doesn't use that technique. From the point of view of the down-stream engineer, I feel that first class modules with a module algebra like OCaml would be a lot less mysterious. Once a thing is locally scoped, it's nicer if I can name it and abstract over it in a concrete and reliable way. Keep in mind that I've never used OCaml's module system. Maybe that's just a lot harder to fit into GHC as it is today, though. But I feel like the problem you're solving has already been solved by first-class modules - type classes are for something else altogether. But maybe we need a better example to argue about :-) Antoine ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
