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 <daniel.t...@gmail.com>:
> 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.