On 21 February 2015 at 10:41, Keean Schupke <[email protected]> wrote:
> Given:
>
> g :: Nat -> Nat -> Nat
>
> g 1 2
>
> At the application site of g we infer the type g :: fn' Nat Nat -> 'a
> where we want to allow definitions of 'g' that are more-curried. The
> relationship between the application type and the imported type is
> subtyping with fully-curried as the top type. However when typing higher
> order functions more curried is the bottom type for contravariant
> arguments. Hence why we can't agree on the order.
>
> It seems the behaviour is covariant with subtyping such that fully-curried
> is the top type.
>
Actually I am talking rubbish... Obviously least-curried is the super type,
I am getting things backwards.
Actually you can make sense of this if you consider 'g' to be an implicit
parameter, consider:
import g :: Nat -> Nat -> Nat
main = g 1 2
main :: {g :: fn Nat Nat -> Nat} -> Nat
Now we can pass 'g' in implicitly using normal subsumtion :-) And I don't
try and think of the inverse-subsumtion rule unification seemed to need.
Keean.
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
