> 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.
I was wrong, it does require a type constraint like this: data Iterable = forall x . (Show (Value_Type x), Iterator x) => Iterable x Further Haskell does not allow instances to declare arbitrary associated types like I thought, but instead you declare type-family like type-level functions inside the instance declaration, which is why you can declare "Show (Value_Type x)". However this does mean that it does not allow two instances of the same type to declare different associated types, which is the problem I was describing. Haskell's associated types as not really associated types in the sense of ML's associated types in modules. So my original point, expressed more precisely, that having multiple instances for a given type-class where the associated types differ is unsound, is not affected by this. Keean. On 2 January 2015 at 19:15, Keean Schupke <[email protected]> wrote: > 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
