On Wed, Jan 7, 2015 at 3:54 PM, Keean Schupke <[email protected]> wrote:
> On the soundness issue, I think I now understand it a bit more. I don't > think there is a problem with type-families, nor with the way Haskell > handles associated types (which is as a type function of the type-class > parameters). > > It comes down to this, the associated types of instances with the same > type parameters must be the same. So the instances must be coherent as far > as the type system is concerned, but can have different values (function > definitions with the same parametric type signatures) > I don't think this is the whole story, and I think it's really important to try to be clear which of us is correct and why. I'd appreciate your help. Earlier, you wrote: If you have type-classes and want associated types (which are equivalent to > type families) the type system will be unsound if you can pass two > instances by value where they have the same type because type classes / > type families are always applicative. > With this view passing a type-class as a value just doesn't make sense, it > is always a type parameter. I think this is very exactly correct, and the key words here are "as a value". Though passing "as a value" is possible and legal as an implementation optimization in many useful cases, TC instances, and even *named* TC instances *are not values*. Or rather, they are a very special kind of value (statically resolvable constant bindings) that have some very unusual properties. Most importantly: they can be completely eliminated by partial evaluation. So given a type class Ord 'a and instances: default instance Ord int is < : int-less-then def upwards = instance Ord int is < : int-greater-than What I'm suggesting is that *because* instances are statically resolvable constant terms, they can be treated a lot like types for resolution purposes. I don't think that associated types change this at all. So if you squint your eyes in some very painful ways, you can actually think of the instance as a *type* and the class as a *kind*, and you can then read sort:: (Ord 'a) => Vector 'a -> Vector 'a as something akin to sort :: instance :: (Ord 'a) -> Vector 'a -> Vector 'a where all internal references to (<) within sort have been rewritten to (instance.<), and "instance" is ultimately replaced within the body of the specialization of sort with the (top level) name of the named instance. Further, if Ord happened to have an associated type, the internally-referenced type would now be (instance.AssociatedType), with "instance" similarly substituted. I claim that no unsoundness results, because these are all specialized away, and after specialization the associated types have all been renamed. I further claim that the same notion can be extended to named type families, should we want it to. IF YOU AGREE, then it would be really nice to find the right words to put around this. What is it, exactly, about statically resolvable constants that allows us to treat them like types in this fashion? Or is it rather that we are able to do type-driven specialization because types are really a higher-order statically resolvable constant? We can then start asking ourselves when such aggressive specialization is not necessary. The answer, in brief, is: whenever that would not create a soundness concern, which is to say: when associated types and associated type synonyms are not involved. > However I think it is a good idea to separate compile time from runtime. > Type classes can be entirely inlined at compile time except two cases I am > aware of, polymorphic recursion, and existential types. > Not true. Type classes can be entirely inlined under the whole-program assumption. When separate compilation gets into the picture, that stops being true. At that point you either need to pass dictionaries or do run-time (rather: dynamic load time) specialization. Which is probably best imagined as a sleazy way of implementing whole-program compilation late in the game. > Polymorphic recursion is somewhat problematic, so leaving it to one side, > I would like to treat all type-classes like C++ templates, and existentials > as virtual functions, where you define a base class for the type-class, and > then override for each instance. This means runtime polymorphism is > introduced only where intended by the programmer, all types can be unboxed > as all polymorphism is static apart from that introduced by an existential, > which is equivalent to an abstract base class with one layer of subclasses. > I lean the same way, for the same reasons, except to note the challenge of separate compilation. So I would say rather that type classes are resolved by specialization and existentials are resolved by value-passing, leaving the decision about the timing of specialization to the language profile. The decision for a whole-program profile can be different from the decision in a dynamic-loading profile. shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
