On Sun, Jan 5, 2014 at 7:58 AM, Sandro Magi <[email protected]> wrote:
> On 04/01/2014 2:27 PM, Jonathan S. Shapiro wrote: > > On Sat, Jan 4, 2014 at 7:01 AM, Sandro Magi <[email protected]<mailto: >> [email protected]>> wrote: >> interfaces = existential quantification + overloading >> >> >> I am not sure how overloading gets in to this. >> > > You're probably assuming a more liberal definition of "overloading", like > that found in C# and Java where one can specify overloaded functions of > different arities. I intended the more principled version as implied by > type classes, where overloading is simply defining a type-indexed > operation. We can disregard this if that's the case since it will only > cause confusion. > Ah. OK. That makes sense. Thanks for helping me get on the same page. I wouldn't normally think of "opening" the existential as type indexing, though of course that is the effect obtained in many actual use-cases (including this one). Anyway, thanks. > > interfaces = existential quantification + single parameter type >> classes >> >> >> I said that a while back, but I no longer think that is correct. >> >> An interface is existentially quantified over 'this exactly if it has >> non-static methods. An interface may be parametric. Type variables /other >> than/ 'this are universally quantified. Those universally quantified >> variables can be subject to constraints. >> >> >> Because those type variables are universally quantified, I think that >> interfaces subsume multi-parameter type classes as well. >> > > The following are equivalent in my mind: > > public interface IFoo > { > T0 Foo<T0, T1>(T0 arg0, T1 arg1) > where T0 : IFoo; > } > > class Foo x where > foo :: Foo a => x -> a -> b -> a > > -- existential wrapper > data AnyFoo = forall a. Foo a => AnyFoo a > > -- instance for the existential > instance Foo AnyFoo where > foo (AnyFoo x) a b = foo x a b > > The 'a' and 'b' parameters of the overloaded foo function are also > universally quantified, and 'a' has an additional IFoo constraint. Am I > missing something? > Yes and no. Your existential wrapper seems to assume that a forall quantifier can be introduced in a non-top-level scope. There are languages where this is the case, but its not the baseline common understanding of forall. > Finally, for interfaces to subsume multiparam type classes, they must > dispatch on multiple parameter types ala multimethods, which interfaces > don't do unless you're assuming some sort of generalized interface like > from the papers I posted a month or two ago. I'm certainly contemplating a more generalized notion of interface, but there are pragmatics issues that I need to make sure I understand how to solve. For the moment, let me simply say that I want an interface mechanisms that is as parametric as I can sustainably make it. shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
