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 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
