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
