I'm sorry, I don't think I understand your message and my answer might be off as a result. Could you link to the current research on more general solutions than Checker, so I can get a clearer picture?
> a type system limitation that every type describing side effects [...] can only be used in the context of a compiler/interpreter.
A type system is just a logic description of a property that a program might have. It specifies how the language constructs interact with this property []. The fact that compilers use a type system is independent of your ability to write your custom type system, or to use it in a different context (IDE, toolchain, ..).
[] Are you saying that a type system shouldn't be concerned by the AST of the language?
Also, I don't understand why you distinguish "typing side effects" as something different from the rest?
> you need to write a different type system for each property
But you do have to define your type system at some point?
Are you thinking of something like Mezzo, where some userland properties can be defined without going down the type-system-definition road? https://protz.github.io/mezzo/
> But the interactions can, and should be more interesting, and take into account the order in which the callees are called etc.
That's why type systems are defined with respect to the language construct, by rules on the AST (? I'm confused because of the earlier [*] here).
To go back to Agda significance for a custom type system, it's not enough to define a type system. You generally want to prove that your definition is valid: If your "checked exceptions" says that a program `P` can't fail due to an exception, you want to check that you didn't forget anything by verifying the type checker with respect to the actual semantic of the language.
You can also embed your custom property into Agda type system (isn't that what you want?).
I am not a type theory expert (or even enthusiast) by any means, but I imagine something that will be very useful like so: the intersection types of callees interact in interesting ways with the type of the caller (taking into account ordering). For example, the type of the caller can be: "this function locks A, then B, then unlocks B, then unlocks A". This type can arbitrarily intersect other effect types, such as: "this function writes to socket X" and also "mutates variable V".
I will be able to define a type "locks A" and "locks B", and the kind "locks" will be ordered, so that the type of a function that locks A and locks B, will be "locks A and then locks B". Also, I will be able to define interactions between types so that unlocking A will undo the effect, so that a function that simple locks A will have the type "locks A", but one that locks and later unlocks will have the type "holds A". Of course, these types intersect arbitrarily.
> a type system limitation that every type describing side effects [...] can only be used in the context of a compiler/interpreter.
A type system is just a logic description of a property that a program might have. It specifies how the language constructs interact with this property []. The fact that compilers use a type system is independent of your ability to write your custom type system, or to use it in a different context (IDE, toolchain, ..).
[] Are you saying that a type system shouldn't be concerned by the AST of the language?
An external type checker for Haskell: http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/blog/2013/0... And the various type checkers for the not statically typed languages (python, ..)
Also, I don't understand why you distinguish "typing side effects" as something different from the rest?
> you need to write a different type system for each property
But you do have to define your type system at some point? Are you thinking of something like Mezzo, where some userland properties can be defined without going down the type-system-definition road? https://protz.github.io/mezzo/
> But the interactions can, and should be more interesting, and take into account the order in which the callees are called etc.
That's why type systems are defined with respect to the language construct, by rules on the AST (? I'm confused because of the earlier [*] here).
To go back to Agda significance for a custom type system, it's not enough to define a type system. You generally want to prove that your definition is valid: If your "checked exceptions" says that a program `P` can't fail due to an exception, you want to check that you didn't forget anything by verifying the type checker with respect to the actual semantic of the language.
You can also embed your custom property into Agda type system (isn't that what you want?).