Why wouldn't it be a link-time failure (as opposed to a compile-time failure)? Individually, the modules are fine, but it's linking them together that's the problem. Or are we not treating individual modules as units of separate compilation?
This reminds me a bit of how Agda encodes type classes using instance arguments: if there's exactly one term of the required type in scope at the use, it's taken as the argument; otherwise, there is a compile error. On Wed, Jul 24, 2013 at 5:19 AM, Jonathan S. Shapiro <[email protected]>wrote: > 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 > > -- Alex R
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
