Bulat Ziganshin wrote:
Subtyping introduced in very natural (at least for OOP souls) way. We may, for example, have functions:
doit :: MemBuf -> IO Int hRequestBuf :: MemoryStream -> IO Int hTell :: SeekableStream -> IO Integral
and call doit -> hRequestBuf -> hTell and then return result, and all will work fine because MemBuf is subclass of MemoryStream that is subclass of SeekableStream while Int is subclass of Integral. We can describe whole type hierarchy as having types at leafs and type classes at internal nodes
As an example that clears my idea the following is function signatures from one my module:
copyStream :: (BlockStream h1, BlockStream h2, Integral size) => h1 -> h2 -> size -> IO () copyToMemoryStream :: (BlockStream file, MemoryStream mem, Integral size) => file -> mem -> size -> IO () copyFromMemoryStream :: (MemoryStream mem, BlockStream file, Integral size) => mem -> file -> size -> IO () saveToFile :: (MemoryStream h) => h -> FilePath -> IO () readFromFile :: FilePath -> IO MemBuf
As one can see, there is only one function that don't uses classes, and another one that can't be written using this syntax, another 3 is just created for using this proposal. I don't say that such ratio is typical, but at least i have a large number of polymorphic functions in my library and found the way to simplify most of their signatures:
copyStream :: BlockStream* -> BlockStream** -> Integral -> IO () copyToMemoryStream :: BlockStream -> MemoryStream -> Integral -> IO () copyFromMemoryStream :: MemoryStream -> BlockStream -> Integral -> IO () saveToFile :: MemoryStream -> FilePath -> IO () readFromFile :: FilePath -> IO MemBuf
i think that second block of signatures is an order of magnitude more readable
These sorts of signatures seem to be the only ones where some way of using a class as a type would be useful - when single parameter type classes constrain variables which only occur once, and the variables are only constrained by a single class. This could be handled with existential wrappers, except that the wrapping is annoying, and probably interferes with optimizing when a concrete type is known. Instead, a few changes to type synonyms handle Bulat's cases. With the proper interpretation, type synonyms like type ABlockStream = BlockStream b => b type AMemoryStream = MemoryStream m => m support some of Bulat's signatures like copyStream :: ABlockStream -> ABlockStream -> Integer -> IO () saveToFile :: AMemoryStream -> FilePath -> IO () This requires two changes to the interpretation of type synonyms 1) Free variables in the definition of the type synonym are allowed, and become fresh (wobbly) variables when the synonym is applied 2) Class constraints in the definition of a type synonym float up to the closest binding of a constrained type. Now, more discussion, examples, and comparisons to the Haskell 98 standard type synonyms and the GHC (6.4.1) implementation. 1) Free variables expand to (wobbly) fresh variables. That is, each time a type synonym with a free variable is used, all the free variables are given fresh names, and then allowed to unify with other types during type checking. This allows the synonyms above to introduce a new type variable, which can carry the class constraint. for example, with type AnAuto = a -> a these definitions are legal op1 :: AnAuto op1 = id op2 :: AnAuto -> AnAuto -> (Int, Bool) op2 f g = (f 1, g True) op3 :: AnAuto -> AnAuto -> AnAuto op3 f g = g . f and result in types op1 :: forall x . x -> x op2 :: (Int->Int) -> (Bool->Bool) -> (Int, Bool) op3 :: forall y . (y -> y) -> (y -> y) -> (y -> y) Implicitly freshening free variables in type synonyms seems very much in the spirit of implicitly quantifying variables in type signatures, and the treatment of names in hygienic macros (the GHC user's guide says " Type synonyms are like macros at the type level"). Standards: Free variables are not allowed by Haskell 98, or GHC. Perhaps there is an explicit quantifier corresponding to this behavior, but I don't see how to make it properly a part of the type system, rather than just something that happens around synonym expansion. What might be meant by something like [fresh a . a -> a]? 2) A class constraint in a type synonym floats up to the nearest binding occurrence of any of the constrained types. This allows the type synonyms above to put a class constraint on the new variable they introduce (which is bound at the top level by the implicit forall). This extension would also allow parameterized type synonyms to add constraints to their arguments. (this would need some changes to error messages, like "cannot satisfy class constraint XX arising from application of type synonym Showable at nn:xx-yy) Type synonyms that add extra constraints to their argument can provide the syntax I suggested earlier to Bulat, where each use of a class-as-type is tagged with a variable, to indicate sharing. type TagMonad a = Monad a => a type TagFunctor a = Functor a => a sequence :: [TagMonad m a] -> TagMonad m [a] sequenceLift :: [TagMonad m a] -> TagMonad r [a] confuse :: (a -> b) -> (TagMonad m) [a] -> (TagFunctor m) b This nearly subsumes Brian Hulley's proposal to allow a list of curried class contexts in braces in front of types, completely if you don't mind declaring a new synonym for each set. Standards: GHC 6.4.1 requires that a class constraint mention some variable bound by a forall in the synonym, Haskell 98 doesn't allow quantifiers in synonyms at all. Brandon