[Haskell-cafe] Fwd: Increasing Haskell modularity

[Paolo Giarrusso]

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... at gmail.com 
> <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.
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20141107/32413a1f/attachment.html>