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

2 - Zod https://zod.dev/

3 - Friendly Functions https://simpatico.io/test/friendly

▲

lock1 3 days ago | parent | next [-]

No?

I think you're confusing ADT with a Typescript-like type system. Adding language support for ADT is not really a warrant for an "enough DOF to become scary" sticker.

I find modern Java surprisingly pretty good at capturing the essence of ADT without introducing way too much fancy stuff. Modern Java supports ADT via `sealed` classes (sum types) and `record` (product types). For working with ADT classes, modern Java provides exhaustive `switch` expression and `record` destructuring.

That's enough for minimal "language ADT support". You still can't do Typescript's wacky operations like conditional / mapped types or type parameter recursion in Java. You can't do fancy Haskell's typeclasses here either. And it is certainly not turning Java's type system into a Turing-complete type system at all.

▲

wk_end 3 days ago | parent | prev | next [-]

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.

	▲	jerf 3 days ago \| parent \| next [-]
		"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.
	▲	torginus 3 days ago \| parent \| prev \| next [-]
		It's like a Go-kart that can do 100 mph - while not inherently dangerous as the excess capability is not necessarily advertised, and it requires and user to exploit them, and it's up to user consensus that how fast a go-kart should be allowed to go, as capability increases so does the potential for abuse. It's up to debate that how much is too much, and while I'd think most people would agree that 100mph is above that limit, some would still argue it's artificially limiting. Powerful type systems are like that. You can program almost everything with what, for example, Go gave you before the generics update, but some would argue that more stuff is needed, like sum types etc. Now as capability increases, and some comipler people boast that their type system is Turing complete, I think you are in fact vindicating people who decide to write things like a type that can only contain prime numbers. But adding a type system this powerful will probably affect the real-world usability in your language, first you add a second language to your code that's awkward to use, slow to execute, and prone to crashing the compiler. I remember having endless debates with C++ people arguing that their doubly-recursive template system, is not in fact, clever, but makes every compile take forever, is prone to crashing the compiler or making it misbehave, and cricitising it is not in fact, just an admission of one's intellectual inferiority.
	▲	simpaticoder 3 days ago \| parent \| prev [-]
		Thanks, I didn't know that about Zod (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.

▲

WorldMaker 2 days ago | parent | prev | next [-]

Zod is great, but it's a giant monster of Typescript meta-typing on your behalf. Some of it is using that "scary" Turing completeness, even, of Typescript's type system.

It is nice in providing extra runtime validation that tests compiler assumptions, but it is adding complexity to do it, not removing it.

Also that "Friendly Function" is about returning Sum Type. `ValidationError | int` in the example's case. It isn't saving you from a type system that understands Algebraic Types, it is absolutely relying on it (if you want compile time type safety). Also, it's only about a step or two removed from (re-)discovering the next step which is the Either<Left, Right> monad. You just need a "bind operator" to make those "Friendly Functions" easier to pipeline together and you will be off to the monad races.

▲

whateveracct 3 days ago | parent | prev [-]

ADTs don't give your type system Turing completeness.

Also acting like Turing complete type systems are scary is more FUD than reality. If it becomes relevant it's because you are choosing to do recursion in some sort of constraint solver the type system provides.