Arie Peterson wrote:
Hello Brandon,
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.
I find those free variables a bit scary. It is not clear to me what it means for a value to have type 'AnAuto'. I like to think about type synonyms as only that, synonyms - so you can always substitute the definition for an occurrence.
Those free variables are just necessary to match the proposed syntax exactly. The type variables could be provided as parameters - type AMemoryStream m = MemoryStream m => m writeToFile :: AMemoryStream m -> FilePath -> IO () type Stream s = Stream s => s copyStream :: Stream s1 -> Stream s2 -> Integer -> IO () That said, making fresh unification variables seems like a reasonable interpretation of free variables in a type synonym, the converse of the renaming you can see in type Cont x = forall r . (x -> r) -> r where the forall doesn't capture the x, even if you use the synonym in return :: r -> Cont r
How does your proposal compare to introducing existential types proper? As in
type ABlockStream = exists b. BlockStream b => b
. This is a known extension, supported partly by jhc and fully by ehc. It seems to be exactly what you need for
copyStream :: ABlockStream -> ABlockStream -> Integer -> IO ()
I don't understand the difference very well. I'm proposing to allow a bit of type inference to further resolve these variables when the type synonym is expanded. A function taking an existential type must work for any type in that existential package. A fresh variable could resolve a bit more, if it turns out that those two BlockStream types must be the same, or the parameter actually has to be a function type. I think mostly it's like a kind of partial type signature, but I'm wondering if there's an interpretation as a logical quantifier. Brandon