If you want to have an upcast as a function you would have to define it as you did:
upcast1_1to2 (f : fn 1 a->fn 1 b->c) : fn 2 a->b->c = f first I don't understand this type, do you mean cast1 :: fn 1 (fn 2 'a -> 'b -> 'c) -> (fn 1 'a -> fn 1 'b -> 'c) or cast2 :: fn 1 (fn 1 'a -> fn 1 'b -> 'c) -> (fn 2 'a -> 'b -> 'c) Keean. upcast1_1to2 f = \x y . (f x) y On 24 February 2015 at 16:28, Matt Oliveri <[email protected]> wrote: > On Tue, Feb 24, 2015 at 10:57 AM, Keean Schupke <[email protected]> wrote: > > On 24 February 2015 at 15:49, Keean Schupke <[email protected]> wrote: > >>> See for yourself: > >>> > >>> Source code: > >>> f x = \y. x + y // This lambda was put by the programmer > >>> ... > >>> f 1 2 // Arity mismatch (but admitted by order) > >>> > >>> Specialize application: > >>> f x = \y. x + y > >>> ... > >>> (f 1) 2 > >>> > >>> Specialize definition: > >>> f x y = x + y > >>> ... > >>> f 1 2 > >> > >> So this is exactly what I was proposing. > > > > This is the mechanism the compiler is using. Now we need a type system > that > > only admits the same types that we can specialise as above. How this type > > system works has nothing to do with the underlying application, its > simply a > > model of the acceptable types. We prove soundness by showing that all the > > types admitted by the type system produce valid programs from the > compiler. > > > > S <: T means we accept S anywhere we would accept T. > > > > There's nothing about coercion here? A coercive subtyping system is > > something different, it is semantics added to the language. > > Rats, I thought that was the end of the story. OK, so if we're on the > same page now with coercions being bad, how do you implement the > upcast from a few emails ago? > > On Tue, Feb 24, 2015 at 10:07 AM, Matt Oliveri <[email protected]> wrote: > > On Tue, Feb 24, 2015 at 9:39 AM, Keean Schupke <[email protected]> wrote: > >> Can you give me an example where you think the subtyping admits a type > that > >> arity-abstract types do not? If you believe there is a difference, you > >> should be able to provide an example. > > > > 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 > > > > This function allocates. > _______________________________________________ > 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
