Re: [Haskell-cafe] Increasing Haskell modularity

On Friday, October 3, 2014 1:05:36 PM UTC+2, Dominique Devriese wrote:

2014-10-02 16:21 GMT+02:00 Oleg javascript:>:

...

However, given

f2 :: Show a => a -> String f2 x = let instance Show Int where show _ = "one" in show x

what should (f2 (1::Int)) return?

I haven't studied this in detail (yet :)), but can't we solve this coherence problem by requiring a bit of additional type annotations from the programmer? Specifically, I would expect the problem to go away if we require the user to explicitly state the resulting type of the "let instance" expression. The syntax could look like

let instance Show Int where show _ = "one" in show x as Show a => String

where the specification "Show a => String" would imply that the Show a instance is propagated outwards and the Show Int instance is unused. If the programmer instead wrote

let instance Show Int where show _ = "one" in show x as String

That would imply that the compiler should try to resolve the required "Show a" constraint, but I would then expect an error saying that "Show a" cannot be derived from "Show Int", because we don't apply unification to constraints (or at least, GHC doesn't, and it seems like a good idea not to).

Such an additional annotation is a bit more work for the programmer, but perhaps that might be acceptable for this indeed sorely missed feature?

FYI, I think that "Modular type classes" [1], Sec. 3.1, discusses what's morally the same point (in a slightly different context, since they start from ML modules). They end up rejecting the annotation overhead, arguing that it ends up being repeated each time you nest a local instance (which is an interesting technical point). However, they don't establish that the nesting is common enough for this to be a problem, hence that argument might just be very insightful handwaving, so I think it's certainly up for discussion. Quoting: Instead, we prefer [...] to put the decision under programmer control,

permitting either outcome [of the two above ones] at her [the programmer's] discretion. We could achieve this by insisting that the scope of a using declaration [which imports a module instance into the implicit scope] be given an explicit signature, so that in the above example the programmer would have to specify whether A.f is to be polymorphic or monomorphic. However, this approach is awkward for nested using declarations, forcing repeated specifications of the same information. Instead we propose that the using declaration be confined to an *outer *(or *top-level*) layer that consists only of module declarations, whose signatures are typically specified in any case. All core-level terms appear in the *inner *layer, where type inference proceeds without restriction, but no using clauses are allowed.

[1] Derek Dreyer, Robert Harper, Manuel M.T. Chakravarty. Modular Type Classes, POPL 2007.