On Thu, Feb 12, 2015 at 12:27 AM, Matt Oliveri <[email protected]> wrote:
> I'm not sure what you're saying we should infer for the (f x y) > example. That could either be a 2-application, or two 1-applications, > if they had the same syntax. That's why I proposed writing two > 1-applications like ((f x) y). So if we want to get detailed about it, (f x y) probably means that we infer 'arity <= 2 => fn 'arity 'a -> 'b The nat in the fn type has nat kind for a reason! So then you use your constraint solver to solve all the constraints on 'arity, but you are likely to still end up with an under-constrained resolution. At that point your sensible choices are "assume 1" (in which case we should have just done arity-less functions in the first place), or "assume the max" (which is likely to be the most efficient calling convention). >From a sound and complete checking perspective, I actually do not like "assume the max" here. It's always a bit ugly when the solver has a tie-breaking heuristic. But I think it is the right heuristic for BitC. shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
