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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
