Re: [Haskell-cafe] Fwd: Increasing Haskell modularity

On Thursday, October 2, 2014 11:30:20 AM UTC+2, Dominique Devriese wrote:

Daniel,

This is an interesting discussion and I personally also think Haskell should in time move away from global uniqueness of instances, at least as the default.

2014-10-02 10:50 GMT+02:00 Daniel Trstenjak javascript:>:

...

On Thu, Oct 02, 2014 at 12:44:25AM +0300, Gesh wrote:

...

Correct, although that's not what I said. I just said that a case could be made for saying the design of programs around global uniqueness was poorly thought out.

I think the problem is, that for some type classes global uniqueness is a very good idea and for some it might not be that relevant.

If there's e.g. a PrettyPrint type class, then one might argue, that it's a good idea to be able to change the pretty printing of a data type depending on the context.

But for a type class represeting the equality of a data type it might be more harmful then good, to be able to change it.

I think you're right that whether we want global uniqueness of instances depends on the situation. However, it doesn't just depend on the type class in question.

Consider for example the Ord type class. The fact that we sometimes want to use different orderings for the same data types is clearly evidenced by the existence of functions such as sortBy and all of the "comparing ..." stuff in Data.Ord. On the other hand, there is the fact that data types like Set crucially depend on being used with a single Ord instance for correctness.

As you suggest, a way to deal with this could be to make a data type like Data.Set carry around the Ord instance, something like this:

data Set a where SomeInternalConstructor :: Ord a => ... insert :: a -> Set a -> Set a

However, it seems a bit unfortunate to me that this extra data (the type class dictionary) would be carried around at runtime instead of it being inferred and potentially compiled out at compile time.

I wonder if a more static alternative could be to introduce some limited form of dependent types (I'm reminded of Scala's value-dependent types) to index the Data.Set data type with the Ord instance that it should be used with, something like:

data Set a (instOrdA :: Ord a) where ... insert :: (ordA :: Ord a, ordA ~v instOrdA) => a -> Set a instOrdA -> Set a instOrdA

In such code, the constraint "ordA ~v instOrdA" would require that the two instances are equal in some intentional and decidably checkable way (i.e. no automatic unfolding of recursive definitions and such). Perhaps it's not even needed to require the "(ordA :: Ord a, ordA ~v instOrdA) =>" contraint, but the compiler could somehow just take the instance from the "Set a instOrdA" type and make it available for type class resolution in the body of insert?

I also like this design, and it's been discussed before in the same context (http://lists.seas.upenn.edu/pipermail/types-list/2009/001412.html). I know a few ways to allow checking the constraints, but I'm not sure whether any of these fits with Haskell: - using definitional equality like in dependent types, or some encoding thereof (e.g. with empty types, as when encoding Peano numbers in the Haskell type system) - using singleton types, as in Scala (not really powerful, and does not fit with Haskell). However, Scala's relevant feature arise from making ML modules first-class and unifying them with objects. For Haskell, I'd leave out objects and get to... - use some variant of ML modules, where the modules are easier to compare because they're second-class (I wonder whether that means using singleton kinds where Scala uses singleton types). Given that the upcoming Backpack descends from a form of ML modules, this might be more relevant than is currently apparent (to me at least). Anyway, I agree with Gesh that at some point, Haskell should deprecate

global uniqueness of type class instances, but we should first explore alternatives for modeling data types like Set that currently depend on it. There's still quite some room for research here in my opinion.