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
