Currently, judgments accept whatever rules are given without questioning whether there should be more rules. It has been pointed out that this allows a language designer to forget to write a rule he intends to add. For example, forgetting to write a typing rule for addition means addition is not typable, rather than being a bug.
Complete judgments would be required to have a rule specifically for each constructor of the primary component. A judgment
Complete Judgment typeOf : tyctx expr* ty
would need to have a rule for each constructor of expr where the primary component was built by that constructor. This would cause an error if the typing rule for addition was left out. The error checking should carry over into modules building on the one introducing the complete judgment so they must also introduce rules for each new constructor of expr.
This would not ban generic rules where the primary component is a variable. However, those rules would not count toward completeness.
Fixed judgments could not be declared as complete because they do not have primary components.
Complete judgments will only check for each constructor having at least one constructor-specific rule. We cannot check that the judgment is always derivable.
Currently, judgments accept whatever rules are given without questioning whether there should be more rules. It has been pointed out that this allows a language designer to forget to write a rule he intends to add. For example, forgetting to write a typing rule for addition means addition is not typable, rather than being a bug.
Complete judgments would be required to have a rule specifically for each constructor of the primary component. A judgment
would need to have a rule for each constructor of
exprwhere the primary component was built by that constructor. This would cause an error if the typing rule for addition was left out. The error checking should carry over into modules building on the one introducing the complete judgment so they must also introduce rules for each new constructor ofexpr.This would not ban generic rules where the primary component is a variable. However, those rules would not count toward completeness.
Fixed judgments could not be declared as complete because they do not have primary components.
Complete judgments will only check for each constructor having at least one constructor-specific rule. We cannot check that the judgment is always derivable.