On Thu, Feb 19, 2015 at 11:33 AM, Jonathan S. Shapiro <[email protected]> wrote:
> On Wed, Feb 18, 2015 at 1:49 PM, Matt Oliveri <[email protected]> wrote:
>> 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.
>
>
> It took me a moment to process that, but you are saying something important
> here. I think you are saying that when we see two types written as
>
> f :: 'a -> 'b -> 'c
> g :: 'a -> 'b -> 'c
>
>
> we know that the argument and return types are the same, but nothing
> inherently tells us that the arities are the same. The reason it doesn't is
> that this textual representation of the type doesn't have any unifiable
> variable that captures the arities.
Essentially, yeah. It was sloppy of me to say "same arity-abstract
type", since in either of our versions of this, arity-abstract types
are not literally types by themselves. In mine, they were constraints,
in yours, they are arity-indexed families, it seems.
> This serves to remind me why at one point I proposed the notation
>
> fn 2 'x -> 'y -> 'z // function type have explicitly encoded native arity 2
>
>
> as opposed to
>
> fn 'x 'y -> 'z' // function type having implicitly encoded native arity 2
>
>
> The first would allow us to write f and g above as:
>
> f :: fn 'arity 'a -> 'b -> 'c
> g :: fn 'arity 'a -> 'b -> 'c
>
>
> which tells us that the two types must specialize with the same arities. If
> the arity type variable has not unified, then we can make things more
> readable by eliding the "fn 'arity" part. That is:
>
> 'a -> 'b -> 'c
>
>
> should be read as
>
> fn 'fresh-arity 'a->'b->'c
I have a question about this way of handling arity-abstract "types".
The thing is, when we specialize one, we don't get a concrete type
unless we maximized the arity.
So if we start with
fn arity a->b->c->d->r
and we want call it with two arguments, you say we get
fn 2 a->b->c->d->r
I suppose. But that type is still not concrete (even ignoring the type
variables). We could finish applying it with another 2-application or
two 1-applications, so there's still a choice of native arity to be
made. So I propose it should really be written:
fn a b -> fn newarity c->d->r
Well OK, so actually I hate that notation. What I'm trying to say is
that your arity-indexed family version of things doesn't seem to
capture how things can be specialized in multiple steps. In this
Frankenstein notation, we have an arity-concrete function returning an
arity-abstract function, which is what I think should happen when you
pick its arity. But where does newarity come from?
It might be less kludgey with my type constraint version, where we can
instantiate the constrained type variable to a type with another
constrained type variable. Starting with (using your notation)
(a->b->c->d->r ~ fn1) => fn1
we specialize to:
(c->d->r ~ fn2) => fn a b -> fn2
More explicitly, we weaken with the new constrained variable (c->d->r
~ fn2), getting the mess
(c->d->r ~ fn2) => (a->b->c->d->r ~ fn1) => fn1
so that fn2's in scope to instantiate fn1 to (fn a b -> fn2). The
rules of "~" must ensure that the fn1 constraint is satisfied,
assuming the fn2 one is.
>> 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.
>
>
> Yes. In this case, we could alternatively express it as a constrained type:
>
> choose_one :: ('a -> 'b -> 'c ~ 'fn) => 'fn -> fn -> 'fn
>
>
> there are other places where the ability to do that is useful, but I think
> in this case it's better to render the arity explicitly in the type.
Right now, my approach looks better, since it handles "partial
specialization" the way I expect. Maybe my assumption that arity can
be partially specialized is wrong, or I'm missing some obvious way to
express it with your approach.
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
