JSAbrahams / mamba

🐍 The Mamba programming language, because we care about safety
MIT License
85 stars 3 forks source link

More explicitly document the type system #452

Open JSAbrahams opened 1 year ago

JSAbrahams commented 1 year ago

Many type system features are now kind of clear, but not wholly. In the sense that I have a broad sense of what I want to achieve, but many design decisions are left vague. Luckily, there's a lot of work on type systems done over the decades which we can leverage. We should more completely document the type system to:

In a general sense, our guiding philosophy is that Mamba should be as flexible as possible. We are not implementing a systems language, so we don't have to worry as much about stack vs. heap shenanigans. But, if the check stage passes, then the application should be well-typed, in the sense that (not exhaustive perse but close I assume):

Implicitly the above also ensures that:

Of course, we can't always guarantee the above if we call Python code. For that we need an unsafe operator, see:

Questions such as:

What about the following?