On Tue, Feb 10, 2015 at 4:41 PM, Geoffrey Irving <[email protected]> wrote:
> > For output purposes, it's probably clearer to emit that as (int -> int)->
> > int, though that won't work as an input syntax.
>
> Output syntax that doesn't work as input syntax seems sketchy.
>
I agree. In fact, that's kind of the point I was trying to make.
> > Alternatively, we could continue to write function types similarly to the
> > way we do now, which in this case would be:
> >
> > fn (int, int) -> int
>
Apologies, but my example above is incorrect. We need a way to describe a
function taking a tuple as a single argument. I can make the example above
work from a grammar standpoint, but then we'd end up writing
fn ((int, int)) -> int
for "function taking tuple of two ints", which seems like a good
opportunity to confuse people. So I think we're probably going to end up
with one of
fn int int -> int
fn 2 int -> int -> int
for this. Int he first variant, the number of argument positions encodes
the function arity. In the second, the number of arguments is encoded by a
Nat > 0
Coming from C, it took me a while to get used to the a->b->c style of
writing function types, but I've come to appreciate it. I now think that
it's unfortunate to lose the spare character of that notation, but when we
start looking at function effects we're going to need a place to put those
annotations, and there's no way we're going to do that without adding some
weight onto that arrow.
Regarding curried application, I realized this morning that it's more
complicated than that. In order to talk about this, it's easier to use the
second variant above.
TYPE COMPATIBILITY
The question concerns type compatibility. In OCaml or Haskell, where
application is curried, the following two types are indistinguishable:
fn 1 int -> int -> int
fn 2 int -> int -> int
The question arises: what should the compatibility rules be in BitC? There
seem to be three possible choices:
*Option 1*: Arity must match. This is the easiest choice, but it means (for
example) that we can't map over a list producing an output list of
partially applied functions without introducing an explicit lambda. It's
the cleanest choice for type inference purposes.
*Option 2*: The formal parameter arity must be less than or equal to the
actual parameter arity. This is the second easiest choice, because given a
function definition having arity *k*, we can statically generate at compile
time all of the wrapper functions having arity 1.. *k-1*. If the procedure
definition cannot be statically resolved, the compiler has to inject a
lambda wrapper at the point of call.
*Option 3:* Place no requirement on arity matching. Require only that the
arrow types match, and have the compiler inject a lambda for arity
impedance matching when necessary. This option fully preserves the
functional style, but it will produce a lot of hidden procedures and
allocations that aren't apparent to the programmer.
In my opinion, Option 2 will feel very strange. It's a choice motivated by
the convenience of the implementation rather than what makes sense
logically or mathematically. It feels like something that people will bump
up against and scratch their heads about.
Both Option 1 (require explicit lambdas) and Option 3 (add implicit lambdas
as needed) will give the language a consistent feel. The problem with
Option 3 is that it's going to produce a lot of hidden allocations, and it
introduces an implicit coercion into the type system. In this (somewhat
unusual) case, I don't think the coercion introduces any major problems,
because from the mathematical point of view the type isn't really changing.
If you'll indulge a temporary term invention, it's an implicit pragmatics
coercion rather than an implicit type coercion.
For the moment, I would prefer to go with Option 1. This will force us to
introduce lambdas explicitly, but existing code will not break if we later
decide to shift to Option 3. My main rationale is that in systems languages
we really don't want to be doing implicit allocations.
This, incidentally, implies that even if we end up using curried
application *syntax*, the application
f a
will signal a type mismatch if the arity of f is something other than 1.
I'm perfectly willing to introduce an operator to explicitly indicate that
the necessary lambda should be constructed. We can't use f . a for this,
but I'm sure we can find something.
FUNCTION DEFINITION SYNTAX
Given that we can explicitly annotate to get any arity we want, two
questions now arise.
First, what type should be given to the following function in the absence
of annotation?
def f x y = x + y
I propose that it should be fn 2 'a -> 'a -> 'a and not fn 1 'a -> 'a ->
'a. You can get a different arity by using either:
def f = lambda 1 x y = x + y
def f 1 x y = x + y
Note that numbers aren't identifiers, which is why this works. Though I
concede they feel strange.
Alternatively, we could adopt a comma convention (parens in types for
emphasis):
def f x y = x + y // fn 1 'a -> (fn 1 'a -> 'a)
def f x, y = x + y // fn 2 'a -> 'a -> 'a
def f x, y z = x + y + z // fn 2 'a -> 'a -> (fn 1 'a -> 'a)
Whatever we decide, one syntax will end up being "lighter" than the other,
so we will end up with a "preferred" syntax. Curried application is closely
associated with functional languages, and arity with non-functional
(disfunctional?) languages, so I think this is a place that's going to have
a lot of impact on the feel of the language. BitC's primary purpose is
*systems* codes, so as much as I want to enable and facilitate the
functional style, the design priority here is probably to avoid implicit
allocations at procedure calls.
INFERENCE
One problem that I anticipate with curried application syntax is that it
removes information needed for arity inference. GIven:
def myfn f x y = f x y
what arity should we infer for f? In this case, I think the answer
probably turns out to be '2", but it's possible to imagine other cases in
which that would not be the case. For example:
def myfn f x y =
let u = f x y
v = f x
in
v y
I think the inferred arity here is "1".
Comments, thoughts, and reactions welcome!
shap
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
