hutao

First of all, nice post! I can tell that you put deliberate effort into using a concrete example, introducing a problem and then building up to how to solve it.

However, the continuation monad has limitations. In your example, it serves a similar purpose to an abstract monad "typeclass"; where you can write an abstract "task" function and run it in the Result effect, or the Promise effect, or any other effect. However, this "task" function can only use map/bind/return, and cannot perform any specific "effectful" operation, such as throwing an error or performing async IO. At the point in the code where it performs an operation, it has to pick a concrete type for the continuation result type `t`. So, a function that performs async IO would need to return `K(Promise(b), a)`, and a function that throws an error would need to return `K(Result(b, Nil), a)`. What would be really useful would be to have a function can perform an effectful operation (such as throwing an error) and still return something like `M(b)` for some abstract effect `M`. This is one of the main problems of "effect systems," and to my understanding, what algebraic effects are currently trying to solve.

I've always felt that ML hit the sweet spot between functional and imperative programming. It affords conveniences such as algebraic data types and first-class functions, but unlike Haskell, it doesn't require monadic programming to use IO or mutable references.

ML also has an interesting module system, which achieves similar goals as object-oriented programming, but in a very different way. While mainstream "class-based" OOP identifies the data type with the unit of encapsulation, ML has "modules," which are separate entities from types, and which may both define types and values as members. However, a downside of this approach is that you sacrifice late binding, as the module language and "core" language are stratified into different layers. Instead, dependency injection is achieved through module-level functions, called functors,

A lesser-known fact is that ML originated as the scripting language for the LCF proof assistant (which is where the name "ML," or meta language, comes from). In the LCF tradition, the inferences rules of the logic are implemented in a trusted kernel, then clients use those inference rules to write tactic scripts that construct theorem objects. This design was supported by ML's module system: theorems were defined as an abstract type in a "kernel" module, and the inference rules were defined as functions inside the module. Here is a tutorial that explains the LCF design better than I can: https://www.cs.cmu.edu/~fp/courses/15317-f17/recitations/rec...

This is the gist of Andrej Bauer's paper:

- An algebraic theory consists of a "signature" (specifying a set of operation symbols with their arities) and a set of equations about those operations. An algebraic theory is purely syntactic, and does not give meaning to the operations or equations.

- An interpretation of an algebraic theory maps each operation symbol to a concrete mathematical object. It maps syntax to semantics.

- A model is an interpretation in which the algebraic theory's equations hold.

- A free model of an algebraic theory, generated by a set, is basically a model that can be mapped to any other model of the theory generated by the set.

So, an example of an algebraic theory is a group (as in the algebraic structure itself, not the various instances of a group). Its signature consists of the binary operation of combining, the unary operation of inverse, and the nullary operation of identity. The models of a group are its instances, such as the integers under additions and subtraction, or permutation functions on a set. The integers are the free group (that is, the free model of the group) generated by the set {1}.

Algebraic theories can also describe the effects of a programming language (e.g. reader, writer, or state). The free model of an algebraic effect is given by the syntax trees describing its effectful computations. Effect handlers are maps from syntax trees, transforming computations into other computations within the programming language.

On the other hand I think it would mean that things like Future and general IO wouldn't be algebraic effects.

For what it's worth, Example 2.3 in the paper states that IO is an algebraic effect, albeit one with no equations. What might be confusing is that the handler of the IO effect cannot have the level of concreteness to actually implement the IO operations. Effect handlers only map computations to computations within the "pure" programming language. From the paper:

What we still lack is a mathematical model of computational effects at the level of the external environment in which the program runs. There is always a barrier between the program and its external environment, be it a virtual machine, the operating system, or the underlying hardware. The actual computational effects cross the barrier, and cannot be modeled as handlers. A handler gets access to the continuation, but when a real computational effects happens, the continuation is not available. If it were, then after having launched missiles, the program could change its mind, restart the continuation, and establish world peace.

Here is an article by Andrej Bauer answering the exact question, "What is algebraic about algebraic effects and handlers?": https://arxiv.org/abs/1807.05923v2

Contrary to the claim from the comment you are replying to, according to Andrej Bauer, "algebraic" does not refer to the composition of different algebraic effects via composing their handlers.

When you see "algebra," think "algebraic structure," i.e., a set of operations and a set of equational laws on those operations.

An algebraic effect consists of a set of effectful operations. In that sense, each algebraic effect (reader, state, etc.) defines its own algebraic structure. In theory, the operations of an effect should also be related to each other by laws. Here is an example for the state effect from Andrej Bauer's paper:

    lookup(ℓ,λs.lookup(ℓ,λt.κst)) = lookup(ℓ,λs.κss)
    lookup(ℓ,λs.update((ℓ,s),κ)) = κ()
    update((ℓ,s),λ_.lookup(ℓ,κ)) = update((ℓ,s),λ_.κs)
    update((ℓ,s),λ_.update((ℓ,t),κ)) = update((ℓ,t),κ)

However, monads that cannot be defined in this equational style cannot be translated to algebraic effects. An example is the continuation monad: https://old.reddit.com/r/haskell/comments/44q2xr/is_it_possi... (I think you are involved in the Reddit comment chain that I'm linking to...)

AFAIK, another example is the "exception" monad, because the way that you interact with it is through the handler itself. I once saw a thread on r/Haskell discussing this, but can't find it.

I'm curious about the other Stack Exchange sites. Have they seen the same decline as Stack Overflow?

Stack Overflow was the "flagship" product of the Stack Exchange company, and if the company pivots to AI, I wonder what the future holds for the other Q&A sites on the SE network.

I was not looking to disagree with your point, I only wanted to make additional commentary. Sorry if my comment came across the wrong way.

I do think "There are no function colors in Go in the way being discussed," versus "all functions [in Go] are red" are two slightly different ways of formulating the same set of facts, and the distinction between them is insightful, so that was what I wanted to touch upon. Namely, I wanted to point out that there is an "implicit" color within the programming language itself.

Go (and other language with threads) implicitly run inside the "async IO monad." In the function color analogy, what this means is that all functions are red, and the "ordinary" function call corresponds to "await" in languages such as JavaScript or C#.

Async/await is one implementation of cooperative concurrency, where the programmer must explicitly annotate the points where a context switch may occur. However, one can imagine a program transformation that marks every function as async, and makes every function call an await. After making that transformation, the async/await annotations would no longer be necessary. The end result is pre-emptive concurrency, where the runtime may potentially interrupt the active thread at any function call.

To make another analogy, Haskell requires all IO actions to run in the explicit IO monad, while most languages (C, Java, JavaScript, etc.) do not distinguish between "pure" and "impure" functions. Therefore, C, Java, and JavaScript could all be said to implicitly run in the IO monad.

Async IO is also an instance of a monad. In JavaScript, all async functions must run inside the explicit async IO monad, while Go does not distinguish between async and sync functions. Therefore, Go implicitly runs in the async IO monad. This is similar to the aforementioned distinction between cooperative (made explicit to the programmer) and pre-emptive (handled implicitly by the runtime) concurrency.

In fact, Eugenio Moggi, the PL theorist who realized monads could describe programming languages, was not looking for a programmer-facing abstraction. Rather, he was trying to describe the "implicit" monad in a programming language's semantics (such as the IO monad in most programming languages, or the async IO monad in Go).

Propagating errors up the stack is not the same, because the top-level function is not developing an error return because of the 10-level-nested function. It is developing one because the function it called has one, and apparently, it needs to return it to its local caller. It's a local consideration ...

By contrast, in a function coloring situation, if the color is wrong 10 layers down, you must change the calling function. It's a non-local consideration. You don't get to decide not to change it. You can't encapsulate it. You don't get a choice. It pollutes the entire stack, forcibly.

I think this is an interesting perspective, where I would raise a counterpoint. Both result types and async/await are instances of monads (the abstraction which approximates the article's idea of a function color, since you mentioned Haskell, I assume you know this). Just as you can "eliminate" the result type by explicitly handling the success and error cases, you could, theoretically, "eliminate" the async function by blocking on it. Doing so would treat the entire async subprogram, at the top-level function boundary, as synchronous IO, while the async subprogram would still benefit from concurrency internal to the function.

Compare Example #1:

    int topLevel() {
      return match fallibleSubprogram() {
        Ok(()) => 0,
        Err(_) => 255,
      };
    }

    Result<(), Err> fallibleSubprogram() {
      let x = f()?;
      let y = g()?;
      return h(x, y);
    }

    int topLevel() {
      block_on(asyncSubprogram);
      return 0;
    }

    async void asyncSubprogram() {
      let promiseX = f();
      let promiseY = g();
      let [x, y] = await Promise.all([promiseX, promiseY]);
      return await h(x, y);
    }

The main difference is that compared to pattern matching on Result types, programming languages typically make it unidiomatic to block on a promise. There are various reasons why this is the case, but my point is that Result types and async/await are more similar than they may initially appear.

To clarify: ML started out as a scripting language for Robin Milner's proof assistant, LCF. The formal system, or "logic," is implemented in a minimal, trusted kernel, and the proof data structure is protected as an abstract data type that can only be constructed through the trusted kernel. On top of the kernel, tactic scripts may be defined to manipulate proof objects and facilitate proof search/automation.

Then, ML grew into a general-purpose programming language (both OCaml and Standard ML are dialects).

One language that uses the tuple argument convention described in the article is Standard ML. In Standard ML, like OCaml and Haskell, all functions take exactly one argument. However, while OCaml and Haskell prefer to curry the arguments, Standard ML does not.

There is one situation, however, where Standard ML prefers currying: higher-order functions. To take one example, the type signature of `map` (for mapping over lists) is `val map : ('a -> 'b) -> 'a list -> 'b list`. Because the signature is given in this way, one can "stage" the higher-order function argument and represent the function "increment all elements in the list" as `map (fn n => n + 1)`.

That being said, because of the value restriction [0], currying is less powerful because variables defined using partial application cannot be used polymorphically.

[0] http://mlton.org/ValueRestriction

This seems to be a plagiarized paraphrase of @le-mark's comment, which was posted one hour earlier: https://news.ycombinator.com/item?id=47424625

@dang I think the account that I'm replying to might be a bot?

One of the unwritten takeaways of this post is that async/await is a leaky abstraction. It's supposed to allow you to write non-blocking I/O as if it were blocking I/O, and make asynchronous code resemble synchronous code. However, the cost model is different because async/await compiles down to a state machine instead of a simple call and return. The programmer needs to understand this implementation detail instead of pretending that async functions work the same way as sync functions. According to Joel Sposky, all non-trivial abstractions are leaky, and async/await is no different. [0]

The article mixes together two distinct points in a rather muddled way. The first is a standard "premature optimization is the root of all evil" message, reminding us to profile the code before optimizing. The second is a reminder that async functions compile down to a state machine, so the optimization reasoning for sync functions don't apply.

[0] https://www.joelonsoftware.com/2002/11/11/the-law-of-leaky-a...

Note that addition also won't overflow if one addend is greater than half the range, but the other addend is still small enough (e.g. for the range -128 to 127, adding 65 + 12 will not overflow, even though 65 is greater than half of 127).

Your intention of having the restricted domain "NonNegativeLessThanHalfMaxValue" is probably so that both addends have the same domain. If you go down that route, perhaps you'll also want the closure property, meaning that the range should also belong to the same set. However, then you have to deal with the overflow problem all over again...

The real point is that when adding two N-bit integers, the range must be N+1 bits, because the "carry bit" is also part of the output. I think this is a scenario where "Parse, Don't Validate" can't easily help, because the validity of the addition is intrinsically a function of both inputs together.

The phrasing that I hear more often is "make illegal states unrepresentable"; both the submitted article and Alexis King's original article use this phrase. At least according to https://fsharpforfunandprofit.com/posts/designing-with-types..., it originates from Yaron Minsky (a programmer at Jane Street who is prominent in the OCaml community).

EDIT: Parent comment was edited to amend the "impossible/unrepresentable" wording

Note that the division-by-zero example used in this article is not the best example to demonstrate "Parse, Don't Validate," because it relies on encapsulation. The principle of "Parse, Don't Validate" is best embodied by functions that transform untrusted data into some data type which is correct by construction.

Alexis King, the author of the original "Parse, Don't Validate" article, also published a follow-up, "Names are not type safety" [0] clarifying that the "newtype" pattern (such as hiding a nonzero integer in a wrapper type) provide weaker guarantees than correctness by construction. Her original "Parse, Don't Validate" article also includes the following caveat:

Use abstract datatypes to make validators “look like” parsers. Sometimes, making an illegal state truly unrepresentable is just plain impractical given the tools Haskell provides, such as ensuring an integer is in a particular range. In that case, use an abstract newtype with a smart constructor to “fake” a parser from a validator.

So, an abstract data type that protects its inner data is really a "validator" that tries to resemble a "parser" in cases where the type system itself cannot encode the invariant.

The article's second example, the non-empty vec, is a better example, because it encodes within the type system the invariant that one element must exist. The crux of Alexis King's article is that programs should be structured so that functions return data types designed to be correct by construction, akin to a parser transforming less-structured data into more-structured data.

[0] https://lexi-lambda.github.io/blog/2020/11/01/names-are-not-...

With Prop, I think what you need to dig into is ‘non-computational’ not ‘non-computable’.

Here's another way to explain this:

As you state, Prop has to do with proof-irrelevance. When doing constructive mathematics, proofs are programs (meaning they carry computational content), but sometimes it's useful to treat any two proofs of the same proposition as equal. As a consequence, proofs cannot be inspected or run as programs, and you get back the Law of Excluded Middle from classical mathematics.

Decidable has to do with decidability. This means that given some proposition P, there is an algorithm that can either produce a proof of P, or a proof of ~P. This is usually useful when P is a predicate, so that at each x, P(x) either has a proof or a disproof.

In classical mathematics, the Law of Excluded Middle holds for all propositions. In constructive mathematics, the Law of Excluded Middle only holds for decidable propositions. If P is decidable, it is safe to constructively assume P or ~P because an algorithm can produce the answer.

This is my point of view as someone who learned WebGPU as a precursor to learning Vulkan, and who is definitely not a graphics programming expert:

My personal experience with WebGPU wasn't the best. One of my dislikes was pipelines, which is something that other people also discuss in this comment thread. Pipeline state objects are awkward to use without an extension like dynamic rendering. You get a combinatorial explosion of pipelines and usually end up storing them in a hash map.

In my opinion, pipelines state objects are a leaky abstraction that exposes the way that GPUs work: namely that some state changes may require some GPUs to recompile the shader, so all of the state should be bundled together. In my opinion, an API for the web should be concerned with abstractions from the point of view of the programmer designing the application: which state logically acts as a single unit, and which state may change frequently?

It seems that many modern APIs have gone with the pipeline abstraction; for example, SDL_GPU also has pipelines. I'm still not sure what the "best practices" are supposed to be for modern graphics programming regarding how to structure your program around pipelines.

I also wish that WebGPU had push constants, so that I do not have to use a bind group for certain data such as transformation matrices.

Because WebGPU is design-by-committee and must support the lowest common denominator hardware, I'm worried whether it will evolve too slowly to reflect whatever the best practices are in "modern" Vulkan. I hope that WebGPU could be a cross-platform API similar to Vulkan, but less verbose. However, it seems to me that by using WebGPU instead of Vulkan, you currently lose out on a lot of features. Since I'm still a beginner, I could have misconceptions that I hope other people will correct.

Typed functional programming has the perspective that types are like propositions and their values are proofs of that proposition. For example, the product type A * B encodes logical conjunction, and having a pair with its first element of type A and its second element of type B "proves" the type signature A * B. Similarly, the NonEmpty type encodes the property that at least one element exists. This way, the program is "correct by construction."

This types-are-propositions persoective is called the Curry-Howard correspondence, and it relates to constructive mathematics (wherein all proofs must provide an algorithm for finding a "witness" object satisfying the desired property).

A great way to understand monads is as a "design pattern," because they pop up extremely often in practical programming. Consider functions with a type signature that looks like `A -> T<B>`, such as `A -> Promise<B>` or `A -> Optional<B>`.

If you have some function fetchResponse that returns a Promise<Response>, and a function processJSON that takes a Response as an argument, you cannot compose them the usual way, as `processJSON(fetchResponse(x))`. Instead, you need to do `fetchReponse(x).then(processJSON)`, and the entire expression has to return another Promise. Ditto for functions that return an Optional.

All data types that implement this design pattern have the structure of a monad. A monad consists of a generic type that is "covariant" in its type parameter (such as Promise or Optional), a way to embed a singular value into the data type, and a "then" method to compose the data type with a callback. Lists also implement the monad design pattern, and the "then" method for lists is flatmap. A monad basically lets you compose functions with a type signature that looks like `A -> T<B>`.

Furthermore, each of these data types (Promises, Optionals, Lists) can be viewed as the output of some computation. Promises are produced whenever a function performs asynchronous IO, Optionals are produced when computations may return some "null" value, and Lists are returned if an algorithm may produce multiple solutions.

Just like Promises have async/await syntactic sugar, similar syntactic sugar can be devised for other "monadic" types. For Optionals, the equivalent of async/await is null propagation (some languages have a `?` operator for this). For Lists, the equivalent of async/await is list comprehension, which "picks" each element from the list to build up a new list. Async/await, null propagation, and list comprehensions all have the same underlying structure, called a "monad."

A "free monad" is a monad that does not implement any specific computation, but instead builds up an abstract syntax tree that needs to be interpreted. Free monads are useful because other monad instances can be implemented in terms of the free monad.

It's serendipitous that I'm seeing this blog post on the front page today, because I'm currently writing an article discussing the free monad.

In addition to the free monad presented in this post, there is a variant, called the "freer" monad, based on the "bind" operation instead of the "join" operation:

    data Freer f a where
      Pure :: a -> Freer f a
      Bind :: f a -> (a -> Freer f b) -> Freer f b

When thinking of monads as giving the semantics of some computational strategy, it's easier to define them in terms of "bind" instead of "join." This way of defining monads is sometimes called a "Kleisli triple" because it is better suggestive of "Kleisli arrows," or functions of the signature `a -> m b`. The "bind" operation defines how to compose a monadic computation with its continuation, and from this perspective, the "freer" monad resembles an abstract syntax tree.

Originally, Eugenio Moggi proposed monads as a technique for specifying the denotational semantics of programming languages. All Java programs "really" happen in the IO + Either monads, because all Java programs may perform IO and throw exceptions. To my understanding, free monads are the monad that OCaml 5 runs in, because they give the semantics for effect handlers (or resumable exceptions).

Over the past few years, OCaml has seen an abundance of new language features and standard library additions. OCaml 4.08 added let-binding operators (syntactic sugar for continuation-passing style and monadic programming), OCaml 5 implemented a multicore runtime and effect handlers, OCaml 5.3 finally added dynamic arrays to the standard library, and OCaml 5.4 added labeled tuples.

With unboxed types, I believe OCaml would achieve similar granularity over memory allocations as C#: garbage-collected, but supporting "structs" which are allocated on the stack (or inline the same heap allocation when part of a reference type). I think there is an unexplored space for "soft" systems programming languages that retain a garbage collector by default, while also allowing the programmer to tightly control memory allocations in performance-critical code.

If OCaml hits this sweet spot in abstraction, what domains would adopt it? Could OCaml potentially compete with C#, or Swift?

This is the difference between functions and effect handlers, to my understanding:

Functions map inputs to outputs, with a type signature that looks like A -> B. Functions may be composed, so if you have f: A -> B and g: B -> C, you have gf: A -> C. Function composition corresponds with how "ordinary" programming is done by nesting expressions, like g(f(x)).

Sometimes, the function returns something like Option<B> or Future<B>. "Ordinary" function composition would expect the subsequent function's input type to be Future<B>, but frequently you need that input to have type B. Therefore, optionals or futures require "Kleisli composition," where given f: A -> Future<B> and g: B -> Future<C>, you have gf: A -> Future<C>. Kleisli composition corresponds with "monadic" programming, with "callback hell" or some syntactic sugar for it, like:

    let y = await f(x);
    g(y)

You are right, in Haskell type constructors may be partially applied. In my opinion, this feature has less to do with any fundamental difference between `Either` in Haskell and `Result` in other languages, and more to do with Haskell's more powerful type system. In the same way, the pair type (a, b) in Haskell is also different from the pair types in other languages. This feature is called "higher-kinded types."

In particular, higher-kinded types are necessary to abstract over functors (or functions from types to types, * -> *). The list type constructor is a functor, and the partially applied type constructor `Either a` is also a functor. However, in languages without higher-kinded types, type variables can only be "ground types" (of kind *).

I don't agree with this statement:

This means that Result <E, T> type effectively has a single type argument, namely pair of types. The Either type has two type arguments and can be partially applied.

The Result<T, E> type still takes two type arguments. The main distinction, in my view, is that Haskell allows types to be "higher-order." In fact, to be really pedantic, you could argue that the `Either` type in Haskell really takes one type argument, and then returns a function from types to types (currying).

This is kind of like the type-level equivalent to how many programming languages support some notion of function or procedure (and functions may have multiple arguments), but only more modern languages support higher-order functions, or allow variables to be functions.

I'd never heard of "resumable exceptions" before, so I searched them up [1][2]. Is this another name for the language feature called "effect handlers" in OCaml 5?

[1] https://osa1.net/posts/2024-11-04-resumable-exceptions.html

[2] https://softwareengineering.stackexchange.com/questions/8033...

The `Either a b` type in Haskell is equivalent to the `Result<T, Error>` type in other languages. The only difference is in the naming: "Result" semantically implies error handling, while "Either" implies a more general usage as the alternative between two options. Either and Result are the binary sum type (the disjoint union between two types).

In Haskell, Either is defined as

    data Either a b = Left a | Right b

Contrast the definition of the Result type in Swift:

    public enum Result<Success: ~Copyable & ~Escapable, Failure: Error> {
      /// A success, storing a `Success` value.
      case success(Success)

      /// A failure, storing a `Failure` value.
      case failure(Failure)
    }

I'm not sure what the parent commenter meant when they claimed that "Result <e, t> of yours is a Result (e, t) in Haskell." In Haskell, `(e, t)` would be the pair type (the binary product type).

One of the most thorough articles on error handling in programming language design that I've read is this one: https://joeduffyblog.com/2016/02/07/the-error-model/. It was written by Joe Duffy, who worked on Microsoft's experimental Midori language.

Another relevant article is Robert Nystrom's "What Color is Your Function?": https://journal.stuffwithstuff.com/2015/02/01/what-color-is-... This article is about async/await, but the same principles apply to error handling. This article uses colors as an analogy, but is really about monads.

Both IO and exceptions can be denoted as a monad. What this means is that a function inside the programming language, A -> B, can actually be denoted by a mathematical function of the signature [[A]] -> M [[B]], for some monad M. For example, if we are dealing with the exception monad, M would be _ + Exception.

A language such as Java implicitly executes in the IO + exception monad. However, the monad can also be exposed to the programmer as an ordinary data type, which is what Haskell does. When people talk about the tradeoff of exceptions versus Result<T, E>, or the tradeoff between preemptive concurrency and async/await, they are really talking about the tradeoff between making the monad implicit or explicit. (A language where all functions may throw is like one where all functions implicitly return Result<T, E>. A language where all functions may be preempted is like one where all functions are implicitly async, and all function calls are implicitly await points.)

The theoretical technique of using monads to model the implicit effects of a programming language was pioneered by Eugenio Moggi, and the idea of making them explicit to the programmer was pioneered by Philip Wadler.

Something else to think about is how monads stack. For example, how would you handle functions that are both async/await and throw exceptions? Does the answer change when the monad is implicit (e.g. throwing exceptions) or explicit (e.g. returning a result)?

Today, we tend to see The Great Gatsby as a work of historical literature, as it gives a window into the Roaring Twenties. However, F. Scott Fitzgerald did not set out to depict the past; he was depicting his own present. Similarly, Proust's literature is seen as a window into the French high-society of the Belle Epoque, a society in which Proust lived.

Which works today do you think future generations will see as the classics of the 2010s and 2020s? Such may not even necessarily be works of literature; they could be other storytelling mediums, such as film.

TypeScript’s type system is purely structural and exists only at compile time. It has no way to verify that your function actually implements what its signature claims. You can declare that a function transforms a User into a SafeUser, and as long as the return object has the required fields of SafeUser, TypeScript doesn’t care what additional properties might still be lurking in there.

This is fundamentally different from languages like Rust, where the type system can actually guarantee that if you claim to return an Option<T>, you genuinely can’t return null, the compiler enforces the contract at the language level. Rust’s type system doesn’t just trust your annotations; it verifies them.

This design where types are present at compile-time but disappear at runtime is called type erasure, and it's extremely common. For example, Java's generics are type erased. If you have some Java class Foo<T, U>, in the bytecode it will simply become Foo, and T and U will become Object. Therefore, you cannot use runtime introspection to recover their instantiations.

The remark contrasting TypeScript to Rust seems a little confused. Rust also uses type erasure; types and lifetimes are checked by the compiler, then the compiler produces a native executable, which is just machine code and would not contain type information. Option<&T> could be treated as a pointer T*, because the niche optimization ensures that the Option::None variant is represented as 0 or NULL. If C code were to interact with Rust code via FFI, it would be able to pass a value of 0. However, Rust doesn't have a null value the way that it's commonly understood in languages such as Java, C#, or JavaScript, a distinguished value that denotes a "sentinel" reference that does not refer to any object. I would say that the null reference is semantically a higher-level concept, specific to these particular programming languages.

Philosophically, the notion of type erasure goes all the way back to Curry-style (extrinsic) typing, which is contrasted with Church-style (intrinsic) typing. For example, in Curry-style typing, the program (fun x -> x) is the identity function on all types, while in Church-style typing, each type A has its own identity function, (fun (x : A) -> x) and a program is meaningless without types.

Please correct me if I'm wrong or misunderstood!

When I first tried to learn Vulkan, I felt the exact same way. As I was following the various Vulkan tutorials online, I felt that I was just copying the code, without understanding any of it and internalizing the concepts. So, I decided to learn WebGPU (via the Google Dawn implementation), which has a similar "modern" API to Vulkan, but much more simplified.

The commonalities to both are:

- Instances and devices

- Shaders and programs

- Pipelines

- Bind groups (in WebGPU) and descriptor sets (in Vulkan)

- GPU memory (textures, texture views, and buffers)

- Command buffers

Once I was comfortable with WebGPU, I eventually felt restrained by its limited feature set. The restrictions of WebGPU gave me the motivation to go back to Vulkan. Now, I'm learning Vulkan again, and this time, the high-level concepts are familiar to me from WebGPU.

Some limitations of WebGPU are its lack of push constants, and the "pipeline explosion" problem (which Vulkan tries to solve with the pipeline library, dynamic state, and shader object extensions). Meanwhile, Vulkan requires you to manage synchronization explicitly with fences and semaphores, which required an additional learning curve for me, coming from WebGPU. Vulkan also does not provide an allocator (most people use the VMA library).

SDL_GPU is another API at a similar abstraction level to WebGPU, and could also be another easier choice for learning than Vulkan, to get started. Therefore, if you're still interested in learning graphics programming, WebGPU or SDL_GPU could be good to check out.