[Haskell-cafe] Fwd: Increasing Haskell modularity

[Gesh]

On 10/2/2014 10:09 PM, Richard Eisenberg wrote:
 > 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.
Looking at what I wrote, I'm sorry for spreading confusion.

Basically, what I was trying to get at is the following:
* There are only three type-safe ways of using instances of open type
   families:
   * As a specialization of a polymorphic function
   * If the open type family is an associated type and an appropriate
     instance is in scope
   * If all possible instances are known, i.e. no more instances can be
     defined without overlapping. This is only possible when there
     exists a catchall instance. (I thought that open type families
     could overlap, but had OverlappingInstances-like semantics. In
     either case, catchall instances eliminate all possibility of
     additional instances. This also explains my point above regarding
     "open type families considered closed", in that if we had
     OverlappingInstances semantics, it would make sense that a
     declaration like
 > type family Open a
 > type instance Open Foo = Bar
 > type instance Open a = a
     would be equivalent to the declaration
 > type family Open a where
 >     Open Foo = Bar
 >     Open a   = a
     What I was suggesting was that these declarations be declared
     equivalent by fiat.)
* The above example, if `F` is taken to be a closed type family and
   the declarations are modified accordingly, shows that in the event
   that we allow local closed type family declarations, then in order
   to keep things type-safe, the local type family and the global one
   may not be considered equal. Otherwise, `unsafeCoerce` would be
   possible.

   But upon further reflection, this point is quite trivial.

Again, sorry for the confusion. I hope things are clearer now.

Gesh