Forwarding to list.
---------- Forwarded message ----------
From: Antoine Latter
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_instanc... 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