• English only

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)
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 : $= \lbrace AtomAnd(\_ ​\_)Or(\_ , \_), Not \_ \rbracewhich is an infinite set ("​_"​ represents any kind of type).+We represent values of this data type as ground terms in language ​$= \{ 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]]