The attempts to write down all the rules we obey when designing the language along with their justifications.
It is a goal of dark to allow bad/invalid/incorrect programs to run, at least until they hit the bad parts of the code.
Compiled languages, and especially statically typed functional languages can be frustrating to write, because they need to be fully and correctly typed to compile, and hence to run. This means that you have to complete all parts of your code (or use language mechanisms like todo() or assert false manually) to run your program.
However, we believe this is frustrating to developers (and it has been frustrating to us). More than once I’ve spent an hour on an edit, carefully following all the type errors until the program compiles successfully, only to discover the edit was flawed when the program runs.
Instead, we’d like users to be allowed make local edits and run the code, and if they had invalid types or other invalid code, it will error when it is evaluated.
We still want to warn users about invalid code, and provide full and comprehensive type checking facilities. All that this is saying is that they aren’t required to be fixed or satisfied for the program to actually run.
In darklang classic, we had some explicit allowances in ProgramTypes to support this, such as EPartial, ELeftPartial, ERightPartial, DIncomplete, EBlank, allowing { ___ : ___ } in records, etc. This was to support programs that were partially written in the live editor, but this is conceptually the same idea.
For generating AI, the AI may generate code that isn’t strictly valid in Darklang, but is valid in other languages like dark. In order to support it, we need to be able to represent it in ProgramTypes, in order to type check it and maybe run it, so that we can refactor it into good code.
Examples:
NonExistantType.X 5 is allowed (errors when evaluated)MyRecord {} is allowed (errors when evaluated)\\ -> 5 (errors when evaluated)If a user inserts an Int into a List<String>, it might be tempting to say “they haven’t used this yet, it’s not an error”. However, as soon as that code is run, there is a real logic error on this code path. If the user was allowed to keep going, they would compound this error and end up with a program that does not type check and has logic bugs.
That implies that while programs are allowed to be invalid, we error early on executed paths. We want the benefits of strong type checking on any path that the user is working on.