Substitution-based Operational Semantics of algebraic datatypes Assume, I want to define the operational semantics for some subset of ML.

e ::= \\x. e | e e | c | match e with p+ | A e*
v ::= ... | \\x. e | ... | A v*
p ::= A p* -&gt; e | x


Where e is the expression language, v are the values or normal forms, p are the patterns and A are the constructors for my algebraic datatypes. 

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. 

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?
I found the solution to my answer: ADTs can be represented by a combination of sum-types and tuples enter link description here. In that representation, every construction takes exactly one argument (possibly the unit value). 

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. 

Hence, any data structure definition is operationally defined by the constructing operations:

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


The corresponding pattern can be substituted similarly.