Document and explain the language hierarchy

[nrnrnr]

Right now, we are interested in this hierarchy:

1. For P-plus we will have simply patterns plus side conditions

2. For V-minus we will have the guarded expressions from today's board, where the right-hand side is a type variable

3. For our target language we will have the decision trees from today's board, where the right-hand side is a type variable.

4. Make a placeholder for an eventual target language, e.g., terms in ML. ML terms might manipulate constructed data defined as follows:

   type vcon = string (* value constructor *)
   datatype data = CON of vcon * data list   (* constructed data *)

We are looking for a formal definition (grammar) for each language in the hierarchy and an explanation of how it fits into the larger story we are trying to tell. This is the path through the woods; so keep each level as simple as it can be while still telling its part in the story. We can add more exciting features on the next pass.

R's edit:

Also, discuss how adding an annotated type:'a decision-tree, 'a guarded-exp -- buys us a closer translational equivalence.

Answer these questions:

What are we trying to solve? What does a type variable buy us in this process? How does it confine the 'versiness?' More broadly, what are we doing here and why? These will likely be sections of the paper.

[rogerburtonpatel]

tex/syntax-and-judgement/syntax-judgement-P.pdf,, tex/syntax-and-judgement/syntax-judgement-V-.pdf, tex/syntax-and-judgement/decision-trees.pdf, tex/paper-sections/big-picture.pdf

[nrnrnr]

Next step here: make it look like the first sections of the Verse paper.

[rogerburtonpatel]

Closed wrong issue

[nrnrnr]

This issue was assigned to both of us, but I couldn't find a task for myself, so I removed myself from the assignee list.