stepchowfun

9 ms·

1.
by stepchowfun 3y 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
2.
by stepchowfun 3y ago
Thanks for your feedback!
3.
by stepchowfun 3y 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/
4.
by stepchowfun 3y ago
For something a bit more lightweight, Toast: https://github.com/stepchowfun/toast
5.
by stepchowfun 3y 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 fo
6.
by stepchowfun 3y 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
7.
by stepchowfun 3y 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
8.
by stepchowfun 3y 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: &
9.
by stepchowfun 3y 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 o
10.
by stepchowfun 3y ago
If I understand you correctly, I believe your understanding is correct.
11.
by stepchowfun 3y ago
No IDL that supports required fields can offer 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 pe
12.
by stepchowfun 3y ago
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 t
13.
by stepchowfun 3y ago
A wasm port doesn't seem too farfetched. What's the use case for running the code generator in the browser?
14.
by stepchowfun 3y ago
I'd love for Typical to support Go! We'd need someone with enough time to implement it. If anyone is interested in contributing any code generators, you can start by copying the Rust or TypeScript generator and modifying it approp
15.
by stepchowfun 3y ago
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
16.
by stepchowfun 3y ago
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` typ
17.
by stepchowfun 3y ago
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
18.
by stepchowfun 3y ago
> 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
19.
by stepchowfun 3y ago
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
20.
by stepchowfun 3y ago
Typical creator here. I'm pleasantly surprised to find this on HN today! Happy to answer any questions about it.
21.
by stepchowfun 3y ago
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
22.
by stepchowfun 4y ago
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 interac
23.
by stepchowfun 4y ago
And Toast: https://github.com/stepchowfun/toast
24.
by stepchowfun 4y ago
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 depe
25.
by stepchowfun 4y ago
> Working on it :) I look forward to checking it out when it's ready!
26.
by stepchowfun 4y ago
- 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 sufficient
27.
by stepchowfun 4y ago
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 prog
28.
by stepchowfun 4y ago
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&
29.
by stepchowfun 4y ago
I see where you're coming from, but it's hard to appreciate the subtle issues surrounding the notion(s) of equality without actually investing some time into doing formal mathematics. My claim is that type theory is a good avenue
30.
by stepchowfun 4y ago
> That sounds interesting, but unless higher category theory has any meaningful applications to non-mathematicians learning math in high school or undergraduate, saying that any of this will replace the equals sign or the standard notion

More ›