Extend soundness appendix #406
Conversation
|
|
||
| .. math:: | ||
| \begin{array}{llll} | ||
| \production{context} & C &::=& | ||
| \{~ \dots, \CRECS ~ (\deftype^\ast)^\ast ~\} \\ | ||
| \{~ \dots, \CRECS ~ \subtype^\ast ~\} \\ |
There was a problem hiding this comment.
the hyperlink on \CRECS doesn't seem to jump to a helpful place right now - is this where \CRECS is defined?
There was a problem hiding this comment.
Yes, that has been the case for all grammars: at their definition site, the hyperlinks generated by the syntax macros essentially jump to themselves. Admittedly slightly confusing at times.
|
|
||
| - Either :math:`\X{ht}_k` is a :ref:`defined type <syntax-deftype>`. | ||
|
|
||
| - Or :math:`\X{ht}_k` is a :ref:`type index <syntax-typeidx>` :math:`y_k` that is smaller than :math:`x`. |
There was a problem hiding this comment.
Is it possible to have a mixture of type indices and recursive type indices here? Can you give me more of an intuition about this? I thought that the process of unrolling/rolling meant that you would always have either one or the other.
There was a problem hiding this comment.
No, it's not, good point. I added a clarifying note to valid/conventions, where the generalised syntax is introduced.
| \end{array} | ||
| \end{array} | ||
| }{ | ||
| \vdashstore S \ok | ||
| } | ||
|
|
||
| .. note:: | ||
| The validity condition on type instances ensures the absence of cyclic types. |
There was a problem hiding this comment.
Why is this deleted? Is it no longer true? If so, why?
There was a problem hiding this comment.
This note has been outdated for a while, I just missed it. We no longer have type instances. And since we no longer have indirections through a type store, types are closed syntactic terms and hence non-cyclic by construction.
| @@ -382,7 +658,7 @@ Module instances are classified by *module contexts*, which are regular :ref:`co | |||
| :ref:`Module Instances <syntax-moduleinst>` :math:`\moduleinst` | |||
| ............................................................... | |||
|
|
|||
| * Each :ref:`defined type <syntax-deftype>` :math:`\deftype_i` in :math:`\moduleinst.\MITYPES` must be :ref:`valid <valid-deftype>`. | |||
| * Each :ref:`defined type <syntax-deftype>` :math:`\deftype_i` in :math:`\moduleinst.\MITYPES` must be :ref:`valid <valid-deftype>` under the empty :ref:`context <context>`. | |||
There was a problem hiding this comment.
To confirm, types in module instances aren't stored in their rolled form?
There was a problem hiding this comment.
No, they are assumed to be rolled up (and closed), see also the definition of alloctype (which I tried to make a bit more readable). But of course, in terms of wf rules for instances, that does not materialise as an observable constraint, since any 1-step unrolling is also a valid defined type, and you can construct a(nother) module that produces that.
For example,
(module $A
(rec (type $t1 (array (ref $t1)))
(rec (type $t2 (array (ref $t2)))
)
(module $B
(rec (type $t1 (array (ref $t1)))
(rec (type $t2' (array (ref $t1)))
)
are both valid modules, but in the instance of $B, the deftype for $t2' would to look exactly like the unrolling of $t2 in $A.
|
@conrad-watt, I also added the cycle-freedom condition. Fixes #332. |
|
And fixed a bunch of oversights in the rules for tail calls, which I forgot to adapt for subtyping after the rebase. Fortunately, this was implemented correctly in the interpreter. |
Also, kill a few related todos.
@conrad-watt, PTAL.