> 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 Keean. On 1 January 2015 at 21:56, Geoffrey Irving <[email protected]> wrote: > 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 >
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
