1
$\begingroup$

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?

Improve this question
$\endgroup$
6
  • $\begingroup$ You would need to say what your "construct" operation does. What does it construct? $\endgroup$ – Dave Clarke Nov 25 '14 at 12:29
  • $\begingroup$ The "construct" operation should create the value of one algebraic data type. The simplest way would obviously be to combine the constructor (or tag) A with the values that were passed to the constructor. $\endgroup$ – choeger Nov 25 '14 at 13:32
  • $\begingroup$ I don't understand what you're after. Do you want to add a semantics for datatype definitions (e.g. 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
  • $\begingroup$ That would be the first step. The substitution would look like [A := ..., B := ...] and the part in the ellipsis is what I currently don't know how to define. $\endgroup$ – choeger Nov 25 '14 at 13:35
  • $\begingroup$ Just to clear my mind: what is the difference between a substitution and an environment ? ... since you want to replace one by the other. $\endgroup$ – babou Nov 25 '14 at 13:55
2
$\begingroup$

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  

=>

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.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.