derivation-rules.saty

@require: stdjareport
@require: itemize
@require: tabular
@require: proof
@require: bnf
@require: itemize
@import: local

document (|
  title = {Derivation Rules in Fialyzer};
  author = {fialyzer developers};
|) '<
  +p{
This file shows derivation rules used in fialyzer.
  }
  +p{
Our derivation rules are almost same as the original success typings paper\footnote{\bib{T. Lindahl and K. Sagonas}{Practical Type Inference Based on Success Typings}{Proceedings of the 8th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming}{167–178}{ACM}{2006}}'s one,
but extended by remote call, local call, list, etc.
  }
  +chapter{Derivation Rules}<
    +p{
      Here are the BNFs used in the derivation rules:
    }
    +small-block<
      +p{
        \BNFs[
          (${e}, [${| v | x | fn | \{e, \cdots , e\} | \mathtt!{let}\ x = e\ \mathtt!{in}\ e | \mathtt!{letrec}\ x = fn, \cdots , x = fn\ \mathtt!{in}\ e |};
                  ${| e\(e, \cdots , e\) | \mathtt!{case}\ e\ \mathtt!{of}\ pg \rightarrow e\; \cdots \;\ pg \rightarrow e\ \mathtt!{end} | \mathtt!{fun}\ f/a | \mathtt!{\[}e\mathtt!{\|}e\mathtt!{\]} | \mathtt!{\[\]} | \mathtt!{fun}\ \mfa{m}{f}{a}|};
                  ${| \map{e \assoc e, \cdots, e \assoc e} | e\map{e \assoc e, \cdots, e \assoc e, e \exact-assoc e, \cdots, e \exact-assoc e} \bnf-desc{term} |}]);
          (${v}, [${| \mathtt!{0} | \mathtt!{\'ok\'} | \cdots \bnf-desc{constant} |}]);
          (${x}, [${| \(\mathrm{snip}\) \bnf-desc{variable} |}]);
          (${fn}, [${| \mathtt!{fun}\(x, \cdots , x\) \rightarrow e \bnf-desc{function} |}]);
          (${pg}, [${| p\ \mathtt!{when}\ g\; \cdots \; g \bnf-desc{pattern\ with\ guard\ sequence} |}]);
          (${p}, [${| v | x | \{p, \cdots , p\} | \mathtt!{\[}p\mathtt!{\|}p\mathtt!{\]} | \mathtt!{\[\]} | \map{e \exact-assoc p, \cdots, e \exact-assoc p} \bnf-desc{pattern} |}]);
          (${g}, [${| v | x | \{e, \cdots , e\} | \mathtt!{\[}e\mathtt!{\|}e\mathtt!{\]} | \mathtt!{\[\]} | e\(e, \cdots , e\) \bnf-desc{guard} |}]);
          (${m}, [${| e \bnf-desc{module\ name.\ a\ term\ to\ be\ an\ atom} |}]);
          (${f}, [${| e \bnf-desc{function\ name.\ a\ term\ to\ be\ an\ atom} |}]);
          (${a}, [${| e \bnf-desc{arity.\ a\ term\ to\ be\ a\ non\_neg\_integer} |}]);
          (${\tau}, [${| \mathtt!{none\(\)} | \mathtt!{any\(\)} | \alpha | \{\tau, \cdots, \tau\} | \(\tau, \cdots, \tau\) \rightarrow \tau | \tau \cup \tau |};
                     ${| \mathtt!{integer\(\)} | \mathtt!{atom\(\)} | 42 | \mathtt!{\'ok\'} | \cdots \bnf-desc{type} |}]);
          (${\alpha, \beta}, [${| \(\mathrm{snip}\) \bnf-desc{type\ variable} |}]);
          (${C}, [${| \(\tau \subseteq \tau\) | \( C \wedge \cdots \wedge C\) | \(C \vee \cdots \vee C\) \bnf-desc{constraint} |}]);
          (${A}, [${| A \cup A | \{x \mapsto \tau, \cdots, x \mapsto \tau\} \bnf-desc{context.\ mapping\ of\ variable\ to\ type} |}])
        ];
      }
    >
    +p{
      Here are the derivation rules:
    }
    +small-block<
     +math(
       ${
         \derive?:{\paren{\mathsc{VAR}}}{
           | |
         }{
           \judgement{A \cup \{x \mapsto \tau\}}{x}{\tau}{\emptyset}
         }
       }
     );
    >
    +small-block<
      +math(
        ${
          \derive?:{\paren{\mathsc{STRUCT}}}{
            | \judgement{A}{e_1}{\tau_1}{C_1} | \cdots | \judgement{A}{e_n}{\tau_n}{C_n} |
          }{
            \judgement{A}{\{e_1, \cdots , e_n\}}{\{\tau_1, \cdots , \tau_n\}}{C_1 \wedge \cdots \wedge C_n}
          }
        }
      );
    >
    +small-block<
      +math(
        ${
          \derive?:{\paren{\mathsc{LET}}}{
            | \judgement{A}{e_1}{\tau_1}{C_1} | \judgement{A \cup \{x \mapsto \tau_1\}}{e_2}{\tau_2}{C_2} |
          }{
            \judgement{A}{\mathtt!{let}\ x = e_1\ \mathtt!{in}\ e_2}{\tau_2}{C_1 \wedge C_2}
          }
        }
      );
    >
    +small-block<
      +math(
        ${
          \derive?:{\paren{\mathsc{LETREC}}}{
            | \judgement{A'}{fn_1}{\tau_1}{C_1} \cdots
              \judgement{A'}{fn_n}{\tau_n}{C_n} |
              \judgement{A'}{e}{\tau}{C} |
              \mathtt!{where}\ A' = A \cup \{x_i \mapsto \alpha_i\} |
          }{
            \judgement{A}{\mathtt!{letrec}\ x_1 = f_1, \cdots , x_n = f_n\ \mathtt!{in}\ e}{\tau}{C_1 \wedge \cdots \wedge C_n \wedge C \wedge \(\tau'_1 = \tau_1\) \wedge \cdots \wedge \(\tau'_n = \tau_n\)}
          }
        }
      );
    >
    +small-block<
      +math(
        ${
          \derive?:{\paren{\mathsc{ABS}}}{
            | \judgement{A \cup \{x_1 \mapsto \alpha_1, \cdots , x_n \mapsto \alpha_n\}}{e}{\tau}{C} |
          }{
            \judgement{A}{\mathtt!{fun}\(x_1, \cdots , x_n\) \rightarrow e}{\(\alpha_1, \cdots , \alpha_n\) \rightarrow \tau}{C}
          }
        }
      );
    >
    +small-block<
      +math(
        ${
          \derive?:{\paren{\mathsc{APP}}}{
            | \judgement{A}{e}{\tau}{C} |
              \judgement{A}{e_1}{\tau_1}{C_1} \cdots \judgement{A}{e_n}{\tau_n}{C_n} |
          }{
            \judgement{A}{e\(e_1, \cdots , e_n\)}{\beta}{\(\tau = \(\alpha_1, \cdots , \alpha_n\) \rightarrow \alpha\) \wedge \(\beta \subseteq \alpha\) \wedge \(\tau_1 \subseteq \alpha_1\) \wedge \cdots \wedge \(\tau_n \subseteq \alpha_n\) \wedge C \wedge C_1 \wedge \cdots \wedge C_n}
          }
        }
      );
    >
    +small-block<
      +math(
        ${
          \derive?:{\paren{\mathsc{PAT}}}{
            | \judgement{A}{p}{\tau}{C_p} |
              \judgement{A}{g}{\tau_g}{C_g} |
          }{
            \judgement{A}{p\ \mathtt!{when}\ g}{\tau}{\(\tau_g \subseteq \mathtt!{boolean\(\)}\) \wedge C_p \wedge C_g}
          }
        }
      );
    >
    +small-block<
      +math(
        ${
          \derive?:{\paren{\mathsc{CASE}}}{
            | \judgement{A}{e}{\tau}{C_e} |
              \judgement{A_i}{pg_i}{\tau_{pg_i}}{C_{pg_i}} |
              \judgement{A_i}{b_i}{\tau_{b_i}}{C_{b_i}} |
              \mathtt!{where}\ A_i = A \cup \{v \mapsto \alpha_v \| v \in Var\(pg_i\)\} |
          }{
            \judgement{A}{\mathtt!{case}\ e\ \mathtt!{of}\ pg_1 \rightarrow b_1\;\ \cdots \ pg_n \rightarrow b_n \mathtt!{end}}{\beta}{C_e \wedge \(C_1 \vee \cdots \vee C_n\)
              \mathtt!{where}\ C_i = \(\(\beta = \tau_{b_i}\) \wedge \(\tau = \tau_{pg_i}\) \wedge C_{pg_i} \wedge C_{b_i}\)
            }
          }
        }
      );
    >
    +small-block<
      +math(
        ${
          \derive?:{\paren{\mathsc{LOCALFUN}}}{||}{
            \judgement{A \cup \{\mathtt!{fun}\ f/a \mapsto \tau\}}{\mathtt!{fun}\ f/a}{\tau}{\emptyset}
          }
        }
      );
    >
    +small-block<
      +math(
        ${
          \derive?:{\paren{\mathsc{LISTCONS}}}{
            | \judgement{A}{e_1}{\tau_1}{C_1} |
              \judgement{A}{e_2}{\tau_2}{C_2} |
          }{
            \judgement{A}{\mathtt!{\[} e_1 \| e_2 \mathtt!{\]}}{\mathtt!{list\(} \alpha \| \tau_1 \mathtt!{\)}}{\tau_2 = \mathtt!{list\(} \alpha \mathtt!{\)} \wedge C_1 \wedge C_2}
          }
        }
      );
    >
    +small-block<
      +math(
        ${
          \derive?:{\paren{\mathsc{LISTNIL}}}{||}{
            \judgement{A}{\mathtt!{\[\]}}{\mathtt!{list\(none\(\)\)}}{\emptyset}
          }
        }
      );
    >
    +small-block<
      +math(
        ${
          \derive?:{\text!{if ${m} and ${f} is atom literal, ${a} is non_neg_integer literal}\ \paren{\mathsc{MFA}}}{||}{
            \judgement{A \cup \{\mathtt!{fun}\ \mfa{m}{f}{a} \mapsto \tau\}}{\mathtt!{fun}\ \mfa{m}{f}{a}}{\tau}{\emptyset}
          }
        }
      );
    >
    +small-block<
      +math(
        ${
          \derive?:{\text!{if ${\diamond}}\ \paren{\mathsc{MFAEXPR}}}{
            | \judgement{A}{m}{\tau_m}{C_m} |
              \judgement{A}{f}{\tau_f}{C_f} |
              \judgement{A}{a}{\tau_a}{C_a} |
          }{
            \judgement{A}{\mathtt!{fun}\ \mfa{m}{f}{a}}{\beta}{\(\tau_m \subseteq \mathtt!{atom\(\)}\) \wedge \(\tau_f \subseteq \mathtt!{atom\(\)}\) \wedge \(\tau_a \subseteq \mathtt!{number\(\)}\) \wedge C_m \wedge C_f \wedge C_a}
          }
        }
      );
    >
    +small-block<+math(${\diamond: \text!{neither ${m}, ${f} is atom literal nor ${a} is non_neg_integer literal}});>
    +small-block<
      +math(
        ${
          \derive?:{\paren{\mathsc{MAPCREATION}}}{||}{
            \judgement{A}{\map{\cdots}}{\mathtt!{map\(\)}}{\emptyset}
          }
        }
      );
    >
    +small-block<
      +math(
        ${
          \derive?:{\paren{\mathsc{MAPUPDATE}}}{
            | \judgement{A}{e}{\tau}{C} |
          }{
            \judgement{A}{e\map{\cdots}}{\mathtt!{map\(\)}}{\paren{\tau \subseteq \mathtt!{map\(\)}} \wedge C}
          }
        }
      );
    >
    +small-block<
      +math(
        ${
          \derive?:{\paren{\mathsc{CATCH}}}{
            | \judgement{A}{e}{\tau}{C} |
          }{
            \judgement{A}{\mathtt!{catch}\ e}{\mathtt!{any\(\)}}{C}
          }
        }
      );
    >
    +section{Differences from the original paper}<
      +p{
        The differences from the derivation rules on the original paper are as follows.
        \listing{
          * ${\alpha}, ${\beta}, and ${\tau} are clearly distinguished. ${\tau} is a type, and ${\alpha}, ${\beta} are type variables.
          * LET is fixed: ${e_2}, not ${e}.
          * ABS is modified: ${\tau} and constrained function are omitted.
          * PAT is modified: type of ${g} is ${\mathtt!{boolean\(\)}}, not ${\mathtt!{true}}.
          * CASE is fixed: ${\tau}, not ${\tau_i}. replaced ${p_1 \cdots p_n} with ${pg_1 \cdots pg_n} because these are patterns with guards.
          * LOCALFUN is added.
          * MFA is added.
          * MFAEXPR is added.
          * MAPCREATION is added (temporary definition).
          * MAPUPDATE is added (temporary definition).
          * ...and some variables are ${\alpha}-converted for understandability.
        }
      }
    >
    +section{Notes}<
      +listing{
        * In ${\judgement{A}{p}{\tau}{C_p}} of PAT rule, ${p} is not an expression but a pattern. Therefore, we have to convert ${p} to an expression which is the same form of ${p}.
          ** This is not described in the original paper.
      }
    >
  >
>