7 ms·

Algebraic Types are not Scary

93 points by Bogdanp 1y ago

raxxorraxor 1y ago
> Algebraic Types are Just Elementary School Algebra My math prof did say the exact same while torturing students with question about proofs about their arcane set of arbitrary numbers and if they can be considered a field or ring or a group or everything at the same time. Sure, just some + and *... And sure, for a programmer it is mostly about which operations are defined on the type. But with just a few tweaks here and there you can transform a tool into a torture device... Jokes aside, I think this is a good explanation about the concepts and parallels.
- HelloNurse 1y ago
  > their arcane set of arbitrary numbers and if they can be considered a field or ring or a group or everything at the same time. A toolbag of abstract theory and tools that can be straightforwardly applied to any "arcane set" is the value that upgrading from arithmetic to algebra provides.
ekidd 1y ago
"Sum types" (aka "Rust enums") are something that I've really come to love for representing the idea "There are 3 possible cases here, here's the data we need in each case, and please remember that these cases are strictly mutually exclusive." Making this super easy and short to express makes a lot of designs clearer. There's also an interesting tradeoff here between sum types and abstract interfaces: - Abstract interfaces: "We have an unknown number of cases/subclasses, but they each support this fixed set of methods." The set of implementations is open, but the set of operations is harder to update. - Sum types (aka Rust enums): "We know all the cases, but there may be many different methods." The set of cases is harder to extend, but the set of methods manipulating them is completely open. A good example of the latter pattern is actually LLVM! LLVMs' intermediate representation is a essentially a small assembly language with a fixed set of operations (and an escape hatch). But because the set of basic instructions is small and known, it's possible to write dozens and dozens of optimization passes that each manipulate that small set of instructions. And a surprising number of programs work well with an LLVM-like structure. So in a language like Rust, which supports both abstract interfaces (via traits) and sum types (via enums), the tradeoff is whether you think you have many different types of values that you'll manipulate in a limited number of ways, or a small number of types of values that you'll manipulate in many different ways. (Oh, and the metaphor of "algebraic types" goes deeper than you might think; there are some super interesting data structures based on taking the "derivatives" of simple algebraic types.)
- phkahler 1y ago
  Sum type sounds like the old Variant from VB. We use something similar in Solvespace. Where one might have used polymorphism, there is one class with a type enum and a bunch of members that can be used for different things depending on the type. Definitely some disadvantages (what does valA hold in this type?) but also some advantages from the consistency.
  - WorldMaker 1y ago
    VB's Variant is a bit "assume I know what this is" dynamic typing, almost Python-like duck typing. It sounds like your solution is also more akin to duck typing. Sum Types are still themselves Types. The Sum Type itself like `int | string` is a Type. That Type generally only provides the intersection of methods/abilities, which depending on the language might only be a `toString()` method and the `+` operator (such as if the language uses that operator for string concatenation and also supports implicit conversions between int and string). The only safe things to do are the methods both types in the Sum support, so that intersection is an important tool to a type system with good Sum Types support. But the other part of it is that Sum Types are still made up of types with their own unique shapes. When you pattern match a Sum Type you "narrow" it to a specific type. You can narrow an `int | string` to an `int` and then subtract something from it or multiply something with it. You can narrow it to a `string` and do things only strings can do like `.split(',')`. Both types are still "preserved" as unique types inside the Sum Type. A good compiler tests your type narrowing in the same way that a good OOP compiler will typecheck most of your casts to higher or lower types in an inheritance tree. Given those cast checks, it's often more the case that you want to implement Sum Types as inheritance trees with casts, because the compiler will be doing more of the safety work. You write a base-class, probably abstract, to represent the Sum with only the intersection methods/operator overloads, then leaf classes, probably sealed/final, for each possible interior type the Sum can be, and use type checks to narrow to the leaf classes or cast back up to the SumType as necessary. That's actually a lot of work in most OOP languages to build. The thing about Sum Types in languages that support them is that a lot of that from pattern matching/narrowing, to computing the intersection of two types, is free/cheap/easy from those compilers. The compiler understands `int | string` directly, rather than needing to build by hand a class IntOrString with sub-types IntOrStringInt and IntOrStringString. (It start to get out of hand when you start adding more types to the sum. IntOrStringOrBoolIntOrString for narrowing from `int | string | bool` down to `int | string`, for instance, which in OOP maybe can't be the same type as IntOrString alone depending on how you want to narrow/expand your sum types.) (Also, not to get too much into the weeds but building a class structure like that is also more like a specialization of Sum Types called Discriminated Unions because each possibility in the Sum Type has a special "name" that can be used to discriminate one from the other. A lot of people that want Sum Types really just want Discriminated Unions, but you can build Discriminated Unions easily inside a Sum Type system without native support for it, but you can't as easily build richer Sum Types with just Discriminated Unions. In Typescript you will see a lot of Discriminated Unions built with a `type` field of some kind, often a string but sometimes an enum or symbol, which would also resemble your solution, but again the key difference is all the types that are summed together may have entirely different shapes and Typescript supports the sum type intersection calculations automatically, so maybe the top level sum just has the `type` field itself and nothing else, but you can use that `type` field to narrow to very specific shapes.)
zk108 1y ago
...and a monad is just a monoid in the category of endofunctors of some fixed category Just kidding but algebraic types are a great abstraction paradigm,
zokier 1y ago
ADTs are just structs and tagged unions. Tbh I don't understand why there is such fetishization of them considering how mudane they are.
- aiono 1y ago
  That's the point I tried to make. All my bachelor education there was no single mention of sum types even though we learned about the visitor pattern. Instead of having to model sum types with object hierarchies, the language should provide a straightforward way to represent them since it's a very basic concept. I think that while things have improved a lot compared to past, sum types concept is still not known as much as objects for instance. Today all mainstream languages added direct support for sum types but awareness of it lacks.
  - deleted 1y ago
    [deleted]
- Munksgaard 1y ago
  They are not "just structs and tagged unions". The language support that enforces safe usage is not optional.
- lock1 1y ago
  And OOP is just subtyping and visibility modifiers too! /j The main problem with ADT is language support for them. Primarily sum types, as they're missing in a lot of major PLs, while product types are "just" structs or classes. Without language support, you can simulate them via brittle workarounds like `if (d.isTypeA()) return d.methodA()`. Actually, I agree, it is mundane. That's exactly why it's kind of becoming an itch for anyone used to ADT, you'll feel like you're missing a basic building block. Just imagine if all languages removed `struct`-like and `class`-like construct. Something like Brainfuck esolang or any plain asm. It certainly possible to create arbitrary complex program in those languages. But would you pick `struct`-less language over language that supports it natively?
tromp 1y ago
> In OCaml for instance, unit corresponds to void. It makes more sense that Void should be void of values, i.e correspond to the empty set, as it does in Haskell [1]. Does OCaml have no empty type? [1] https://hackage.haskell.org/package/void-0.6.1/docs/Data-Void.html https://hackage.haskell.org/package/void-0.6.1/docs/Data-Voi...
- aiono 1y ago
  Void in Haskell is not the same thing as `void` in C, C++, Java or similar languages. If you return `Void` in Haskell, you will get a runtime error but `void` returning functions in C-like languages don't fail. It's not a type that doesn't have any value, rather it's a type that has a single value (normal return). Therefore it's more similar to `unit`.
  - chuckadams 1y ago
    Void having no values means it's impossible to return it or call a function that accepts it, so that would make it a compile-time error as opposed to runtime, no?
    - aiono 1y ago
      In practice yes, so when you try to execute the function that accepts `Void`, that will error out. But there is no reason to not compile it because it will never actually execute. This may sound unpractical but quite the contrary it's very useful. For instance, it's used to model functions that panics in Rust (https://doc.rust-lang.org/reference/types/never.html https://doc.rust-lang.org/reference/types/never.html). That way you can have a function called `todo` which fails when executed, but keeps the type checker happy until you actually implement it.
      - chuckadams 1y ago
        Right, it's very useful for lots of reasons, one being that any construct that actually tries to use a Void return value or construct a parameter value will be rejected at compile time. What I am really curious about is whether there's any uses of `absurd :: Void -> a` in the wild. I guess it's a top type for arbitrary functions, though I'm not sure how useful that is in itself...
spicyusername 1y ago
I always miss them so much in languages that don't have them. It is just such a common situation to be in where you have something that can only be X, Y, or Z, where X, Y, or Z are separate types. And then being able to pattern match over it to guarantee all cases are handled. Just perfect.
simpaticoder 1y ago
Algebraic types aren't scary, but they offer enough degrees-of-freedom to become scary [1]. Software is interesting because you can move around the complexity, and putting complexity into the type system has its advocates. They like to move complexity to compile time, but there are serious trade-offs that must be acknowledged! Turing-complete type systems can get programmers in trouble. Most programs are better off putting the complexity into the body of the function being called and away from the type system itself. Use simple, fixed, runtime types[2][3], and deal with the occasional complex case in user code that you control rather than compiler code you don't. 1 - Demonstration of the Turing-completeness of Typescript's types: https://github.com/microsoft/TypeScript/issues/14833 https://github.com/microsoft/TypeScript/issues/14833 2 - Zod https://zod.dev/ https://zod.dev/ 3 - Friendly Functions https://simpatico.io/test/friendly https://simpatico.io/test/friendly
- wk_end 1y ago
  Algebraic types, by themselves, don't do anything to make things "scary" or Turing-complete. Even C has (sort of) a weak, limited form of algebraic types through structs and unions. Zod, which you linked to as an example of the "simple, fixed, runtime types" you're advocating for supports discriminated unions too.
  - simpaticoder 1y ago
    Thanks, I didn't know that about Zod (https://zod.dev/api#intersections https://zod.dev/api#intersections). But I suppose I could generalize my point to be "less is more when it comes to algebraic types". A little ketchup is good on fries, but no-one wants fries swimming in ketchup.
  - jerf 1y ago
    "Algebraic types, by themselves, don't do anything to make things "scary" or Turing-complete." That's what "offer enough degrees-of-freedom to become scary" is getting at. The types themselves are no more complicated than non-algebraic types in the end. However it so happens that for historical reasons they have appealed to certain personality types who proceed to build glorious castles on top of them, and indeed per the "degrees of freedom" point, multiple different overlapping-yet-often-conflicting castles. It is easy to mistake those castles as being "algebraic types", which is not helped by the name, rather than being simple things which can be explained to children and could easily be used in an introduction to programming curriculum rather than conventional types. Conventional types are also not necessarily that complicated, or don't have to be. For instance, the complexity of C++'s towers of subclasses and templates should be accounted to C++ itself, rather than as a fundamental aspect of conventional type systems. There's things like Go that use a much simpler type system that is not generally amenable to such towers of complexity, which is a rephrasing of the most common complaints against it.
taeric 1y ago
The name for them feels a bit unfortunate, to me. The vast majority of programmers know of algebra from grade school, at best. And there you think of algebra as being able to do symbolic operations on equations. Not so much as "algebra over a field." I think it is fair to say that that is the more unfortunate naming, maybe? I still contend that that is what people think of when they hear the term, though.
- bananaflag 1y ago
  I always thought "algebraic" sounds unscary because in high school / undergraduate, algebra feels easier than analysis. Now, "analytic data types", that would be something.
  - thechao 1y ago
    Right. So, there's a unit type: the type that the sum of returns the other type, i.e., a + () = a So that means there's an identity type for the product type operator: a * 1 = a I.e., the type that you can "multiply" by that doesn't give you a two-field tuple, but just returns the single-field tuple. If "1" is a type, then we can build a sum-type with it: a + 1 = (a, 1) Ok. Cool. But! If we can "add 1", then we should be able to remove "1", right? That kinda implies that "-1" exists: (a, 1) -1 = (a,) # don't shoot the messenger, I'm just riffing But, that also implies that we can allow a product type whose result is the "-1" type? (i, i) = -1 OH NOES!
  - adastra22 1y ago
    Why not just “struct” or “record” and “enum” or “variant”?
  - taeric 1y ago
    Apologies, I missed this yesterday. It isn't that it is scary. It is that it connotes something about equations and such. It is literally the name of the class people learn how to symbolically solve quadratic equations and such. I was saying in another thread that I think this would be a lot more obvious if people actually did algebra on the types. But we don't. At least, I can't recall ever seeing it done. Closest I've seen is in places where people have to do so to justify the naming here. And I want to be clear, I specifically mean using + and * with types. And not that it can be done. Is it done?
stuartjohnson12 1y ago
Algebraic types aren't scary at all. See: type CollatzConjectureIsTrue< N extends any[] = [unknown], M = "∀", A extends any[] = [] > = M extends "odd" ? (N extends [any, any, ...infer R] ? CollatzConjectureIsTrue<R,"odd"> : N extends [any] ? true : false) : M extends "half" ? (N extends [any, any, ...infer R] ? CollatzConjectureIsTrue<R,"half",[unknown,...A]> : A) : M extends "3n1" ? [unknown, ...N, ...N, ...N] : M extends "next" ? (CollatzConjectureIsTrue<N,"odd"> extends true ? CollatzConjectureIsTrue<N,"3n1"> : CollatzConjectureIsTrue<N,"half">) : M extends "term" ? (N extends [unknown] ? true : CollatzConjectureIsTrue<CollatzConjectureIsTrue<N,"next">,"term">) : (CollatzConjectureIsTrue<N,"term"> extends true ? CollatzConjectureIsTrue<[unknown,...N]> : false);
- wk_end 1y ago
  Where are the sum and product types in this, exactly?
- mrkeen 1y ago
  any, extends, unknown and infer. What algebraic operations do they correspond to?
gherkinnn 1y ago
They clicked for me nigh a decade ago while learning Elm and since then I can't think in code without them.

93 points by Bogdanp 1y ago

> Algebraic Types are Just Elementary School Algebra My math prof did say the exact same while torturing students with question about proofs about their arcane set of arbitrary numbers and if they can be considered a field or ring or a group or everything at the same time. Sure, just some + and *... And sure, for a programmer it is mostly about which operations are defined on the type. But with just a few tweaks here and there you can transform a tool into a torture device... Jokes aside, I think this is a good explanation about the concepts and parallels.

HelloNurse 1y ago
> their arcane set of arbitrary numbers and if they can be considered a field or ring or a group or everything at the same time. A toolbag of abstract theory and tools that can be straightforwardly applied to any "arcane set" is the value that upgrading from arithmetic to algebra provides.

ekidd 1y ago

"Sum types" (aka "Rust enums") are something that I've really come to love for representing the idea "There are 3 possible cases here, here's the data we need in each case, and please remember that these cases are strictly mutually exclusive." Making this super easy and short to express makes a lot of designs clearer. There's also an interesting tradeoff here between sum types and abstract interfaces: - Abstract interfaces: "We have an unknown number of cases/subclasses, but they each support this fixed set of methods." The set of implementations is open, but the set of operations is harder to update. - Sum types (aka Rust enums): "We know all the cases, but there may be many different methods." The set of cases is harder to extend, but the set of methods manipulating them is completely open. A good example of the latter pattern is actually LLVM! LLVMs' intermediate representation is a essentially a small assembly language with a fixed set of operations (and an escape hatch). But because the set of basic instructions is small and known, it's possible to write dozens and dozens of optimization passes that each manipulate that small set of instructions. And a surprising number of programs work well with an LLVM-like structure. So in a language like Rust, which supports both abstract interfaces (via traits) and sum types (via enums), the tradeoff is whether you think you have many different types of values that you'll manipulate in a limited number of ways, or a small number of types of values that you'll manipulate in many different ways. (Oh, and the metaphor of "algebraic types" goes deeper than you might think; there are some super interesting data structures based on taking the "derivatives" of simple algebraic types.)

phkahler 1y ago
Sum type sounds like the old Variant from VB. We use something similar in Solvespace. Where one might have used polymorphism, there is one class with a type enum and a bunch of members that can be used for different things depending on the type. Definitely some disadvantages (what does valA hold in this type?) but also some advantages from the consistency.
- WorldMaker 1y ago
  VB's Variant is a bit "assume I know what this is" dynamic typing, almost Python-like duck typing. It sounds like your solution is also more akin to duck typing. Sum Types are still themselves Types. The Sum Type itself like `int | string` is a Type. That Type generally only provides the intersection of methods/abilities, which depending on the language might only be a `toString()` method and the `+` operator (such as if the language uses that operator for string concatenation and also supports implicit conversions between int and string). The only safe things to do are the methods both types in the Sum support, so that intersection is an important tool to a type system with good Sum Types support. But the other part of it is that Sum Types are still made up of types with their own unique shapes. When you pattern match a Sum Type you "narrow" it to a specific type. You can narrow an `int | string` to an `int` and then subtract something from it or multiply something with it. You can narrow it to a `string` and do things only strings can do like `.split(',')`. Both types are still "preserved" as unique types inside the Sum Type. A good compiler tests your type narrowing in the same way that a good OOP compiler will typecheck most of your casts to higher or lower types in an inheritance tree. Given those cast checks, it's often more the case that you want to implement Sum Types as inheritance trees with casts, because the compiler will be doing more of the safety work. You write a base-class, probably abstract, to represent the Sum with only the intersection methods/operator overloads, then leaf classes, probably sealed/final, for each possible interior type the Sum can be, and use type checks to narrow to the leaf classes or cast back up to the SumType as necessary. That's actually a lot of work in most OOP languages to build. The thing about Sum Types in languages that support them is that a lot of that from pattern matching/narrowing, to computing the intersection of two types, is free/cheap/easy from those compilers. The compiler understands `int | string` directly, rather than needing to build by hand a class IntOrString with sub-types IntOrStringInt and IntOrStringString. (It start to get out of hand when you start adding more types to the sum. IntOrStringOrBoolIntOrString for narrowing from `int | string | bool` down to `int | string`, for instance, which in OOP maybe can't be the same type as IntOrString alone depending on how you want to narrow/expand your sum types.) (Also, not to get too much into the weeds but building a class structure like that is also more like a specialization of Sum Types called Discriminated Unions because each possibility in the Sum Type has a special "name" that can be used to discriminate one from the other. A lot of people that want Sum Types really just want Discriminated Unions, but you can build Discriminated Unions easily inside a Sum Type system without native support for it, but you can't as easily build richer Sum Types with just Discriminated Unions. In Typescript you will see a lot of Discriminated Unions built with a `type` field of some kind, often a string but sometimes an enum or symbol, which would also resemble your solution, but again the key difference is all the types that are summed together may have entirely different shapes and Typescript supports the sum type intersection calculations automatically, so maybe the top level sum just has the `type` field itself and nothing else, but you can use that `type` field to narrow to very specific shapes.)

zk108 1y ago

...and a monad is just a monoid in the category of endofunctors of some fixed category Just kidding but algebraic types are a great abstraction paradigm,

zokier 1y ago

ADTs are just structs and tagged unions. Tbh I don't understand why there is such fetishization of them considering how mudane they are.

aiono 1y ago
That's the point I tried to make. All my bachelor education there was no single mention of sum types even though we learned about the visitor pattern. Instead of having to model sum types with object hierarchies, the language should provide a straightforward way to represent them since it's a very basic concept. I think that while things have improved a lot compared to past, sum types concept is still not known as much as objects for instance. Today all mainstream languages added direct support for sum types but awareness of it lacks.
- deleted 1y ago
  [deleted]
Munksgaard 1y ago
They are not "just structs and tagged unions". The language support that enforces safe usage is not optional.
lock1 1y ago
And OOP is just subtyping and visibility modifiers too! /j The main problem with ADT is language support for them. Primarily sum types, as they're missing in a lot of major PLs, while product types are "just" structs or classes. Without language support, you can simulate them via brittle workarounds like `if (d.isTypeA()) return d.methodA()`. Actually, I agree, it is mundane. That's exactly why it's kind of becoming an itch for anyone used to ADT, you'll feel like you're missing a basic building block. Just imagine if all languages removed `struct`-like and `class`-like construct. Something like Brainfuck esolang or any plain asm. It certainly possible to create arbitrary complex program in those languages. But would you pick `struct`-less language over language that supports it natively?

tromp 1y ago

> In OCaml for instance, unit corresponds to void. It makes more sense that Void should be void of values, i.e correspond to the empty set, as it does in Haskell [1]. Does OCaml have no empty type? [1] https://hackage.haskell.org/package/void-0.6.1/docs/Data-Void.html https://hackage.haskell.org/package/void-0.6.1/docs/Data-Voi...

aiono 1y ago
Void in Haskell is not the same thing as `void` in C, C++, Java or similar languages. If you return `Void` in Haskell, you will get a runtime error but `void` returning functions in C-like languages don't fail. It's not a type that doesn't have any value, rather it's a type that has a single value (normal return). Therefore it's more similar to `unit`.
- chuckadams 1y ago
  Void having no values means it's impossible to return it or call a function that accepts it, so that would make it a compile-time error as opposed to runtime, no?
  - aiono 1y ago
    In practice yes, so when you try to execute the function that accepts `Void`, that will error out. But there is no reason to not compile it because it will never actually execute. This may sound unpractical but quite the contrary it's very useful. For instance, it's used to model functions that panics in Rust (https://doc.rust-lang.org/reference/types/never.html https://doc.rust-lang.org/reference/types/never.html). That way you can have a function called `todo` which fails when executed, but keeps the type checker happy until you actually implement it.
    - chuckadams 1y ago
      Right, it's very useful for lots of reasons, one being that any construct that actually tries to use a Void return value or construct a parameter value will be rejected at compile time. What I am really curious about is whether there's any uses of `absurd :: Void -> a` in the wild. I guess it's a top type for arbitrary functions, though I'm not sure how useful that is in itself...

spicyusername 1y ago

I always miss them so much in languages that don't have them. It is just such a common situation to be in where you have something that can only be X, Y, or Z, where X, Y, or Z are separate types. And then being able to pattern match over it to guarantee all cases are handled. Just perfect.

simpaticoder 1y ago

Algebraic types aren't scary, but they offer enough degrees-of-freedom to become scary [1]. Software is interesting because you can move around the complexity, and putting complexity into the type system has its advocates. They like to move complexity to compile time, but there are serious trade-offs that must be acknowledged! Turing-complete type systems can get programmers in trouble. Most programs are better off putting the complexity into the body of the function being called and away from the type system itself. Use simple, fixed, runtime types[2][3], and deal with the occasional complex case in user code that you control rather than compiler code you don't. 1 - Demonstration of the Turing-completeness of Typescript's types: https://github.com/microsoft/TypeScript/issues/14833 https://github.com/microsoft/TypeScript/issues/14833 2 - Zod https://zod.dev/ https://zod.dev/ 3 - Friendly Functions https://simpatico.io/test/friendly https://simpatico.io/test/friendly

wk_end 1y ago
Algebraic types, by themselves, don't do anything to make things "scary" or Turing-complete. Even C has (sort of) a weak, limited form of algebraic types through structs and unions. Zod, which you linked to as an example of the "simple, fixed, runtime types" you're advocating for supports discriminated unions too.
- simpaticoder 1y ago
  Thanks, I didn't know that about Zod (https://zod.dev/api#intersections https://zod.dev/api#intersections). But I suppose I could generalize my point to be "less is more when it comes to algebraic types". A little ketchup is good on fries, but no-one wants fries swimming in ketchup.
- jerf 1y ago
  "Algebraic types, by themselves, don't do anything to make things "scary" or Turing-complete." That's what "offer enough degrees-of-freedom to become scary" is getting at. The types themselves are no more complicated than non-algebraic types in the end. However it so happens that for historical reasons they have appealed to certain personality types who proceed to build glorious castles on top of them, and indeed per the "degrees of freedom" point, multiple different overlapping-yet-often-conflicting castles. It is easy to mistake those castles as being "algebraic types", which is not helped by the name, rather than being simple things which can be explained to children and could easily be used in an introduction to programming curriculum rather than conventional types. Conventional types are also not necessarily that complicated, or don't have to be. For instance, the complexity of C++'s towers of subclasses and templates should be accounted to C++ itself, rather than as a fundamental aspect of conventional type systems. There's things like Go that use a much simpler type system that is not generally amenable to such towers of complexity, which is a rephrasing of the most common complaints against it.

taeric 1y ago

The name for them feels a bit unfortunate, to me. The vast majority of programmers know of algebra from grade school, at best. And there you think of algebra as being able to do symbolic operations on equations. Not so much as "algebra over a field." I think it is fair to say that that is the more unfortunate naming, maybe? I still contend that that is what people think of when they hear the term, though.

bananaflag 1y ago
I always thought "algebraic" sounds unscary because in high school / undergraduate, algebra feels easier than analysis. Now, "analytic data types", that would be something.
- thechao 1y ago
  Right. So, there's a unit type: the type that the sum of returns the other type, i.e., a + () = a So that means there's an identity type for the product type operator: a * 1 = a I.e., the type that you can "multiply" by that doesn't give you a two-field tuple, but just returns the single-field tuple. If "1" is a type, then we can build a sum-type with it: a + 1 = (a, 1) Ok. Cool. But! If we can "add 1", then we should be able to remove "1", right? That kinda implies that "-1" exists: (a, 1) -1 = (a,) # don't shoot the messenger, I'm just riffing But, that also implies that we can allow a product type whose result is the "-1" type? (i, i) = -1 OH NOES!
- adastra22 1y ago
  Why not just “struct” or “record” and “enum” or “variant”?
- taeric 1y ago
  Apologies, I missed this yesterday. It isn't that it is scary. It is that it connotes something about equations and such. It is literally the name of the class people learn how to symbolically solve quadratic equations and such. I was saying in another thread that I think this would be a lot more obvious if people actually did algebra on the types. But we don't. At least, I can't recall ever seeing it done. Closest I've seen is in places where people have to do so to justify the naming here. And I want to be clear, I specifically mean using + and * with types. And not that it can be done. Is it done?

stuartjohnson12 1y ago

Algebraic types aren't scary at all. See: type CollatzConjectureIsTrue< N extends any[] = [unknown], M = "∀", A extends any[] = [] > = M extends "odd" ? (N extends [any, any, ...infer R] ? CollatzConjectureIsTrue<R,"odd"> : N extends [any] ? true : false) : M extends "half" ? (N extends [any, any, ...infer R] ? CollatzConjectureIsTrue<R,"half",[unknown,...A]> : A) : M extends "3n1" ? [unknown, ...N, ...N, ...N] : M extends "next" ? (CollatzConjectureIsTrue<N,"odd"> extends true ? CollatzConjectureIsTrue<N,"3n1"> : CollatzConjectureIsTrue<N,"half">) : M extends "term" ? (N extends [unknown] ? true : CollatzConjectureIsTrue<CollatzConjectureIsTrue<N,"next">,"term">) : (CollatzConjectureIsTrue<N,"term"> extends true ? CollatzConjectureIsTrue<[unknown,...N]> : false);

wk_end 1y ago
Where are the sum and product types in this, exactly?
mrkeen 1y ago
any, extends, unknown and infer. What algebraic operations do they correspond to?

gherkinnn 1y ago

They clicked for me nigh a decade ago while learning Elm and since then I can't think in code without them.