[Haskell-cafe] Increasing Haskell modularity

[Paolo Giarrusso]

On Friday, October 3, 2014 1:05:36 PM UTC+2, Dominique Devriese wrote:
>
> 2014-10-02 16:21 GMT+02:00 Oleg <ol... at okmij.org <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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20141107/69dc68b0/attachment.html>