stepchowfun

I've been writing notes as plain text files since forever, and it occurred to me that note-taking could benefit from the typical features that a language server provides: clickable links, autocomplete, hover previews, formatting, diagnostics, refactoring, etc. So I built a little language server and vscode extension. Note-taking now feels more like writing code, and I get to use my favorite vscode keybindings (vim).

Most of the comments so far are negative, so I'll add something positive. One thing I love about the Haskell community is how they are always questioning their assumptions and genuinely seeking the best way to do things (often drawing upon or contributing to computer science research). The core concepts behind Haskell are clean and simple (essentially something between System F and System Fω), but there's a lot of baggage on the surface that obscures that underlying elegance. We should support people taking an introspective look into their tools and asking how they can be better, even if certain proposals are unrealistic or controversial.

I think the author is just writing down their opinions (which are worth discussing!) and not seriously trying to start a new GHC frontend. Personally, I think Haskell is approximately stuck in a local maximum, which can only be escaped by embracing dependent types (which are actually simpler than where Haskell has been heading) rather than building increasingly complex approximations of them. Once you try a dependently typed language like Agda, Lean, Coq, or Idris, it's hard to go back to the complexity of having two (or more!) separate languages for types and programs.

Thanks for your feedback!

If you're already familiar with a functional programming language like Haskell or OCaml, you have the prerequisite knowledge to work through my Coq tutorial here: https://github.com/stepchowfun/proofs/tree/main/proofs/Tutor...

My goal with this tutorial was to introduce the core aspects of the language (dependent types, tactics, etc.) in a "straight to the point" kind of way for readers who are already motivated to learn it. If you're fascinated by proof assistants like Coq or Lean and you just want the TL;DR of how they work, then this tutorial is written for you.

Any feedback is appreciated!

For something a bit more lightweight, Toast: https://github.com/stepchowfun/toast

I think you're right, and now I understand why the rules seemed buggy to you but not to me. You're considering persisted messages that need to be compatible with more than just two subsequent versions of the schema, whereas the discussion and rules are formulated in the context of RPC messages between services which only need to be compatible with at most two versions of the schema: the old one and the new one. The README could do better to clarify that.

In the persisted messages scenario, there is one change to the rules: you can never introduce a required field (since old messages might not have it). Not even asymmetric fields can be promoted to required in that scenario.

Asymmetric fields are in a temporary transition state to/from required. So it would seem a bit odd to me for the transition state to be the default.

However, I think I see your reasoning: you don't want to accidentally introduce a required field without first making it asymmetric, and having asymmetric as the default would effectively prevent that.

So I can see the appeal of both designs!

> That's reasonable but it's a different notion of what a safe change is than I remember from using protobufs. I believe they just say adding or removing a required field isn't backward compatible.

Safe just means the old code and the new code can coexist (e.g., during a rollout), which requires compatibility in both directions. Not just backward compatibility.

This is true for Protocol Buffers as well, except they have no safe way to introduce or remove required fields, so they caution against using them.

You're considering an alternative behavior for asymmetric fields in choices, but you need to consider the behavior of optional fields in choices too.

In particular, the following duality is the lynchpin that ties everything together: "asymmetric" behaves like optional for struct readers and choice writers, but required for struct writers and choice readers.

From that duality, the behavior of asymmetric fields is completely determined by the behavior of optional fields. It isn't up to us to decide arbitrarily.

So the question becomes: what is the expected behavior of optional choice fields?

Along the lines you proposed, one could try to make optional choice fields behave as if they had an uninhabited type, so that writers would be unable to instantiate them—then you get exactly the behavior you described for asymmetric choice fields. Optional fields are symmetric, so both readers and writers would treat them as the empty type. This satisfies the safety requirement, but only in a degenerate way: optional fields would then be completely useless.

So this is not the way to go.

It's important to take a step back and consider what "optional" ought to mean: optionality for a struct relaxes the burden on writers (they don't have to set the field), whereas for a choice the burden is relaxed on readers (they don't have to handle the field). So how do you allow readers to ignore a choice field? Not by refusing to construct it (which would make it useless), but rather by providing a fallback. So the insight is not to think of optional as a type operator (1 + T) that should be dualised in some way (0 * T), but rather to think about the requirements imposed on writers and readers.

You're right to note the duality between sums and products and initial and terminal objects, and indeed category theory had a strong influence on Typical's design.

I can't speak with authority about ATD, but the following might be helpful:

Aside from algebraic data types, the big selling point of Typical is asymmetric fields. That's the crucial feature that distinguishes Typical from every other framework. Without asymmetric fields, there is no safe way to introduce or retire required fields. People using other frameworks fear required fields (rightly so), whereas Typical gives you the tools to embrace them.

If I understand you correctly, I believe your understanding is correct.

No IDL that supports required fields has the transitivity property you're referring to.

Typical has no notion of commits or pull requests in your codebase. The only meaningful notion of a "change" from Typical's perspective is a deployment which updates the version of the code running in production.

When promoting an asymmetric field to required (for example), you need to be sure the asymmetric field has been rolled out first. If you were using any other IDL framework (like Protocol Buffers) and you wanted to promote an optional field to required, you'd be faced with the same situation: you first need to make sure that the code in production is always setting that field before you do the promotion. Typical just helps more than other IDL frameworks by making it a compile-time guarantee in the meantime. The fact that other frameworks offer no help with this has led many organizations to ban required fields entirely, which only kicks the can down the road.

We should be more careful about how we use the overloaded word "change", so I'm grateful you pointed this out. Another comment also helped me realize how confusing the word "update" can be.

If you add an asymmetric field to a struct, writers need to be updated to set the field for the code to compile.

If you also add an asymmetric field to a choice, readers need to be updated to be able to handle the new case for the code to compile.

You can do both in the same change. The new code can be deployed to the writers and readers in any order. Messages generated from the old code can be read by the new code and vice versa, so it's fine for both versions of the code to coexist during the rollout.

After that first change is rolled out, you can promote the new fields to required. This change can also be deployed to writers and readers in any order. Since writers are already setting the new field in the struct, it's fine for readers to start relying on it. And since readers can already handle the new case in the choice, it's fine for writers to start using it.

A wasm port doesn't seem too farfetched. What's the use case for running the code generator in the browser?

I'd love for Typical to support Go. We just need someone with enough time to implement it.

Go doesn't have sum types and has an ad hoc story about nullability, so it clashes somewhat with Typical's algebraic type system. Nevertheless, it's important for Go programs to be able to communicate with other programs which do benefit from Typical's hardline stance on type safety, so having code generation support for Go would be great.

If anyone is interested in contributing any code generators, you can start by copying the Rust or TypeScript generator and modifying it appropriately. See the contributing guide here: https://github.com/stepchowfun/typical/blob/main/CONTRIBUTIN...

Yes! We have comprehensive integration tests that run in the browser to ensure the generated code only uses browser-compatible APIs. Also, the generated code never uses reflection or dynamic code evaluation, so it works in Content Security Policy-restricted environments.

See this section of the README for more info: https://github.com/stepchowfun/typical#javascript-and-typesc...

Avro has no equivalent of Typical's asymmetric fields. In Avro:

1. Record types can have optional (but not asymmetric) fields, just like in most IDLs. Avro implements this by taking the union of the field type with a special `null` type, but in practice it's equivalent to having optional fields.

2. Avro doesn't support proper sum types, but it has two approximations of them: unions (but not tagged unions) and enums. Unions have no support for adding/removing new cases safely. Enums can have a default value that is used if the case is not recognized.

From the "Typical perspective", both of these are problematic:

1. If you are trying to introduce a required field in Avro, you first introduce it as optional, and then at some point in the future when you have manually confirmed that the field is always being set by every writer, you can promote the field to required. Typical's asymmetric fields offload the burden of having to do that manual confirmation onto the type checker.

2. For unions, Avro offers no equivalent of optional or asymmetric cases. If you add a new case, you better not use it until all readers can handle it, and the type checker won't enforce that. For enums, the solution of having default values is unsatisfactory, because not every type has a suitable default. In practice, this usually means adding a catch-all default that is only used to signal an unrecognized input, but then what is a reader supposed to do with that? With Typical, if a writer introduces a new optional or asymmetric case, it must then provide an appropriate fallback to use when the new case isn't recognized by readers. For example, if a new specific type of error is introduced (e.g., with a stack trace), the fallback might be a more general type of error (e.g., with only an error message) that readers already know how to handle. If the new case is asymmetric, then you know readers can handle it, so once its rolled out you know it's safe to subsequently promote the case to required (so that writers no longer need to provide a fallback).

Here I've only discussed the challenges with adding new required fields/cases, but you run into similar trouble when removing them. This section of the README discusses all the pitfalls: https://github.com/stepchowfun/typical#required-optional-and...

It's a good question! The binary format is completely inscrutable to human eyes and is not designed for manual inspection/editing. However:

1) For Rust, the generated types implement the `Debug` trait, so they can be printed in a textual format that Rust programmers are accustomed to reading.

2) For JavaScript/TypeScript, deserialized messages are simple passive data objects that can be logged or inspected in the developer console.

So it's easy to log/inspect deserialized messages in a human-readable format, but there's currently no way to read/edit encoded messages directly. In the future, we may add an option to encode messages as JSON which would match the representation currently used for decoded messages in JavaScript/TypeScript, with sums being encoded as tagged unions.

> If I have a single language codebase, why should I prefer the first approach?

Probably the most compelling reason is that a single language codebase might not be a single language codebase forever. But, as you suggested, the switch to a language-agnostic framework can be deferred until it becomes necessary.

However, there's a reason to use Typical specifically: asymmetric fields. This feature allows you to change your schema over time without breaking compatibility and without sacrificing type safety.

If you ever expect to have newer versions of the codebase reading messages that were generated by older versions of the codebase (or vice versa), this is a concern that will need to be addressed. This can happen when you have a system that isn't deployed atomically (e.g., microservices, web/mobile applications, etc.) or when you have persisted messages that can outlive a single version of the codebase (e.g., files or database records).

An embedded DSL could in principle provide asymmetric fields, but I'm not aware of any that do.

> Typical isn't focused on JSON, so it doesn't seem like it is optimized for web.

It just makes different trade-offs than most web-based systems, but that doesn't make it unsuitable for web use. We have comprehensive integration tests that run in the browser. Deserialized messages are simple passive data objects [1] that can be logged or inspected in the developer console.

[1] https://en.wikipedia.org/wiki/Passive_data_structure

You're exactly right about other frameworks appealing to the lowest common denominator, whereas Typical isn't willing to make such compromises.

Languages without proper sum types are at a disadvantage here, but it's possible to encode sum types with exhaustive pattern matching in such languages using the visitor pattern. That approach requires some ergonomic sacrifices (e.g., having to use a reified eliminator rather than the built-in `switch` statement), and people using those languages may prefer convenience over strong guarantees. It's an unfortunate impedance mismatch.

Typical creator here. I'm pleasantly surprised to find this on HN today! Happy to answer any questions about it.

This is a Typical concept. I haven't seen this approach to optionality for sum types in any other serialization framework.

Programmers have good intuition for what it means for a field in a struct to be optional: it's either there or it's not. But for a sum type, what does it mean for a case to be "missing"? It's not quite as obvious, but it helps to think about what responsibilities are placed on writers vs. readers: optionality for a struct relaxes the burden on writers (they don't have to set the field), whereas for a sum type the burden is relaxed on readers (they don't have to handle the case).

It's always a pleasant surprise to see people using Coq and other formal verification technology to build confidence in their ideas and algorithms. We need to stop producing buggy software! If this article gave you a thirst for interactive theorem proving and you want to learn it from the ground up, I've recently written a Coq tutorial [1] which covers topics like programming with dependent types, writing proofs as data, and extracting verified code. That repository also contains a handy tactic called `eMagic` [2] (a variant of another useful tactic called `magic`) which can automatically prove the theorem from the article.

[1] https://github.com/stepchowfun/proofs/tree/main/proofs/Tutor...

[2] https://github.com/stepchowfun/proofs/blob/56438c9752c414560...

And Toast: https://github.com/stepchowfun/toast

Coq is so much fun. It makes writing proofs feel like playing a video game.

I've just finished writing a Coq tutorial [1] that is aimed at programmers (rather than, say, computer scientists). It covers topics like programming with dependent types, writing proofs as data, universes & other type theory stuff, and extracting verified code—with exercises.

[1] https://github.com/stepchowfun/proofs/tree/main/proofs/Tutor...

> Working on it :)

I look forward to checking it out when it's ready!

- A build system / package manager like Nix [1] but with a better user experience / more straightforward command-line tooling.

- A dependently typed programming language like Coq [2] (or Agda, Idris, Lean, etc.) that is sufficiently approachable to gain enough mindshare that companies start adopting it for mission-critical work.

- A version control system which scales to petabytes or more. Something that I could put large video files in without thinking twice about it. Something a large company could use for their monorepo—or even their data warehouse.

- A note-taking tool that allows me to organize notes in a graph with links between them (like a wiki), not as files and folders in a tree, which enforces the invariant that every note is transitively reachable from some "root" (by following links) so I never lose a note.

- Something like Toast [3] but which is also designed for running services in production, not just local development and continuous integration. A unified way to run code in dev, test, and prod environments. A new k8s.

[1] https://nixos.org/

[2] https://coq.inria.fr/

[3] https://github.com/stepchowfun/toast (shameless plug)

People often say state is hard in functional programming, but things like the Tardis monad have convinced me that (semantically speaking) functional programming is even better at state than the imperative/OOP paradigms. Imperative programs are essentially restricted to one global monad implicitly hardcoded into the language semantics, whereas with functional programming you have the freedom to choose the most appropriate monad for the task at hand. You want state? Use the state monad. You want continuations? Use that monad. You want time traveling? Yep, there's a monad for that too. IO, randomness, nondeterminism, parallelism, environment variables, failure, backtracking, software transactional memory, you name it. Many problems are best solved with a custom monad, rather than one of the standard ones; for example, using a monad that allows your code to emit constraints to be solved (this is a common technique for implementing type inference in compilers). Satisfyingly, reifying effects with monads preserves referential transparency and is therefore compatible with laziness, unlike traditional side effects which are sensitive to evaluation order.

I don't think it's an easy journey—not because the material is intrinsically difficult, but because almost all resources are written for mathematicians and computer scientists. I think a "homotopy type theory for programmers" book/blog/playlist could be a big hit. I've been considering putting something like that together.

I view the relationship between HoTT and topology as similar to that of functional programming and category theory: you don't need to know the latter to learn the former, but having that extra background can certainly help.