[TYPES] A show-stopping problem for modular type classes?

[Brian Hulley]

Philip Wadler wrote:
> On Mon, Oct 12, 2009 at 7:27 AM, Brian Hulley <brianh at metamilk.com> wrote:
>> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>>
>> Brian Hulley wrote:
>>> Actually even if we go back to plain Haskell 98 and consider the
>>> original types for the functions in Data.Set we can see that none
>>> of the types would be sufficient to describe the parameter
>>> requirements in a modular setting:
>>>
>>>     data Set a = Set [a] -- example implementation
>>>
>>>     insert :: Ord a => a -> Set a -> Set a
>>>
>>>     union  :: Ord a => Set a -> Set a -> Set a
>> Over the last few days I've been thinking a bit more about this example, and although I still stand by my observation that the above code would be unsafe (i.e. type-correct but bug-friendly) in a scoped-instance context
> 
> Why do you claim this would be bug-friendly?  My understanding of how
> scoped-instance contexts work is that in the presence of a scoped
> instance one cannot export a function with a type class in its
> signature that overlaps the instance.  I think that eliminate the
> bug-friendly case.  An example that you consider bug-friendly would be
> welcome.  Yours,  -- P
> 
> 

The example I had in mind was (using layout + Haskell/ML mixed up syntax):

    module Set = struct
        data Set a = Set [a]
        val insert : Ord a => ...
        ...

    data T = T Int

    module S0 : sig val s : Set T end = struct
       instance Ord T where ...

       val s = Set.insert ...

    module S1 : sig val s : Set T end = struct
       instance Ord T where ...
       val s = Set.insert ...

    module U  : sig val u : Set T end = struct
       instance Ord T where ...

       val c : Set T = Set.union S0.s S1.s

where both S0 and S1 construct sets of more than one element using different orderings, and the binding to U.c uses (perhaps) yet another ordering to implement the merge that is part of the implementation of Set.union.

The problem is that the particular ordering used to construct a set is not reflected in the type of the set itself, and indeed the fact that Ord is used at all is not reflected in the Set type so the export of val s from S0 effectively causes the instance of Ord to travel (in its effects) outside its lexical scope without anyone knowing that this has happened.

If you meant, by the rule you gave, that a function with a type class in its signature that is exported by a library module (Set) cannot be used from within the scope of a local instance decl (e.g. within the body of S0) then this might solve the bug-friendly problem but would seem to limit the usefulness of scoped instances. For example it would no longer be possible to use any monadic library functions with a locally defined monad instance.

In section 7.1.2 of [1] there is an example (given in the language of "concepts" and "models") showing the usefulness of lexically scoped instances which I think is similar in structure to the above: there is a function taking a typeclass argument that is used in the scope of two separate instance declarations for the same type, so it seems like with scoped instances bug-friendliness and enhanced utility are two sides of the same coin.

(Btw I hadn't heard of that rule before and indeed I haven't been able to find any paper that discusses possible bug-friendliness of scoped instances or gives any examples so any pointers to literature would be welcome.)

Cheers, Brian.


[1] "A language for generic programming" by Jeremy G. Siek, Doctoral Dissertation, Indiana University, Computer Science, August 24, 2005.