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
