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* -> 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?
datatype t = A | B; \x. match x with A -> B | B -> A
should reduce to(\x. match x with A -> B | B -> A)[some substitution]
)? $\endgroup$ – Gilles 'SO- stop being evil' Nov 25 '14 at 13:33