Implementing typing rules -- how do I implement non-syntactic rules?

Hi all,

Typing rules in papers are usually not directly implementable as a checker. For example, they usually include a rule that requires coming up with a type for a binder, e.g. a lambda argument (when lambda doesn't have type of its argument in the syntax). I'm wondering if there's a standard way of implementing this type of rules, because as far as I can see none of the papers I'm looking at explicitly say how to do this.

To be more concrete, I'm looking at the Frank paper ( The paper says it has bidirectional typing dicipline, but other than that it doesn't hint at how to implement the typing rules. So when I see this rule for lamabda (Fun) I have no idea how to implement that.

I checked the literature on bidirectional typing (Local Type Inference etc.) but couldn't see anything relevant. So I'm guessing that in the literature when I see this kind of rules it means "use Damas-Hindley-Milner style metavariable generation + unification etc.", am I right? Are there any other ways of doing this? If yes, then how do I know which method I should be using?


Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

No, when people don't

No, when people don't provide algorithmic rules, they don't mean use HM-style inference. The Frank paper splits the rules into (in the terminology of the LTI paper) synthesis and checking rules. The checking rules (such as Fun) do not have any outputs -- the type to be checked against is an input just like the term and environment. In Figure 4 in that paper, the algorithm goes into checking mode using the Coerce rule, which has the type there in the syntax.

Ahh, I had a quick look

Ahh, I had a quick look after reading your comment and it finally made sense. I guess I was confused because the figure does not indicate inputs and outputs (like plus and minus signs in this lecture notes: Thanks!