[Haskell-cafe] type synonym liberalization (was "class []" proposal)

[Brandon Moore]

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