That's certainly true, but that's a separate issue of decidability, not soundness. 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. If you assume instances are coherent, this dependency can be eliminated in a nonconstructive sense. However, since the compiler doesn't have access to the dependency before it has access to the type class instances, I don't see how enforcing coherency turns an undecidable type system into a decidable one.
Geoffrey On Thu, Jan 1, 2015 at 1:44 PM, Keean Schupke <[email protected]> wrote: > My understanding is that it is a different type system, so the rules are > different. Its okay for types to depend on values in a dependant type > systems. You gain the ability to type these kind of things, but lose > decidability. > > Keean. > > > On 1 Jan 2015 01:34, "Geoffrey Irving" <[email protected]> wrote: >> >> On Wed, Dec 31, 2014 at 10:41 AM, Keean Schupke <[email protected]> wrote: >> > Here's perhaps a simpler explanation, and a slight retraction. If a type >> > class has an associated type (which we want because we would like for >> > example an iterator concept to have an associated value type) and we >> > allow >> > multiple instances per type, then we can pass values that are different >> > instances by value. If each of instances encoded as values have a >> > different >> > associated type, then passing then to a function with a type like this: >> > >> > deref :: Iterator i => i -> Value_Type i >> > >> > Then we cannot statically check this function at compile time, because >> > the >> > return type will depend on the value passed as the Iterator. >> > >> > This problem can be avoided by having type-families instead of >> > associated >> > types, separating the type functions from the type-classes, so perhaps >> > it is >> > okay to allow multiple instances for a type class providing you have >> > type-families instead of associated types. >> >> I'm trying to translate this problem into dependent types and >> dictionary passing to aid in my understanding, but the problem seems >> to go away in the translation. With dependent types, we'd write >> something like >> >> type Iterator i = struct { >> value_type : Type >> deref : i -> value_type >> } >> >> and then have functions like >> >> deref2 : (i: Type) -> (it: Iterator i) -> (x: i) -> (it.value_type) >> deref2 i it x = it.deref x >> >> This all seems perfectly fine: the unsoundness is replaced with the >> (natural) fact that deref2's type depends on its "it" parameter. Is >> this just an instances of "dependent types are much simpler to think >> about", or is there an alternate way of describing the problem that >> translates? >> >> 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
