Ah, I've just realised I misread your type signature. In any case, this is safe:
down f x y = (f x) y and this is not up f x = \y . f x y My system permits the first not the second, thats the whole point of the order on types. Keean. On 24 February 2015 at 15:25, Keean Schupke <[email protected]> wrote: > Huh? You need a lambda to do the reverse: > > downcast1_2to1 f x = \y . f x y > > but not the upcast. > > > Keean. > > > On 24 February 2015 at 15:24, Matt Oliveri <[email protected]> wrote: > >> On Tue, Feb 24, 2015 at 10:18 AM, Keean Schupke <[email protected]> wrote: >> > On 24 February 2015 at 15:07, Matt Oliveri <[email protected]> wrote: >> >> >> >> You mean admits a program? That's very easy. The basic problem with >> >> subtyping that it admits coercions: >> >> >> >> upcast1_1to2 (f : fn 1 a->fn 1 b->c) : fn 2 a->b->c = f >> > >> > Hmm but this coercion is safe, as all we are doing is this: >> > >> > upcast1_1to2 f x y = (f x) y >> >> No, because in BitC, that would require f, x , and y to be passed at >> once. You'd have to write it with a lambda. >> _______________________________________________ >> bitc-dev mailing list >> [email protected] >> http://www.coyotos.org/mailman/listinfo/bitc-dev >> > >
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
