Hello Lennart, Sunday, March 19, 2006, 4:05:03 AM, you wrote: LA> I have to agree with Manuel. I write a lot of Haskell code. LA> People even pay me to do it. I usually stay with Haskell-98, when i wrote application code, i also don't used extensions very much, i even don't used Haskell-98 very much and afair don't defined any type classes at all but when i gone to writing libraries, that can be used by everyone, type classes and requirement in even more extensions is what i need permanently. in particular, i try to write library so what any conception (stream, Binary, reference, array) can be used in any monad and that immediately leads me to using MPTC+FD. moreover, problems with resolving class overloading and other deficiencies of current unofficial Hugs/GHC standard are permanently strikes me so, from my point of view, we should leave MPTC+FD+any well-specified extensions in resolution of overlapping classes. but these should be seen only as shortcuts for the new type-calculation functions, like the old-style "data" definitions now seen as shortcuts for GADT ones just some examples how this can look: i had a class which defines "default" reference type for monads: class Ref m r | m->r where newRef :: a -> m (r a) readRef :: r a -> m a writeRef :: r a -> a -> m () instance Ref IO IORef where ... instance Ref (ST s) (STRef s) where ... this class allows to write monad-independent code, for example: doit = do x <- newRef 0 a <- readRef x writeRef x (a+1) readRef x can be runned in IO or ST monads, or in any monad derived from IO/ST (with appropriate instance Ref definitions). As you can see, even such small example require using FDs. That's all great but not flexible. That we required is a real functions on type values. In ideal, types should become first-time values, compile-type computations should be allowed (what resembles me Template Haskell), and computed types should be allowed to used in any place where current Haskell allows type literals. moreover, runtime-computed types can be used for dynamic/generic programming, but that is beyond of our current theme. really, Haskell already has functions on types: type Id a = a type Two a = (a,a) and so on. but these definitions don't have full computational (Turing) power, can't contain several sentences, can't be split among different modules/places and so on, so on. on the other side, class definitions are our most powerful type functions, but has very different syntax and semantic model compared to plain functions, plus had some additional duties (declaring a family of functions) how about adding to type functions the full power of ordinal functions? first, data/newtype declares new type constructor on its left part in the same way as it defines new data constructors on its right part: data List a = Nil | Cons a (List a) defines Nil and Cons data constructors and List type constructor. Together all data constructors defined in program plus primitive types (Int, Char...) defines a full set of types that can be constructed/analyzed by type construction functions. so, we should not only allow to construct new more complex types on the right side of type function, but also allow to analyze complex types on the left side of function definition! : type Element (List a) = a Element (Array i e) = e Element (UArray i e) | Unboxed e = e cute? i love it :) i also used pattern guard here, it's a partial replacement of Prolog's backtracking mechanism. of course, to match power of type classes, we should allow to split these definitions among the whole module and even among the many modules. library type function should be allowed to be extended in application modules and application definitions should have a priority over library ones this will allow to rewrite my Ref class as: type Ref IO = IORef Ref (ST s) = STRef s Next problem is declaring types (to be exact, kinds) of type functions. currently, kinds are defined only in terms of arity: type ReturnInt (m :: * -> *) = m Int but what we really want is to declare that `m` is Monad here: type ReturnInt (m :: Monad) = m Int or type ReturnInt :: Monad -> * type ReturnInt m = m Int i also propose to show kind arity by using just "**", "***" instead of current "*->*", "*->*->*". the above definition can be extended in user module by: type ReturnInt (ST s) = Int but not with type ReturnInt Int = IO because last definition break types for both left and right sides having all this in mind, we can break class definitions into the lower-level pieces. say, class Monad m where return :: a -> m a fail :: String -> m a instance Monad IO where return = returnIO fail = failIO translates into: type Monad :: ** -> (a -> m a, String -> m a) type Monad IO = (returnIO, failIO) i.e. Monad is function that translates '**' types into the tuple containing several functions. well, translation is not ideal, but at least it seems promising next, my Ref class is a Monad->Reference function (what is established by FD used), so: type Ref :: (Monad m, r :: **) => m -> (r, a -> m (r a), r a -> m a, r a -> a -> m ()) type Ref IO = (IORef, newIORef, readIORef, writeIORef) many MPTC declarations is not functions, but relations. That makes programmer's life easier, but compilation harder and returns to us in form of strange compiler behavior and numerous prohibitions. i suggest see such classes as the types->functions definitions. for example: class (HasBounds a, Monad m) => MArray a e m where unsafeRead :: Ix i => a i e -> Int -> m e unsafeWrite :: Ix i => a i e -> Int -> e -> m () instance MArray IOArray e IO where ... instance (Unboxed e) => MArray IOUArray e IO where ... can be translated to: type MArray :: (HasBounds a, Monad m, e :: *) => a -> e -> m -> (UnsafeRead a e m, UnsafeWrite a e m) type UnsafeRead a e m = Ix i => a i e -> Int -> m e type UnsafeWrite a e m = Ix i => a i e -> Int -> e -> m () type MArray IOArray e IO = (arrRead, arrWrite) MArray IOUArray e IO | Unboxed e = (arrReadUnboxed, arrWriteUnboxed) well, i don't catched all the problems: 1) how these definitions allow us to select proper "instance" for operations like readRef? i don't know, my examples even don't define names of functions. well, i can imagine something like this: type ReadRef (IORef a) (IO a) = readIORef ReadRef (STRef s1 a) (ST s2 a) | s1==s2 = readSTRef what maps types of arguments/result of readRef invocation to proper function body, but that's too verbose and don't solves the problems that solves FDs 2) i don't proposed good syntax to rewriting classes in terms of type functions. i think that using structures with named fields should be great here and will closely resembles ML's functors i propose to start with type functions, allow type declarations for type functions including using classes as "types of types" and allow to mix types and ordinal values in type functions arguments/results i don't see any good alternative to using prolog-like relations to declare classes: type Ref :: (Monad m, r :: **) => m -> r -> NewRef m r -> ReadRef m r -> WriteRef m r -> () type NewRef m r = forall a . a -> m (r a) type ReadRef m r = forall a . r a -> m a type WriteRef m r = forall a . r a -> a -> m () type Ref IO IORef newIORef readIORef writeIORef = () Ref (ST s) (STRef s) newSTRef readSTRef writeSTRef = () but this definition again loses the FD :( -- Best regards, Bulat mailto:Bulat.Ziganshin@gmail.com