On 19 February 2015 at 08:49, Matt Oliveri <[email protected]> wrote:
> On Wed, Feb 18, 2015 at 1:05 PM, Jonathan S. Shapiro <[email protected]> > wrote: > > Either x, y, and z will specialize to the same concrete arity, or the > > expression will fail to type check. > > So in order to enforce this, the type of choose_one needs to say that > x and y must have the same native arity, which doesn't follow from > them having the same arity-abstract type. I'm guessing what you meant > to say is that an arity-abstract type is actually a constraint on an > implicitly-quantified arity-concrete type. > > In general, writing an arity-abstract type twice will infer a > quantified variable for each of them. But in cases like choose_one, > from the definition of the function, you infer that there's a single > quantified variable. That is what expresses the requirement that x and > y have the same native arity. > Thanks Matt, PKE, and Shap. These two paragraphs are the missing piece of the puzzle. I could write it in Idris like so: > choose_one : {N : nativeFunctionTypeFor (Nat -> Nat -> Nat)} -> N -> N -> Bool -> N stating the variable in the type. ... well, maybe. You also said this, Shap: choose_one returns one of its arguments; and perhaps x has a curried >> definition and y takes two arguments directly. They have the same type, of >> course, so this is a perfectly reasonable thing to do. >> > > This is incorrect, because that is *not* a reasonable thing to do. They > have the same type. Therefore they are required to have the same concrete > type, therefore the same arity. > > If there is one concrete type per abstract function type, there's no need for quantification at all I guess. Just a global dictionary? BTW I wrote my email after reading your concrete proposal, but like I said, it only talks about applications and parameters and doesn't really deal with return values (or case expressions or any other kind of meet). Say, you said that paramaters and return values could be abstract, and then only talked about inference rules for parameters. -- 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
