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
