Typechecking

[dmbarbour]

I really should develop a typechecker for ABC. Or perhaps more than one type checker. I have a lot of ideas, at the moment, but I feel I need a lot more progress on data structures to proceed with these ideas.

Multiple Type Systems

In AO, I could potentially have multiple typecheckers the way I have multiple test. words today.

I like the idea of having multiple, pluggable type systems and linters, each able to cast yay or nay votes for any given subprogram. I like the idea that developers who use difficult-to-typecheck idioms are free to build a recognizer for these specific use cases. I also like the idea of pursuing 'soft' typecheckers that work with confidence levels other than binary.

An interesting possibility is to also have cooperative type checkers, e.g. based on a blackboard metaphor, or a monotonic variant, which may have varying levels of trust in one another. If it can also be made reactive, i.e. such that it's easy to excise and rebuild all nodes with a common dependency (on either a typechecker or a slice of code), then we could also keep type information continuously in our programming environments. The same blackboard might remain useful for guiding optimizations.

However, cooperation does introduce a challenge of ensuring compatible type descriptions.

Declared Types

AO and ABC don't have any form of type declarations at the moment, which means they rely entirely on type inference. Inference can be useful, but it can be difficult to isolate type errors or enforce parametric polymorphism. I would like to support type declarations, or at least something similar to type declarations.

Assuming I have some way to describe the types, the actual declaration shouldn't be too difficult to represent. I can use a naming convention in AO, similar to the current test. words. (It would be nice to typecheck not just specific words, but arbitrary blocks.)

The type descriptors are again relevant a challenge. If I have multiple type systems, then I don't want to have implement a different type declaration for each system. I want to declare types just once, and check the declared type in many systems.

Type Descriptors

Type descriptors in AO will be constructed concatenatively; they're just values, and can be abstracted like anything else. I would like type descriptors to be composable. And it would be really nice if they can generate sample values for property testing or probabilistic testing. We need types to be relatively easily processed, refined, and unified.

I can potentially model 'parametric polymorphism' in terms of sealed value types. A lot of design work to do here, especially if I want multiple type systems to work together effectively. I wonder if type descriptors might be best modeled in terms of grammars?