I disagree, valueof is the constrained function, once it has returned a value you are free to pass that value to any function.
Keean. On 2 January 2015 at 17:27, Geoffrey Irving <[email protected]> wrote: > 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]> 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] >> 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
