On Friday, January 2, 2015, Keean Schupke <[email protected]> wrote: > I think I see how to do it, you want to type check all possible return > types. In effect the return type is the intersection type of all the > associated types of the instances. So in the case of: > > show $ valueof iterator > That is a compilation error, not unsoundness. Unless Iterator requires Show, or the existential had an additional Show constraint, the call to show won't type check.
Geoffrey > The type checker would have to prove that there is an instance of 'show' > for the associated Value_Type of the iterator at the call site of the > existential constructor. > > The problem will be if the 'show' call is in a separate compilation unit, > so that the type-checker does not know what functions may be applied to > valueof in the rest of the program. > > This is probably one form of the separate compilation issue. (and we can > probably trigger it without existential types by using polymorphic > recursion). > > Keean. > > > > Ok, it seems I misread your deref example: Value_Type is an associated > type - a type-valued field associated with the instance - rather than > something unboxed. > > On 2 January 2015 at 18:19, Keean Schupke <[email protected] > <javascript:_e(%7B%7D,'cvml','[email protected]');>> wrote: > > 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 > > data Iterable : Type where > Iterable : {X : Type} -> {Iterator X} -> (x : X) -> Iterable > > deref : Iterable -> Type > deref {X} {it} x = 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? > > The Iterable constructor takes three arguments in the formulation with > dependent types; although the first is usually erased. > > Using a pretend Haskell record syntax (because Shap does not > understand Agda syntax (yet)), > > data Iterable = Iterable { > Value_Type :: Type, -- erased > iterator :: Iterator Value_Type, > value :: Value_Type > } > > You can see that this verifies the relationship between the value and > the iterator: in order to construct this Iterable, you've had to > provide me an iterator and a value that are consistent with the value > type. > > And so yes, because you've had to give me this, you can also fish it out: > > valueof :: ((Iterable vt _ _) :: Iterable) -> vt > valueof Iterable _ _ v = v > > Now the equivalent non-polymorphic valueof does actually typecheck, > however, the onus is now on the caller. The caller must provide an > Iterable whose Value_Type is the type they expect to get back. And > they couldn't have constructed an Iterable that would cause valueof to > be unsound. > > Incidentally, vt is information you must have had anyway in order to > do this, as you can't match on types in most sane dependantly typed > languages. > > -- > William Leslie > > Notice: > Likely much of this email is, by the nature of copyright, covered > under copyright law. You absolutely MAY reproduce any part of it in > accordance with the copyright law of the nation you are reading this > in. Any attempt to DENY YOU THOSE RIGHTS would be illegal without > prior contractual agreement. > _______________________________________________ > bitc-dev mailing list > [email protected] > <javascript:_e(%7B%7D,'cvml','[email protected]');> > http://www.coyotos.org/mailman/listinfo/bitc-dev >
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
