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

[Brandon Moore]

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