Forwarding to list.
---------- Forwarded message ---------- From: Antoine Latter <aslat...@gmail.com> Date: Sat, Oct 16, 2010 at 9:47 AM Subject: Re: Local evidence and type class instances To: Max Bolingbroke <batterseapo...@hotmail.com> 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 > """ I think UHC has something like that: http://www.cs.uu.nl/wiki/bin/view/Ehc/UhcUserDocumentation#3_8_Local_instances One thing that worries me is that the local instance only applies to type-expressions that consume constraints - if the constraint was satisfied before the local constraint was introduced then the local constraint would not apply. Am I making sense? I don't have much of a background in type-theory, so I may not be using the correct language, but I'm having trouble seeing how it wouldn't be confusing. What I'm thinking is that the following two functions would have different effect: f n = Set.insert n and: f' (n::Int) = Set.insert n When called like so: updateSet (n::Int) s = let n' = someComputation n s in f n' s where instance Ord s ... 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. Type-classes are engineered to be global in scope. It's nice that from a GHC type-checking perspective they need not be, but changing them to be non-global is also an engineering and design problem. Antoine > > Not only would this prevent instances from "leaking" into all > importing modules, but you could refer to *lexically scoped variables* > in the type class instance. This would let programmers implement e.g. > implicit configurations in the style of Kieslyov and Shan > (http://okmij.org/ftp/Haskell/types.html#Prepose) without any mad > hackery to tunnel pointers through the type system. > > Of course, it could lead to problems. For example: > > """ > newtype MyInt = MyInt { unMyInt :: Int } > > f :: [Int] -> S.Set Int > f xs = S.map unMyInt $ S.toList (map MyInt xs) > where > instance Ord MyInt where > x `compare` y = unMyInt x `compare` unMyInt y > > g :: [Int] -> S.Set Int > g xs = S.map unMyInt $ S.toList (map MyInt xs) > where > instance Ord MyInt where > x `compare` y = unMyInt y `compare` unMyInt x > > main = do > let s1 = f [1, 2] > s2 = g [1, 2] > print $ s1 == s2 -- prints False! > print $ S.toList s1 == s2 -- prints True! > """ > > I don't think this is a big problem. It would be up to the users of > this extension to do the Right Thing. > > As Kieslyov and Shan point out, this extension also kills the > principal types property - but so do GADTs. Just add more type > signatures! > > Are there big theoretical problems with this extension, or is it just > a lack of engineering effort that has prevented its implementation? > > Max > _______________________________________________ > Glasgow-haskell-users mailing list > Glasgow-haskell-users@haskell.org > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users > _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users