Substitution-based Operational Semantics of algebraic datatypes - Computer Science Stack Exchange most recent 30 from cs.stackexchange.com 2019-08-22T07:51:39Z https://cs.stackexchange.com/feeds/question/33506 http://www.creativecommons.org/licenses/by-sa/3.0/rdf https://cs.stackexchange.com/q/33506 1 Substitution-based Operational Semantics of algebraic datatypes choeger https://cs.stackexchange.com/users/24132 2014-11-25T11:43:29Z 2015-02-27T00:19:05Z <p>Assume, I want to define the operational semantics for some subset of ML.</p> <pre><code>e ::= \\x. e | e e | c | match e with p+ | A e* v ::= ... | \\x. e | ... | A v* p ::= A p* -&gt; e | x </code></pre> <p>Where <em>e</em> is the expression language, <em>v</em> are the values or normal forms, <em>p</em> are the patterns and <em>A</em> are the constructors for my algebraic datatypes. </p> <p>Also assume I want to define the semantics based on substitution, not on environments. Finally, the language should be typable, e.g. every constructor will only be allowed to be applied to the same number of arguments. </p> <p>So I assume, I have to introduce a "construct" operation and a "data declaration" and then substitute every constructor with an appropriate datatype declaration. But how does one define this "construct" operation? And how does the data declaration look like in an untyped calculus?</p> https://cs.stackexchange.com/questions/33506/-/33605#33605 2 Answer by choeger for Substitution-based Operational Semantics of algebraic datatypes choeger https://cs.stackexchange.com/users/24132 2014-11-28T23:13:11Z 2014-11-28T23:13:11Z <p>I found the solution to my answer: ADTs can be represented by a combination of sum-types and tuples <a href="http://books.google.de/books?id=ti6zoAC9Ph8C&amp;pg=PA133&amp;lpg=PA133&amp;dq=sum%20type%20inject%20left%20right&amp;source=bl&amp;ots=EBFguCoXXG&amp;sig=5-Eep5FmYPUwFsxsYAj35pJ2wZc&amp;hl=en&amp;sa=X&amp;ei=OwB5VI7gDYT4ywOezIKYDA&amp;ved=0CCsQ6AEwAg#v=onepage&amp;q=sum%20type%20inject%20left%20right&amp;f=false" rel="nofollow">enter link description here</a>. In that representation, every construction takes exactly one argument (possibly the unit value). </p> <p>Two special tagging forms, inl and inr for "inject left" and "inject right" are introduced. These forms allow the encoding of arbitrary tags. So every constructor is a one-argument function that applies the corresponding tag. </p> <p>Hence, any data structure definition is operationally defined by the constructing operations:</p> <pre><code>data A | B | C =&gt; let A = \\x. inl x in let B = \\x. inr (inl x) in let C = \\x. inr (inr x) in </code></pre> <p>The corresponding pattern can be substituted similarly.</p>