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. 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. Keean. On 1 January 2015 at 22:11, Geoffrey Irving <[email protected]> wrote: > On Thu, Jan 1, 2015 at 2:04 PM, Keean Schupke <[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] > http://www.coyotos.org/mailman/listinfo/bitc-dev >
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
