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

Reply via email to