On Fri, Jan 2, 2015 at 3:20 PM, Keean Schupke <[email protected]> wrote: >> That is a compilation error, not unsoundness. Unless Iterator requires >> Show, or the existential had an additional Show constraint, the call to show >> won't type check. > > I was wrong, it does require a type constraint like this: > > data Iterable = forall x . (Show (Value_Type x), Iterator x) => Iterable x > > Further Haskell does not allow instances to declare arbitrary associated > types like I thought, but instead you declare type-family like type-level > functions inside the instance declaration, which is why you can declare > "Show (Value_Type x)". > > However this does mean that it does not allow two instances of the same type > to declare different associated types, which is the problem I was > describing. Haskell's associated types as not really associated types in the > sense of ML's associated types in modules. > > So my original point, expressed more precisely, that having multiple > instances for a given type-class where the associated types differ is > unsound, is not affected by this.
I think we agree technically, in that I believe your point is that if we assume that instances are coherent but have incoherent instances, we get a contradiction. That's certain true, and the question is what we lose by giving up that assumption. I'm right that we don't lose decidability, and the syntax can stay exactly the same, what other problems arise? Geoffrey _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
