Differences
This shows you the differences between two versions of the page.
Next revision | Previous revision | ||
sav08:set_constraints_for_algebraic_datatype_inference [2008/05/22 00:13] vkuncak created |
sav08:set_constraints_for_algebraic_datatype_inference [2015/04/21 17:30] (current) |
||
---|---|---|---|
Line 5: | Line 5: | ||
**Example** | **Example** | ||
- | Using the following grammar : | + | Consider data type definition |
type form = Atom of string | type form = Atom of string | ||
- | | And of form*form | + | | And of form * form |
- | | Or of form*form | + | | Or of form * form |
| Not of form | | Not of form | ||
- | we can have the following types : $F = \lbrace Atom, And(\_ , \_), Or(\_ , \_), Not \_ \rbrace$ which is an infinite set ("_" represents any kind of type). | + | We represent values of this data type as ground terms in language $L = \{ atom,not,and,or\}$. |
+ | |||
+ | Define function: | ||
- | But if we define the following function : | ||
let rec elimOr(f : form) : form = | let rec elimOr(f : form) : form = | ||
match f with | match f with | ||
Line 21: | Line 23: | ||
S4: | Not(f1) -> Not(elimOr f1) | S4: | Not(f1) -> Not(elimOr f1) | ||
- | It is clear that the output types of this function is a subset of $F$ (as the $Or$ is removed). In fact, if we define $res$ as the resulting type of this function, $res$ can be computed by computing the fixpoint of : $S_1 \cup S_2 \cup S_3 \cup S_4 \subseteq res$ | + | We infer the subset of formulas returned by this function using set constraints. Introduce set for each case of pattern matching expression. Let 'res' denote the set of values that can be returned by the function. We obtain the system of constraints: |
- | + | \begin{equation*} | |
- | - $Atom \subseteq S_1$ | + | \begin{array}{l} |
- | - $And(res, res) \subseteq S_2$ | + | atom \subseteq S_1 \\ |
- | - $Not(And(Not(res), Not(res))) \subseteq S_3$ | + | and(res, res) \subseteq S_2 \\ |
- | - $Not(res) \subseteq S_4$ | + | not(and(not(res), not(res))) \subseteq S_3 \\ |
- | + | not(res) \subseteq S_4 \\ | |
- | In this particular case, the fixpoint is : $Atom \cup And(res, res) \cup Not(res) \subseteq res$ which computes correctly the fact that the $Or$ has been removed. | + | res = S_1 \cup S_2 \cup S_3 \cup S_4 |
+ | \end{array} | ||
+ | \end{equation*} | ||
+ | We can prove that the least fixpoint is the same as the least fixpoint of | ||
+ | \begin{equation*} | ||
+ | res = atom \cup and(res,res) \cup not(res) | ||
+ | \end{equation*} | ||
+ | the last expression is a description of the solution set. We can use it later on to prove that the result does not mention 'or' syntax tree node. | ||
* [[http://theory.stanford.edu/~aiken/publications/papers/fpca93.ps|Type inference]]. Semantics of untyped lambda calculus. | * [[http://theory.stanford.edu/~aiken/publications/papers/fpca93.ps|Type inference]]. Semantics of untyped lambda calculus. | ||
* [[http://theory.stanford.edu/~aiken/publications/papers/popl94.ps|Soft typing with conditional types]] | * [[http://theory.stanford.edu/~aiken/publications/papers/popl94.ps|Soft typing with conditional types]] | ||
+ | * [[http://lara.epfl.ch/dokuwiki/doku.php?id=projects:matcheck|Verifying Pattern Matching in Scala]] | ||