[Haskell-cafe] Fwd: Increasing Haskell modularity

[Richard Eisenberg]

On Oct 4, 2014, at 4:27 PM, Gesh <gesh at gesh.uni.cx> wrote:

> * 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.

As far as I know, all uses of type families are (in 7.8) type-safe. I assume you mean "there are only three ways of using instances of open type families." Also, just to make the point clear: an open type family with a catchall instance *must* have only that one instance. For exactly the reasons I've been describing in this thread, *any* overlap among type family instances puts the type system in jeopardy.

As a counter-example to your claim above about the allowable uses of open type families:

> type family SwapIntBool a
> type instance SwapIntBool Int  = Bool
> type instance SwapIntBool Bool = Int
> 
> data G1 a where
>   MkG1Int  :: G1 Int
>   MkG1Bool :: G1 Bool
> 
> swapIntBool :: G1 a -> G1 (SwapIntBool a)
> swapIntBool MkG1Int  = MkG1Bool
> swapIntBool MkG1Bool = MkG1Int

This example may be contrived, but it follows the well-established pattern of using type families in concert with GADTs. I'll admit that it may seem that the type family could be closed, but it's also conceivable that the author of this code wants to allow `SwapIntBool` to be able to work with as-yet-unwritten types, in perhaps a GADT similar to G1 but with more constructors.

> * 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.

If by that, you mean that this is just a simple case of shadowing, then I agree. It still doesn't address local type instances, which seem at issue here.

(For what it's worth, local closed type families would be great. In fact, all manner of local type-level definitions would be nice... except instances!)

Richard