Recent submissions

Comment · 11 days ago
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).
Comment · 3 years ago
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 encourage 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.

Regarding the proposals in the article, the most interesting to me is (2), although I'm not sure about some of the specifics. In general, I think Haskell needs a way to graduate (or retire) language extensions, rather than having them accumulate unboundedly. It's harder to talk about Haskell when everyone is using a different flavor of it.

Comment · 3 years ago
Thanks for your feedback!
Comment · 3 years ago
If you're already familiar with a functional programming language like Haskell or OCaml, you have the background 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.) from first principles. If you're fascinated by proof assistants like Coq or Lean and want to understand how to use them, this tutorial is written for you.

Any feedback is appreciated!

Comment · 3 years ago
Comment · 3 years ago
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 many 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 three versions of the schema: the version that generated the message, the version before that, and the version after. 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.

Comment · 3 years ago
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!

Comment · 3 years ago
> 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 the common wisdom there is to not use required fields at all.

Comment · 3 years ago
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.

Comment · 3 years ago
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.

Live from the official Hacker News API

A modern reader for Hacker News · SvelteKit + Skeleton