So first, all of what Wren says is correct. But second, the original
example would be impossible, because the two bindings of Ord U presumably
would be in the same assembly, and colliding bindings within an assembly
would cause a compile time failure. In BitC, you could introduce two
instances at the same type with both named, but only one of them can be a
candidate for automatic instance resolution. Thus, to abuse the Haskell
syntax from the original example:
$ cat B.hs
...
Upwards = instance Ord U where
compare X X = EQ
compare X Y = LT
compare Y X = GT
compare Y Y = EQ
open Upwards -- makes Upwards a candidate for automatic resolution
$ cat C.hs
...
Downwards = instance Ord U where
compare X X = EQ
compare X Y = GT
compare Y X = LT
compare Y Y = EQ
-- open Downwards -- collides with Upwards, would cause a compile failure
But with these two instance definitions, one could write something like:
let insertDescending = using Downwards
in insert
in ...
where the intent that "using" is providing an explicit lexically scoped
override of the type class constraint resolution (cruddy syntax, not
defending it). Note that insertDescending isn't the same procedure as
insert after concretization, and doesn't have the same type signature:
insert :: (Ord U := Upwards) => a -> Set a d -> Set a d
insertDownwards :: (Ord U := Downwards) => a -> Set a d -> Set a d
Also note that we don't need to show the instance resolution in the type
signature when it is the default.
On Tue, Jul 23, 2013 at 8:36 PM, wren ng thornton <[email protected]> wrote:
> On 7/23/13 3:25 PM, Alex Rozenshteyn wrote:
> > I don't see how this would avoid Haskell's problem with orphan instances
> > (as explained here: http://stackoverflow.com/a/12744568/52310)
> >
> > Would it force you to export the specialized insert functions with a less
> > eagerly unified type signature? For example:
> >
> > ins :: (U ~ a, Ord a) => a -> Set a -> Set a
>
> The issue isn't delaying the unification U ~ a, it's making explicit the
> instantiation of the Ord U constraint with either B._ or C._
>
> Thus, as suggested by the GADT approach to avoiding the problem, the
> solution is to make the type explicitly capture the dictionary by using a
> dependent kind like:
>
> Set :: (a::*) -> Ord a -> *
>
> where Haskell, unfortunately, makes the second argument to Set implicit.
> Done this way we'd have the more accurate type:
>
> insert :: (d :: Ord a) => a -> Set a d -> Set a d
>
> which gives rise to the types:
>
> ins :: U -> Set U B._ -> Set U B._
> ins' :: U -> Set U C._ -> Set U C._
>
> And it's the failure of the constraint (B._ ~ C._) which means we can't
> intermingle uses of ins and ins'.
>
> Using Shap's approach instead of the dependent kind approach, we'd have
> the types:
>
> insert :: (Ord a) => a -> Set a -> Set a
>
> ins :: (Ord U := B._) => U -> Set U -> Set U
> ins' :: (Ord U := C._) => U -> Set U -> Set U
>
> where I'm using (:=) to mean the rhs is the chosen solution to the lhs.
> Again, attempts to intermingle ins and ins' will lead to a constraint (B._
> ~ C._) which can't be resolved.
>
> --
> Live well,
> ~wren
>
> _______________________________________________
> bitc-dev mailing list
> [email protected]
> http://www.coyotos.org/mailman/listinfo/bitc-dev
>
>
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
