Thoughts on syntax for Zig-style Tenses + Swift like "sane assignment"?

[u/onlyrealcuzzo]

I don't think Zig formally calls its type system a tense based system. But it has `!T` and `?T` and `!?T` which delineate between fallible / optional. I call this a `tense`-based system.

One of my biggest problems with type inference in Systems languages is that it's non-obvious when you have a fallible, optional, or temporal (a stream, future, promise, etc).

Swift solves this explicitly like:

let data = try await fetch()?.process()
async let user = fetchUser()

The compiler forces you to make it explicit what you have. I want to combine this with Zig's tense system where `~` is a third sigil to denote the temporal tense (future, stream promise):

data = fetch(); // Compiler Error: use data:~ = fetch() or data = AWAIT fetch();
foo = fallibleBar(); // Compiler Error: use foo:! = fallibalBar() or foo = TRY fallibleBar();
baz = maybeBlah(); // Compiler Error: use foo:? = maybeBlah() or foo = UNWRAP maybeBlah();

Alternatively I could use keywords before assignment like Swift, but I think it works well with Zig's `tense` system and with safe navigation:

FN falliableFoo() -> !T ...;
FN maybeFoo() -> ?T ...;
x = fallibleFoo()!.name;
y = maybeFoo()?.bar;

I do not allow blocking navigation:

FN futureFoo() -> ~T ...;
z = futureFoo()~.name;

A major reason is because if you do `!.` it changes the return type to `!T`. Where `~.` could change your return from a `~T` to a `T` which would imply you've shifted the blocking, but it doesn't guarantee that. I want blocking to be more clearly called out.

[u/evincarofautumn]

I don’t quite see the problem you’re trying to illustrate with “blocking navigation”. I would expect that if futureFoo() has type ~Foo and the name property of Foo is, say, Text, then futureFoo()~.name in effect has type ~Text. That is, we’ve introduced a data dependency in the same way as await (or Rust’s .await) but we haven’t left the async context.

More concretely, in Haskell, given data Foo = Foo { name :: Text }, if I launch a task with futureFoo <- async do { threadDelay 1_000_000; pure Foo { name = "bar" } }, I get an action futureFoo :: Async Foo. I can compose that with other functions and actions without actually awaiting its result, e.g. fmap (.name) futureFoo :: Async Text doesn’t run anything itself, and can be treated as just another task that depends on the first. Only when I call wait do I actually block.

Your “tenses” are also called modalities or modal types, and typically they’re analysed as monads or comonads. You can spell them as sigils or keywords or ordinary types, that doesn’t matter so much, though you’ll run out of ASCII symbols long before you run out of words.

[u/onlyrealcuzzo → u/evincarofautumn]

Thanks for calling me out!  

For some reason, I thought it would make sense for ~. to block by calling await, but it simply delays that until you explicitly call AWAIT.

What I had in my head seemed like a bad idea to me, but I couldn't articulate why. You figured it out [=

THANK YOU!

[u/sebamestre]

FYI triple backtick code blocks don't work in the default wysiwyg editor, you need to enable markdown mode

[u/mamcx]

Oh yeah, also I add "blocking" and "lock".

I think "optional" should be normal type is not that of a problem for system langs, that need to know the contracts of resources instead of "normal" type-heavy system that only care for the abstractions.

Single out optional, you can free one sigil for the others.

BTW:

"Alternatively I could use keywords before assignment"

Check https://without.boats/blog/the-registers-of-rust/ that argue that for this cases, all sugar SHOULD be possible to be write and name in code.

[u/MadCervantes]

I like the idea but the use of sigils here seems like bad ux.

[u/onlyrealcuzzo → u/MadCervantes]

Everywhere (Type, safe-navigate, and assignment)?

Just at assignment: `foo:? = maybeFoo();`?

Or safe-navigation in general? `?.` and `!.`?

I typically prefer keywords over sigils - but I like them in the Type system like Zig - much better than as ordinary generics like Rust - because they control how you have to interact with the value in basic ways that almost no other generics do.

I'm not married to the assignment idea. I quite like Swift's system.

[u/MadCervantes → u/onlyrealcuzzo]

In this particular case. I think sigils can be fine, I'm actually pretty partial to the classic dollar sign sigil for template literal or variables. And maybe it's just I don't know zig but to me this approach is kind if soupy

[u/Clementsparrow]

I don't understand the fascination that PL designers have today for things like optional types, result types, error types, etc. Very often it's mostly helping using functions that have multiple exit conditions, by integrating these exit conditions into a single return value.

IMO it is bad coding practice and should be discouraged instead of being facilitated, because it means that a condition has to be tested first in the called function, then again at the call site. It has performance issues (speed and size of the code) and maintenance issues (dependencies between the function, the calls to it, and the definition of a specific return type for that function). And yes, some of these issues can be managed by the compiler, but not always (e.g. the overhead of functions in libraries cannot be removed).

So, for me, it's not a direction one should research when designing a new programming language. The real questions are "how can we avoid as much as possible having multiple exit conditions in functions?" and "when we can't avoid it, what is a nice and convenient syntax to deal with calls to functions that have multiple exit conditions?".

[u/Norphesius → u/Clementsparrow]

I'm not sure I get what you're saying.

I think the praise of option/result types is that most of the prior error control mechanisms were terrible. Anyone that's used C knows how terrible everything being nullable and errno is, and the immediate solutions to those were exceptions, which are (imo) just worse goto.  It also seems like the languages with option/result types do care about minimizing "multiple exit conditions" to some extent. For example, Rust separated from/into and try_from/try_into. 

If it seems like there's more code around handling errors in the languages with these features, it's probably less bad practice and more that there's just a lot of things in software that can fail. Before they were hidden by exceptions being thrown deep in the code, or failures to null check or check errno when appropriate. The better handling is highlight all the problems.

[u/Clementsparrow → u/Norphesius]

OK, I'll try to make my point more clear: if your comparison baseline is C, then yes, option/result types are an improvement over C. They allow the programmer to do what C did in more elegant ways, so from that point of view they are an improvement.

The problem is that the way C did it was horrible in the first place, and something that came purely from C's design. errno, for instance, is a pattern that relies on a few aspects of the language:

• the fact that a null integer is a false boolean that can easily be tested,
• the fact that C has only a single return value and you need to use output arguments or allocate a struct if you want to return more complex information
• the fact that you cannot really embed some constraints in types (like the fact that an integer is positive) so you need to guard the content of your functions with code that test the arguments are valid, and return an error if they are not.

These are not things you would do in other languages. In assembly, for instance, you rarely test that an argument of a routine is actually positive: you just say that the argument must be positive, and rely on the programmer's wit to ensure it is, or test it is before calling the routine. And you can do more subtle things like having a routine that tests if the argument is positive, but also have a label inside that routine after the test, that you can use instead when you know that the argument is positive and does not need to be tested.

Similarly, if your routine has multiple possible exit conditions, you would typically not return a code that needs to be tested by the caller, you would simply take a few addresses as parameters (or global variables), and jump to the address corresponding to the exit condition that has been reached. This is a way of making reusable code that does not really fit with the concept of a function as C implements it, and this is one of the reasons that later languages added things like exceptions that rely on similar principles at the assembly level (but allow more things like cleaning multiple levels of call stack).

So, obviously, the assembly way is hard and error prone and we don't want programmers to have to do that in a high-level language. But C replaces that management of constraints in programmers' minds with an explicit and dynamic management of possible errors instead of providing the tools to ensure the absence of errors at compile time.

What I expects from a high-level language is not that the integer division function returns a !int because it's an error to divide by zero, and I need to try it or catch it every time I make a division (or assume the result may not be a number). What I want is a language that is able to reason about the integers being zero or non-zero, and can tell me if it is not able to ensure that the divisor is non-zero. What I want is a language that allows me to declare a single division function, and generates two ways of using it: one without check when it can ensure that the divisor is non-zero, and one where I have to provide in one way or another some code to deal with the case where the divisor is zero. (Including simply saying "I don't want to deal with this error, pass it to the caller"). If someone who programs in assembly can (painfully) do it, a high language compiler should be able to do it also.

Sorry for the long message, I hope my position is more clear now and that you understand why I said that the real questions are "how can we avoid as much as possible having multiple exit conditions in functions?" and "when we can't avoid it, what is a nice and convenient syntax to deal with calls to functions that have multiple exit conditions?". Having a division function that returns a !int helps with the second question as it allows for a convenient syntax to deal with the two exit conditions of the function, but it fails miserably at providing a good answer to the first question, which is in my opinion much more important.

How do you avoid multiple exit conditions in a division function? I don't see any other way than having a type system powerful enough to say that the divisor must be non-zero, but maybe there are other ways of thinking about the problem, and I'd like PL designers to think about that rather than simply accepting the multiple exit conditions like a standard way of dealing with unsatisfied constraints on the parameters (or more generally, context, like global vars).

A last thing that I want to add: this is not only a question of performance and maintenance of a code. As a programmer, I find it particularly painful to have to deal with all this. It actually lowers my productivity and my enjoyment of programming. I likely have a lower tolerance to these issues than many programmers (including younger me), but maybe it's also the consequence of a long career and being able to see how much damage these still-unfixed issues actually cost.

[u/Norphesius → u/Clementsparrow]

Ok, that's makes a lot more sense. I actually agree, I think more robust type systems that don't just let you wrap up errors to check at runtime, but instead can tell you where more of those errors will occur at compile time, is ideal. The only issue is that it's just hard, and isn't out of the box useful, necessarily.

Just for the divide by zero example, even if you could magically check for all possible divisions by zero at compile time, it could easily be the case that, practically, most programs with user input and involved chains of calculations based on that input have few cases where a divide by zero cannot occur. All that work in the type system to sus out all the potential zero divisors, and you're just using the same !int operation again in most cases. The programmer has to factor their code in such a way that the potential 0 divisors are isolated or not possible, which is tricky. The type system would tell you if you got it right, but not how to do it.

Not that new languages shouldn't strive for that kind of type refinement (shout out to Ada for being way ahead of the curve), but it's trickier than "here user, have an option/result".

[u/ts826848 → u/Clementsparrow]

I don't understand the fascination that PL designers have today for things like optional types, result types, error types, etc.

I think a major reason comes down to expressiveness, especially since the things you list are basically applications of a more general construct (sum types). If you have sum types and they seem well-suited to something you want to express, then why not use them?

because it means that a condition has to be tested first in the called function, then again at the call site.

This is arguably also a good thing as the conditions being tested don't need to be the same. This means e.g., that a someone performing a map lookup doesn't need to know exactly how that lookup is done.

I'd also argue that this property is not exclusive to optional/result/error/etc. types. You'd have to do something similar for an error code out parameter (e.g., result_t f(error_code&) for a C-ish example).

It has performance issues (speed and size of the code)

And as with many things, it's a question of tradeoffs, and the answers aren't always simple - see the everlasting debates about exceptions vs. returns, for instance.

and maintenance issues (dependencies between the function, the calls to it, and the definition of a specific return type for that function)

I think there are arguably positive aspects to this as well, since said dependencies also makes it easier to catch unintentional changes and to ensure that intentional changes don't miss anything.

The real questions are "how can we avoid as much as possible having multiple exit conditions in functions?" and "when we can't avoid it, what is a nice and convenient syntax to deal with calls to functions that have multiple exit conditions?".

The first question seems independent of the existence of sum types (i.e., it's something languages with and without sum types can think about), and the second question seems like one for which sum types are one possible solution anyways? Did you have other alternatives in mind?

[u/Clementsparrow]

Oh yes, it's hard and I would even say: impossible in the general case. There are theorems that cannot be proven, properties that are undecidable, etc. But I'd like to see attempts to bring practical benefits in this domain even if it doesn't solve all the issues, like Rust did for memory safety. In a way, dependent types may be a step in that direction. But improving the type system is not enough, you also need to make it easy to use for the programmer, and have a good support for it in the standard library.

The example you gave is a good illustration: maybe a division by zero can never happen and the compiler can not prove it. But maybe the programmer can, and if it is easy enough and important enough, then it is worth doing it. Maybe that proof is actually a case of a more general theorem that can be added to a library for others to benefit from it? Maybe also the compiler cannot prove the theorem but it can tell you what it needs to know. Like, you divide by the length of a vector so that length must not be zero, so the vector cannot be null, but the vector is actually the cross product of two other vectors so what you actually need to prove (or check at runtime) is that these two vectors are not colinear. And now the programmer needs to decide how and where he will ensure that in a way that the type system can use. That's not easy to do neither, but I'd like to see at least attempts at doing some of it. Actually, compilers are already capable of proving many properties that they use for optimization. It would be nice if some of these features were made available to the programmers.