Hacker News
points by poly2it 2 days ago | 0 comments
You might consider it type safe according to C's rules, but it is not type safe according to contemporary opinion because the success type and error type are the same.
[–] eru 2 days ago
> [...] because the success type and error type are the same.

That's a bit weird? In Rust, if you have an thing that returns Result<String, String> that's still type safe, even though success and error types are the same.

I think I understand what you want to express, maybe. You might say it's in-band vs out-of-band error signalling?

[–] itishappy 2 days ago
> In Rust, if you have an thing that returns Result<String, String> that's still type safe, even though success and error types are the same.

These types are not the same:

    Ok<String>
    Err<String>
[–] markasoftware 2 days ago
Those are not types at all. Ok and Err are type constructors for the Result<A, B> type that take arguments of type A and B respectively.
[–] SkiFire13 2 days ago
> type constructors

Nit: the type constructor is `Result`: given two types `A` and `B` (not instances of those types, but actual types) it gives you a new type `Result<A, B>`.

`Ok` and `Err` are called "variants" and can be used to construct a new _instance_ of `Result<A, B>`.

[–] markasoftware 1 day ago
Ah, thanks! I'd remembered the term "data constructor" from Haskell and called it a type constructor instead.
[–] kazinator 1 day ago
Ok and Err are "thingies" which are in the type system, which give rise to distinctions that allow for compile-time diagnostics. They are part of the type.

Ok and Err are not just type constructors because they appear on the left hand side in pattern matching: they "do" matching and destructuring also.

[–] kazinator 1 day ago
The success and error types are not the same, because they are in different positions in the type, and so distinguished by different patterns.

If you have literally the above convention where a valid result is a String, and an error result is also a String (e.g. error message) that is still type safe.

  match (whatever()) {
    Ok(s) => println!("good result string: {s}"),
    Err(s) => println!("error string: {s}"),
  }
The success type and error type having to be different is not a good way to express the idea; rather that success and error cases are distinguished by type (even if the success and error data units are of the same type).

In other words, the "Ok" and "Err" entities are an ingredient of the type and that effectively makes the result and error be distinguished at the type level.

But we could also argue that Rust still allows you to write an integer-returning function such that -1 means error.

[–] eru 1 day ago
Basically, you need the whole 'success and error types are different' in a language like Python if you make the return type something like "int | string", where 'string' stands for your error message.

Of course that breaks down, when the success type is also an error message, eg when you are looking up something in a catalogue of error messages.

Rust has no trouble with this, for exactly the reasons you line out.

[–] quotemstr 2 days ago
Contemporary opinion among who? Words mean things, and "type safe" simply does not mean "agrees with my preferred style of error reporting"
[–] poly2it 2 days ago
Papers on type soundness from the last 30 years usually explore the domain further than C semantics.
[–] pron 2 days ago
Soundness means that the program behaves in accordance with what its types express. You're right that C may be unsound due to undefined behaviour, but I don't think this is about soundness. What you're saying is that papers on types show how you can use types to express more constraints.
[–] ranger_danger 2 days ago
There can be other valid perspectives and definitions of that word than yours.

I think almost all (tech) arguments stem from simple disagreements and/or different assumptions made on the definition of a (subjective) term.

[–] pron 2 days ago
You may be right in general, but soundness comes from formal logic, where they're pretty fastidious with their definitions. Soundness certainly doesn't mean the expressivity of the types (i.e. what constraints they can represent); it's about the relationship between the runtime behaviour of a program and the types in the code.
[–] ranger_danger 2 days ago
Again I think you're trying to push a specific definition as more correct than OP's somehow. Why not just ask them what they meant to understand their intent/context instead of saying they are wrong?

Unless the point of your argument isn't to understand OP but simply to "win."

[–] pron 1 day ago
I think I understand their point and even said, "What you're saying is that papers on types show how you can use types to express more constraints," and that's correct. I merely pointed out that that's not soundness, which is something I think they'd like to know. There may be some leeway in the definition of soundness and how it's similar to or different from type safety, but either way, type expressivity is something different altogether (and C certainly has issues with both expressivity and type safety or soundness, but they're different issues). So the point isn't to win - the argument was right and I'm not claiming that C's type system is expressive - but to explain the different terms and their meaning in programming languages and formal semantics.
[–] ciefa 2 days ago
Can you link some?
[–] quotemstr 2 days ago
That's not the same as asserting that soundness requires adherence to the current fashion, sum types over results and errors. TIMTOWTDI.

You don't have to think C is sound or good to distinguish a disfavored API style from mathematical unsoundness. There are infinitely many type safe APIs and languages that are, despite their soundness, ugly and hard to use.

Let's not project every dimension along which a language can be good or bad onto the axis of safety.

[–] majorchord 2 days ago
Opinion among people who know better than to try to authoritatively explain subjective words with rigid dogma, because that just makes them look silly.