[Haskell-cafe] Fwd: Increasing Haskell modularity

[Miguel Mitrofanov]

How can we merge two Sets if they carry different Ord dictionaries?

02.10.2014, 03:51, "Richard Eisenberg" <eir at cis.upenn.edu>:
> Thanks, Gesh, for the email below and the previous one, spelling out the distinction between coherence and global uniqueness. I had been conflating coherence and global uniqueness (as it seems others have been), and drawing this out is helpful.
>
> Though I can't yet say I'm in support, exactly, I'm less vehemently against this idea than I was this morning. In particular, I actually really like the idea of local class instances, which have occurred to me before but which I've never considered seriously.
>
> Unfortunately, this all breaks apart horribly when thinking about type instances. Global uniqueness, not just coherence, is needed for type instances:
>>  type family F a b
>>  type instance F a b = b
>>
>>  oops :: F a b -> b
>>  oops = id
>>
>>  unsafeCoerce :: a -> b
>>  unsafeCoerce = let type instance F a b = a in
>>                 oops
>
> The problem is that a type instance introduces a type equality. Haskell is capable of passing type equality evidence around, so equalities can escape their scope, if the programmer wants to do so. Thus, there can never be a situation where some type (in this case `F a b`) is equal to one thing in one context and an incompatible thing in a different context, anywhere in the same program. I've written my example above with non-associated types, but the same thing can be written with associated types (and more syntactic overhead). I can't currently imagine a type-safe system that did not require global uniqueness for type instances.
>
> For what it's worth, I think I can agree that types like `Set` should carry around the relevant `Ord` dictionary. Global uniqueness of class instances is already threatened by all manner of extensions; we've just been much more careful about global uniqueness of type instances.
>
> Richard
>
> On Oct 1, 2014, at 6:05 PM, Gesh <gesh at gesh.uni.cx> wrote:
>>  On 10/1/2014 11:42 PM, Bardur Arantsson wrote:
>>>  (I say "proposal"... this needs some serious fleshing out and a
>>>  semi-formal specification for instance resolution rules &c before it
>>>  becomes a proposal. Just "Look at Oleg's paper" is not good enough.)
>>  I see I came off unclearly. Please allow me to remedy that.
>>
>>  My reference to Oleg's paper was badly framed. What I meant to say was
>>  more along the following lines:
>>  Oleg discussed adding local typeclass instances in his reflection paper.
>>  For some reason, his proposal wasn't taken. (Does anyone know why?)
>>  I'd like to suggest something along similar lines:
>>  Allow instances in let-expressions and where-clauses. These instances
>>  shadow other instances with the same parameter list.
>>  Similarly, instances defined in modules shadow imported instances.
>>
>>  Thus, in the following program:
>>>  module Foo where
>>>  import Bar (Baz) -- Where Bar defines instance Show (Baz a)
>>>  instance Show (Baz a) where -- shadows the imported instance
>>>  foo = let instance Show (Baz a) where -- shadows the instance defined
>>>        in ...              -- in where below, just like other bindings
>>>    where instance Show (Baz a) -- shadows the module-global instance
>>>          instance Show (Baz Quz) -- only allowed with
>>>          -- OverlappingInstances, isn't shadowed by any of the other
>>>          -- instances in this example.
>>  In this example, the instances for Baz have the following scopes:
>>  * From Bar: Nowhere, as it is immediately shadowed.
>>  * From Foo: Within all top-level declarations besides foo, as foo's
>>             where clause shadows it.
>>  * From the where clause: Within the where clause. The instance for
>>                          Baz Quz is also visible within the let
>>                          expression, as it is not shadowed by it.
>>  * From the let expression: Within the let expression.
>>
>>  Basically all I'm doing is applying regular name resolution semantics
>>  to instances with the same parameter lists.
>>
>>  I hope this helps clarify things. If not, please tell me what needs to
>>  be done to fully clarify this.
>>
>>  Gesh
>>  _______________________________________________
>>  Haskell-Cafe mailing list
>>  Haskell-Cafe at haskell.org
>>  http://www.haskell.org/mailman/listinfo/haskell-cafe
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe