# Differences

This shows you the differences between two versions of the page.

 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) 2008/05/22 12:11 vkuncak 2008/05/22 00:13 vkuncak created Next revision Previous revision 2008/05/22 12:11 vkuncak 2008/05/22 00:13 vkuncak created 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]]