On 12 February 2015 at 19:56, Keean Schupke <[email protected]> wrote:
> You can infer the required type of 'f' from its use.
>
> You can also infer the defined type of f from its definition.
>
The issue under discussion is not about types (at least, not in the usual
sense). Consider:
f : Nat -> Nat -> Nat
f x y = ...
g : {X} -> (X -> Nat) -> X -> Nat
g f x = f (S x)
let h = (if something then f else (g f)) in ...
both f and g have the same type, but different native arities. The
question is, what is the native arity of h? There are two sensible
answers. Of the usages of h that might follow, we may have a hard time
deciding which to make first-class. When h is a local, it might even be
sensible to provide both immediately.
> You can treat this compositionally, so when two program fragments are
> composed, you match the requirements from one fragment against the
> definitions from the other.
>
We are familliar with how a type system works, you know. In the specific
case of type systems for calling conventions, there is "Types Are Calling
Conventions" by Bollingbroke and SPJ, as existing work. BitC's intended
audience has additional bearing on this, and that is what we're trying to
discuss. BitC cannot entertain the same level of magic as other languages
might be able to get away with. We want native performance out of what may
be generic or higher-order calls.
--
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
