In the higher order function case: f g = g 1 2 f :: (Nat -> Nat -> Nat) -> Nat
- d definiton: f :: ((Nat -> Nat -> Nat) -> Nat) :> (fn 1 (fn 2 Nat -> Nat -> Nat) -> Nat) - f application: f (\x . \y . x + y) f :: (fn 1 Nat -> (fn 1 Nat -> Nat)) - combining into range f :: (fn 1 (fn 1 Nat -> (fn 1 Nat -> Nat)) -> Nat) :> ((Nat -> Nat -> Nat) -> Nat) :> (fn 1 (fn 2 Nat -> Nat -> Nat) -> Nat) - considering the order on types: (fn 1 (fn 1 Nat -> (fn 1 Nat -> Nat)) -> Nat) <: (fn 1 (fn 2 Nat -> Nat -> Nat) -> Nat) - it admits no types, however: f g = ((g 1) 2) f :: ((Nat -> Nat -> Nat) -> Nat) :> (fn 1 (fn 1 Nat -> (fn 1 Nat -> Nat)) -> Nat) f (\x y . x + y) f :: fn 1 (fn 2 Nat -> Nat -> Nat) -> Nat) :> ((Nat -> Nat -> Nat) -> Nat) :> (fn 1 (fn 1 Nat -> (fn 1 Nat -> Nat)) -> Nat) - which does admit types, and is under-specified so we pick the most-curried of the range. That all seems reasonable, assuming I haven't made any mistakes :-) Keean.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
