> This implementation is just the type checker, right? That's not what > I'm concerned about if it's true that you're just using unrestricted > subtyping among arity-concrete function types.
Well the type checker implementation clearly specifies what types are admitted and which ones not, so you cannot get confused by english, which is far to imprecise and informal to capture the exact definitions. The implementation is in logic, so its a mathematical description not an implementation in that sense, and the interpreter I am using does not follow normal Prolog clause order, so you can treat it as a nondeterministic-specification. The soundness of this type inference depends on this AST transformation being available to the compiler: app(lam(x, lam(y, A)), B, C) => app(app(lam(x, lam(y, A), B), C) OR app(lam(x, lam(y, A)), B, C) => app(lam(x, y, A), B, C) The first works all the time, even if the function is imported from 'C' and has a fixed concrete arity. The second is a more efficient optimisation available if you have access to source of the function. Keean.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
