On Wed, Feb 18, 2015 at 1:49 PM, Matt Oliveri <[email protected]> wrote:
>
> Hopefully you are not saying that whenever the same arity-abstract
> type appears twice, the corresponding arity-concrete types are
> arbitrarily required to be the same. With choose_one, the native
> arities must be the same, but that's because of how choose_one is
> defined....
I'm not saying that. What I *am* saying is that a given abstract type can
only concretize one way in a given specialization. In the choose_one case,
those two types unify, so they are the same type, so they specialize the
same way **at a given application**.
> 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.
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.
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
and can often be printed using the simpler notation. Once the arity is
concrete, there are several candidate notations, any of which would work:
fn 2 'x->'y->'z
fn 'x 'y -> 'z
fn 'x, 'y -> 'z // need to check grammar conflicts
My point is only that a concrete arity doesn't necessarily need to have a
number syntactically associated with it.
To those of you who have objected to it, I'd note that *I* don't like the
"fn" notation either. I agree that it seems unnecessarily heavy. But
regardless of how we write the surface syntax, "fn" is actually a
two-argument constructor taking arity and function 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.
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.
shap
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
