On Wed, Apr 1, 2015 at 4:00 AM, Keean Schupke <[email protected]> wrote: > On 1 Apr 2015 08:45, "Matt Oliveri" <[email protected]> wrote: >> On Wed, Apr 1, 2015 at 3:23 AM, Keean Schupke <[email protected]> wrote: >> > We agree that arity-aware types break paretricity right? >> >> I don't see why. > > Because they break the smoothness requirement of universally quantified > types.
Is the rest of your email explaining why you think that, or is this just an isolated assertion? > choose_one :: a -> a -> Bool -> a > > The type of 'a' depends on the types unified for each argument. You mean the type we chose to instantiate 'a' with is determined by unifying the actual argument's types? Yes. So what? > The accepted > type is the intersection of the two argument types. Just encoding a single > value is not enough. For example: That doesn't sound right. Shouldn't it be the lub of the types of the actual arguments? Intersection would be glb. But anyway, we aren't doing subtyping. At least that's not how we've been talking about doing it the whole time. It's just unification. It might start to look more like subtyping once we consider effect annotations and application-driven specialization. > x : a => b c => d > y : a => b => c -> d Let's get something straight: our scheme is completely independent from yours. I used a combination of ours and your notation in an earlier email. This was to increase the likelihood of you understanding the immediate point, but it may have been misleading. We would write the type of x as (cfn 'a->cfn 'b 'c->'d). I don't know what the type of y means, now that you've acknowledged that the "c -> d" isn't an HM arrow. Can y be called with 3 arguments? If not, or you can't tell, then our system cannot express that type, and this is an important aspect of the design. If so, then it seems it should be (a=>b=>c=>d) in your system, and it would be (cfn 'a->cfn 'b->cfn 'c->'d) in ours. > Both would be: > > cfn 1 a -> b -> c -> d Whose notation is that? Not ours. > You would need at least: > > x : cfn [1,2] a -> b -> c -> d > y : cfn [1,1] a -> b -> c -> d > > To deal with this. I'm fairly certain you just made this notation up. I figure you're using deep arities, but we don't use deep arities with cfns. Only (possibly) afns. Moreover, the type "afn [1,1] 'a 'b 'c->'d" would be ill-formed because it has 3 arguments, but the deep arity only accounts for 2 of them. > But like you say you then need to wrap arity-abstract types into afns. > > But then you have to explicitly deal with AFN unification cases. It seems to > be turning into a big mess. There is a reason why curried types are used > normally. > > It all seems to be heading towards intersection types to me. I'd take your warning about our system more seriously if you appeared to understand how our system works. You have loaded more complexity than our system has overall into just the "cfn" types you invented above. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
