User loginNavigation |
archivesImplementing 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 (http://lambda-the-ultimate.org/node/5401). 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? Thanks |
Browse archivesActive forum topics
|
Recent comments
9 weeks 5 days ago
14 weeks 4 hours ago
15 weeks 4 days ago
15 weeks 4 days ago
18 weeks 2 days ago
22 weeks 6 days ago
22 weeks 6 days ago
23 weeks 2 days ago
23 weeks 2 days ago
26 weeks 1 day ago