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. Keean.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
