>>86684956Types are already constrained to what a programmer foresees.
In a library, you can only call functions with the documented types. Otherwise it would be undefined behaviour.
In local code, you can just change the type of any function which is not general enough.
The result is the same in both static and dynamic.
The existence of a typed lisp is trivial.
It is reasonable of me to assume that a file of typed lisp code could be statically checked checked.
You can take a set of REPL evaluations (the state of the interpreter) and turn them into a file of code.
Therefore any state of the interpreter can be statically verified, and an updated state can be re-verified.
You could accomplish this by keeping graph of which objects reference which names.
Then when a name's type is redefined, you recheck the functions values that reference it (you would only need to recompile them if you did unboxing optimisations).
This probably wouldn't cause much lag at all, but if you think it would be to much, you could just provide the checking function to the user.
Calling this function would then report any type errors.
Critically, this doesn't stop you from submitting type invalid code and doesn't force a monolithic compilation model.
It's fine for the system to exist in invalid states, static typing only means that the errors in those states can be reported to the user before the code runs and fails.
Just as updating a function can invalidate others which call it, the re-checking could validate functions which were wrong before.
An undefined value could easily be used before becoming defined in this way.
