3 ms·

> It can also be quite possible to invent structures which are valid but have no valid path to creating them. I'm curious if you have an example of such a stru

• Normal_gaussian 7mo ago
  You are quite right to call this out - and quite right in general. With AST verification alone your statement holds strongly. I was remembering a professor I had who was very into formal verification and had an IDE that would only accept valid programs - however his validity checks were more than just tree based, they involved passing a type check. Which now you've called me on it, is quite definitely beyond valid AST editing. The base case: if you have a structure with a mandated cyclical reference that doesn't accept a second (e.g. nil) type, you cannot construct it without creating an intermediate invalid program. This doesn't tend to show up if the cyclical reference is all the same type (A1 -> A2 -> A1) because you can often cheat and self reference, but it does if it is different types (A1 -> B1 -> A1). You can't construct an A without a B, which cannot be constructed without an A. But that's still not a problem you cry! And quite right, you can edit the type itself to remove and re-add the reference. That is until the type is built into the language, or a library.
• integralid 7mo ago
  OP clarified, but I understood that as a valid tree without a path to empty node. I don't have an example, but with grammar weird enough it sounds plausible. Especially if some form of type checking is involved, as OP mentioned.