[Haskell-cafe] Fwd: Increasing Haskell modularity

[Richard Eisenberg]

On Oct 2, 2014, at 2:37 PM, Gesh <gesh at gesh.uni.cx> wrote:

> On 10/2/2014 2:50 AM, Richard Eisenberg wrote:
> >> type family F a b
> >> type instance F a b = b
> >>
> >> oops :: F a b -> b
> >> oops = id
> 
> 
> Several things can be said about the above code. First and foremost,
> it seems unsafe to allow oops to even typecheck today. Suppose `F` did
> not have a catchall instance. Then the type `F a b` is morally
> equivalent to `forall a. a`, because we could create any instance we
> wished for `F`. Therefore, I would suggest that regardless of my
> original proposal being accepted, we only allow open type families in
> type signatures where they are either morally equivalent to closed
> type families (by having catchall instances) or where they appear as
> restrictions on more polymorphic values (such as
> `id :: F a b -> F a b`). Associated types would also be permitted if
> an instance of their typeclass were in scope.
> 

I'm sorry, but I don't understand the paragraph above at all. You say below that "open type families with catchall instances [such as F] are morally equivalent to closed type families" and you say "we only allow open type families in type signatures where there are morally equivalent to closed type families". So it seems `oops` is OK. And I don't know what you're getting at by "restrictions on more polymorphic values".

Incidentally, as type family instances can *never* overlap, a type family with a catchall instance must have only that one instance.

> Second, as hinted above, open type families with catchall instances
> are morally equivalent to a closed type families, since no other
> instances can be added to them without overlapping with the catchall
> instance. Therefore, I also suggest that open type families with
> catchall clauses be considered closed.

What does your last sentence mean? What do you mean by a type family that is considered closed?

> 
> Finally, this case serves as an excellent example to show that if and
> when we add support for local closed type families, we must consider
> the local type family distinct from the global one.

But I don't have a local type family. I have a local type family instance. How can one instance be seen as distinct from another?

> In particular, one
> won't be able to pass instances of the local families to functions
> expecting the global family without compromising type safety.

Unlike class instances, type family instances do not form dictionaries and are not passed around. Given that fact, I'm not sure what you mean here.

> 
> With the proposal from my first point, we outlaw `oops`, even with
> associated types, and thereby regain type safety.
> 
> Any other problems?

Yes. See above. :)

Richard

> 
> Gesh