Is there any way to algorithmically check the consistency of a set of bidirectional typing rules, e.g. the absence of cycles and the uniqueness of the derivation tree? This problem is naturally similar to the problem of grammar unambiguity checking, except you also gotta manage side effects applied to the typing context.


Ok, from reactions I figured that this question needs more context:

  • I am not building a bidirectional type system.
  • Instead I am building it's sanity checker.
  • I presume, that there is a serialized representation for a set of rules, like yaml, json, what have you.
  • By the time I get an instance of that representation it is presumed to be a syntactically (and schema-wise) valid document.
  • Now, it is obvious that being a valid document doesn't give any guarantees about rules consistency with one another:
    • There might be several premise sets for a given conclusion.
    • There might be several different conclusions from a given premise set.
    • Premises and corresponding conclusions might be in a cyclic dependency on one another.
    • Maybe something else.

All in all, having a valid rule set S, just add a wildcard inference rule like $$ \frac{}{\Gamma \vdash a \Rightarrow Int} $$ and you will get the rule set S' that is either ambiguous (if there is no rule ordering) or 'non-minimal' at best (if wildcards go at the end).

So, those bad things can happen, and it seems like there must be a paper or something considering discussed problem.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.