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
