[Haskell-cafe] Fwd: Increasing Haskell modularity

[Gesh hseG]

Sorry, should have used reply-list.
To clarify, under the proposal, the associated family instances would
also be locally unique, with local instances overriding global instances.

Gesh


---------- Forwarded message ----------
From: Gesh <gesh at gesh.uni.cx>
Date: Wed, Oct 1, 2014 at 5:30 PM
Subject: Re: [Haskell-cafe] Increasing Haskell modularity
To: Richard Eisenberg <eir at cis.upenn.edu>


On 10/1/2014 5:01 PM, Richard Eisenberg wrote:
>
> * I'm not sure exactly what you mean by "adopt [Oleg's] proposal".

In Section 6.1, Oleg discusses how to keep principal typing while
allowing local instances. He then suggests making this part of the
semantics of local instances.

> It seems the first part of your proposal just says
> "Haskellers can no longer expect class instance coherence."
> As such, this is a drastic change that would require all Haskell
> programs to be inspected to see if they crucially rely on coherence
No. Coherence is preserved, since you always use the unique in-scope
dictionary. What *is* lost, however, is global uniqueness, which means
that code that assumes that the same dictionary is used for the same
type across calls to functions must be modified. Arguably, that code
is semantically incorrect to begin with, but that's neither here nor
there.

> * As for associated vs. non-associated type families:

> There is essentially no difference between associated
> and non-associated type families, save concrete syntax.
> If the Haskell house were on fire and we needed to eliminate
> one of these forms, I would agree to it without much trouble,
> because the two forms are equally expressive.
>
>
> But, eliminating non-associated type families wouldn't solve

> your problem at all: while class instance incoherence causes
> wonky runtime behavior, associated type instance incoherence
> breaks the type system. If I understand your proposal correctly,
> users could implement unsafeCoerce through clever hackery around
> associated type instance incoherence. This seems to be against
> the Haskell tradition of strong typing.
To clarify my proposal: Associated type families have the added
guarantee over non-associated families that functions will be defined
that allow one to work with them. As mentioned above, typeclass
coherence is preserved under the proposal, so I see no danger of family
incoherence.

However, I'm inexperienced with these kinds of proposals, and the
concern that unsafeCoerce will be possible with this proposal is
worrying. Could you please construct a case implementing unsafeCoerce?

Thanks,
Gesh