[Haskell-cafe] Increasing Haskell modularity

[oleg at okmij.org]

The issue with local instances is very complicated one. First, they
are sorely missed. However, they present quite a problem. Let us
assume they are implemented and consider the following function

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

I think we all agree (f1 1) should evaluate to "one". 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? One answer is that it should still
return "one" -- that is, local instances should sort of form a
closure (like local variables in the real closure). That is a good
answer, but may lead to unpleasant surprises because the fact of the
closure is not at all reflected in the type of the function. Consider

data T = T
f3 :: Show a => a -> String
f3 x = 
  let instance Show T where show _ = "T"
  in show x

and take the closure semantics. The type says that to make (f3 T)
well-typed, there has to be an instance Show T in scope. The user of
f3 has no way to know of the private local instance that is closed
over (short of examining the source code). Since the user knows there
is no global instance T, the user attempts to define in. The user will
be quite surprised to discover that (f3 T) is well-typed but their
global instance Show T has no effect.

Let us assume the opposite of the closure semantics -- local instances
are not closed. So, local instances should behave sort of dynamically
scoped variables (which are not captured in closures). Therefore, 
(f2 (1::Int)) should return "1". Such a choice is also
problematic. Suppose GHC, seeing our call to f2, notices that the
polymorphic f2 is called at type Int and decides, to save time on
indirect dictionary calls, to specialize f2 to the type Int. So, GHC
will generate a specialized instance of f2:

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

and we have already decided that (f2_Int 1), should return "one" rather than
"1" (since f2_Int looks just like f1). Previously, specialization of a
function was easy to understand: GHC may, at will, create a copy of a
polymorphic function and instantiate it at a specific type. Then all
calls to the polymorphic function at that specific type are replaced
with the calls to the specialized function. The user can even do such
a specialization themselves. With unclosed local instances, such a
specialization changes the program behavior. We have to complicate the
matters. 

Further, what should (f4 (1::Int)) return?

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


Stefan Kaes, the person who introduced ``parametric overloading''
(type classes, in modern term) chose the ``closure semantics''. His
system and prototype implementation had only local instances (and even
local type classes).

        http://okmij.org/ftp/Computation/typeclass.html#Kaes

Perhaps the most comprehensive treatment of local instances is the old
paper

        D. Duggan and J. Ophel. Open and closed scopes for constrained
        genericity (PDF). Theoretical Computer Science, 275, 215-258, 2002.
        http://dl.acm.org/citation.cfm?id=570578

They propose a method to have both closure and non-closure semantics, 
differentiating based on so-called open and closed types.


Our HW 2004 paper with Chung-chieh Shan proposed a way to elide the
problem by restricting the local instances in such a way that the
problem never arises. The `reflection' facility was used to implement
such local instances. The idea was that local instances can be thought
of as ordinary global instances; however, the scope of the type in
their head is restricted. That is, rather than make the instances local
we make local the type for which they are defined (or one of the
types, for multi-parameter type classes). Local types can be emulated
via first-class polymorphism. (BTW, if one can leave with
unsafeCoerce, local instances can be much more efficiently
implemented.)

Gesh wrote:
> * Give up on non-associated open type families.  This I have
> researched less well, but it seems to me that these have no use
> case. Since one can make whatever instances one wishes for these type
> families, one can't do anything useful with values of their instances.

On the contrary, we found them very useful in defining interpreters
that provide their own interpretation of not only primitives but also
of types. 
        http://okmij.org/ftp/gengo/NASSLLI10/index.html
See, for example,
        http://okmij.org/ftp/gengo/NASSLLI10/Lambda.hs
for partial evaluation and
        http://okmij.org/ftp/gengo/NASSLLI10/CFG.hs

In the latter case, extensibility is particularly important as we do
want to add further syntactic categories and their semantic
interpretations.