On 20 February 2015 at 21:24, Matt Oliveri <[email protected]> wrote:
> passArith f = f (\x y -> x + y) (\x y -> x - y) > passArith : fn ((fn Nat Nat -> Nat)->(fn Nat Nat -> Nat)->Nat) -> Nat > If we infer an abstract arity: passArith : ((Nat -> Nat -> Nat) -> (Nat -> Nat -> Nat) -> Nat) -> Nat > useArith plus minus = minus 10 (plus 4 3) > useArith : fn (Nat->Nat->'a) (Nat->'a->'b) -> 'b > useArith : (Nat -> Nat -> Nat) -> (Nat -> Nat -> Nat) -> Nat useArith' plus = lambda minus = minus 10 (plus 4 3) > useArith' : fn (Nat->Nat->'a) -> fn (Nat->'a->'b) -> 'b useArith' : (Nat -> Nat -> Nat) -> (Nat -> Nat -> Nat) -> Nat everything seems fine, looking at an application: import plus :: fn Nat Nat -> Nat passArith (useArith plus plus) from the application we get useArith :: fn (fn Nat Nat -> Nat) (fn Nat Nat -> Nat) -> Nat and passArith fn (fn (fn Nat Nat -> Nat) (fn Nat Nat -> Nat) -> Nat) -> Nat which by subtyping would be accepted as an application of: passArith : ((Nat -> Nat -> Nat) -> (Nat -> Nat -> Nat) -> Nat) -> Nat however we can emit a specialised version of 'passArith' for the concrete type: fn (fn (fn Nat Nat -> Nat) (fn Nat Nat -> Nat) -> Nat) -> Nat Which is more efficient than this inferred from the definition: passArith : fn ((fn Nat Nat -> Nat)->(fn Nat Nat -> Nat)->Nat) -> Nat Keean.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
