At Fri, 17 Jun 2011 13:21:41 +0000, Simon Peyton-Jones wrote:
Concerning "1. mutual dependencies" I believe that equality superclasses provide the desired expressiveness. The code may not look quite as nice, but equality superclasses (unlike fundeps) will play nicely with GADTs, type families, etc. Do you agree?
By equality superclasses, do you just mean being able to say "a ~ b" in a class context? If so, that is basically what you get by enabling fundeps and defining a class such as: class AssertEq a b | a -> b, b -> a instance AssertEq a a Unless I'm missing something, that is not sufficient to do a lot of things I would like to do, as those things require both OverlappingInstances and FunctionalDependencies (as well as UndecidableInstances). A good test would be whether superclasses let you eliminate N^2 mtl instances and do something equivalent to: instance (Monad m) => MonadState s (StateT s m) where get = StateT $ \s -> return (s, s) put s = StateT $ \_ -> return ((), s) instance (Monad (t m), MonadTrans t, MonadState s m) => MonadState s (t m) where get = lift get put = lift . put Superclass equality is crucial for type families, since you can't mention a class's own type function in its head, but are there other things they allow you do to?
Concerning "2. combination with overlapping instances", you say "The solution has been described already in the HList paper: provide something the typeOf at the type level. That is, assume a type function "TypeOf :: * -> TYPEREP".
...
Incidentally Pedro's new "deriving Generic" stuff does derive a kind of type-level type representation for types, I think. It's more or less as described in their paper. http://www.dreixel.net/research/pdf/gdmh_nocolor.pdf
I'm very excited about this new Representable class and have just started playing with it, so it is too early for me to say for sure. However, my initial impression is that this is going to make me want OverlappingInstances even more because of all the cool things you can do with recursive algorithms over the Rep types... An initial issue I'm running into (and again, this is preliminary, maybe I'll figure out a way without OverlappingInstances) is in implementing a function to serialize Generic data types to JSON. If the Haskell data type has selectors (i.e., is a record), then I would like to serialize/unserialize the type as a JSON object, where the names of the selectors are the JSON field names. If the Haskell data type does not have selectors, then I would like to serialize it as a JSON array. Generic deriving gives me the conIsRecord function, but this is at the value level, and I want to do something different at the type level. For a record, I need a list of (String, Value) pairs, while for a non-record, I need a list of Values. This leads me to write code such as the following: class JSON1 a r | a -> r toJSON1 :: a -> r instance (JSON a) => JSON1 (S1 NoSelector (K1 c a)) [Value] where toJSON1 (M1 (K1 a)) = [toJSON a] instance (Selector x, JSON a) => JSON1 (S1 x (K1 c a)) [(String, Value)] where toJSON1 s@(M1 (K1 a)) = [(nameOf s undefined, toJSON a)] where nameOf :: S1 c f p -> c -> String nameOf _ c -> selName c The key piece of magic I need here (and in so many other places) is to be able to do one thing at the type level if x is a particular type (e.g., NoSelector) or sometimes one of a small number of types, and to do something else if x is any other type. Closed type families might do it. One question I should think about is whether a combination of open type families with safe dynamic loading (if this is possible) and closed type families would cover everything I need. You'd need to be able to do things like: -- Type-level if-then-else closed type family IfEq :: * -> * -> * -> * -> * type instance IfEq a b c d = d type instance IfEq a a c d = c You would also need to be able to dangle closed type families off of open ones. (I.e., "type instance Foo ProxyType = MyClosedTypeFamily") I also can't quite figure out how to pass around ad-hoc polymorphic functions the way you can with proxy types and a class such as: class Function f a b | f a -> b where funcall :: f -> a -> b David