Substitution-based Operational Semantics of algebraic datatypes
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.