The thought was more about associated types and existentials. You can fix instances by lifting them to the type level, but how does that help:
data Iterable = Iterable (forall x . Iterator x => x) valueof :: Iterable -> t? valueof (Iterable x) = deref x How do we get the type of t, or more to the point we should not be able to get the type of 't' out of the container, but deref x returning the associated 'value type' would break this? If we could even represent this type which will be unknown at compile time. If we allow passing the iterator in as an implicit: valueof :: Iterator t? -> Iterable -> t.ValueType valueof i (Iterable x) = i.deref x However this would require the passed iterator to match the value type of the iterator inside the existential, which of course we cannot know, so if the type system allows this it is unsound, as as runtime it will use the (possibly) incorrect dictionary on the encapsulated iterator. Am I missing something about how this would be solved with dependent types? Keean. On 1 Jan 2015 23:22, "Geoffrey Irving" <[email protected]> wrote: > 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]> 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 > >
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
