On Thursday, January 1, 2015, Keean Schupke <[email protected]> wrote:
> It sounds like you are talking about the same thing: > > > essentially by shifting instances to the type level > > Yes, this sounds like the phantom type solution in ML. However for me the > use of associated types result in this requirement, and mix two different > things together. > > Keeping type-classes and type-families separate gives a much better > separation of concerns and avoids the need to implement this to fix the > problem because it doesn't occur in the first place. All instances of a > type-class have the same parametric type, then there is no need to lift the > instances to the type level, as they all share the same type. > Cool, I think I'm on the same page now. Thank you for the explanations! How would you deal with existential types though? If instances can have > different types, they can leak type information out of the existential > container, which seems like it would be unsound. > I'm imagining that the implementation is the same as the fully dependently typed version with implicits, namely dictionary passing. Dictionary passing seems required in the existential case even if it is avoided normally via polyinstantiation. An existential with a type constraint is then an existential with a tuple. Since the dependently typed implementation is sound, soundness of the simple system would follow as long as the map from simple to dependent is injective. A simpler way to see safety in the existential case is that if the compiler sees two instances of exists a. Iterator a => a it has no way to distinguish between these two cases: 1. There are two different a's, with two accordingly different type class instances. 2. There is one a with two different type class instances. Thus, at least in this case, it can't generate a contradiction. However, I suppose the more problematic example is exists a. ((Iterator a => a), (Iterator a => a)) where without instance coherency the type cannot be converted to exists a. Iterator a => (a,a) In the dependent case with type classes as sugar for dictionary passing, these two types are clearly different. In the nondependent case, I would expect that the phantom types would solve the problem (there would be two different phantoms floating around rather than one). Geoffrey On 1 January 2015 at 22:11, Geoffrey Irving <[email protected] > <javascript:_e(%7B%7D,'cvml','[email protected]');>> wrote: > >> On Thu, Jan 1, 2015 at 2:04 PM, Keean Schupke <[email protected] >> <javascript:_e(%7B%7D,'cvml','[email protected]');>> wrote: >> >> A system with type families as you describe is already slightly >> dependent, >> >> since the type of a function can dependent on the instance passed in. >> > >> > No, it only depends on the type of the argument. This is where >> type-families >> > differ from associated types. >> > >> > The lambda-cube has: >> > values that depend on values = functions >> > values that depend on types = type-classes >> > types that depend on types = type-families >> > types that depend on values = dependent-types >> >> I'm likely just being dense here, but I still don't see it. I claim >> that given an algorithm to decide types that assumes that instances >> are coherent, I can lift it into an algorithm that decides types >> without assuming that instances are coherent, essentially by shifting >> instances to the type level. Maybe this is what the reference to >> phantom types was referring to? >> >> Do you have a reference showing that this isn't possible? That is, a >> reference that shows that if you drop the instance coherency >> constraint, typing becomes provably undecidable? >> >> Geoffrey >> _______________________________________________ >> bitc-dev mailing list >> [email protected] >> <javascript:_e(%7B%7D,'cvml','[email protected]');> >> http://www.coyotos.org/mailman/listinfo/bitc-dev >> > >
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
