Hacker News Reader

>"The type system is for structuring how your program runs not its logical correctness."

Type-level programming can be a very powerful and useful way to coerce correctness in some scenarios, so I'm really confused by this statement.

I think the arguments on both sides are valid.

In dynamic programming languages, I generally prefer factoring business logic outside of procedures and into lookup tables. This is sometimes called "data-driven" or "table-oriented" programming. It eliminates control flow, which makes code more maintainable and less buggy.

Using Julia's dispatch mechanism accomplishes a similar goal. Here, multiple dispatch is akin to a table lookup. It may even be faster than the explicitley data-driven approach since the lookup can be done in compile-time.

I like data driven programming too. The code can become more declarative this way and the logic more malleable.

Part of his point seems to be that you can manipulate data with code, but you can't manipulate your app's typings with code.

Expressing your business domain in types makes it more likely that a given change of requirements demands a lot of by-hand, non-abstractable changes to the code.

I'd argue on the contrary, having the business domain in the type system allows the compiler to help you ensure the changes are made correctly instead of relying purely on tests (which are still valuable, but I'll take guarantees where I can get them).

The type system also makes it easy to reduce the state space of the program. For example, if a method takes an int as a parameter you have a pretty large state space. But if it takes a strongly typed enum which can only be of 3 values, now you have restricted the surface area for which you have to test. If you exploit the type system to this effect it is very powerful.

I agree with both your points! I didn't make a value judgment, and in fact I think our comments aren't mutually exclusive, we're just describing the pros for each side of what ends up being a trade-off.

The problem I call out is less of an issue for the parts of the domain that are unlikely to change often, or that touch fewer parts of the system.

"Part of his point seems to be that you can manipulate data with code, but you can't manipulate your app's typings with code."

You can do both you know.

Yeah if you’re writing a standard library or a parser or maybe a database query optimizer, but if you aren’t writing code about code, then it’s probably not the way to go.

I don't know. I'm of course biased, though that bias is built on several years of dealing with increasingly critical systems and the entirely avoidable issues those systems faced due to a preponderance of foot-guns that could have been otherwise mitigated with clever use of "ahead of time" constraint checking and enforcement. Not to mention the runtime quality and localizability of your diagnostics goes up a ton too when you know ahead of time that when you see certain kinds of errors/exceptions/failures that they must have happened in certain places and/or under very narrow conditions.

It also has a very nice quality of not mucking up your runtime performance with doing all the constraint checking on-demand and in very branchy ways.

As a simple example of how useful the approach can be, here's a thing we did awhile ago for making safe abstractions to low-level hardware resources: https://blog.auxon.io/2019/10/25/type-level-registers/ .

With that approach we could build a pipeline to consume hundreds of pages of SoC datasheet, generate the appropriate type specs from the register definitions, and end up with an API to the hardware that would fail to compile if a program was written to consume the hardware interface in a way that violated the spec in the datasheet.

take a look at https://blog.moertel.com/posts/2006-10-18-a-type-based-solut... for a good counterexample

Is it a good counterexample? It seems to have approximately the same misuse resistance as parameter binding or equivalent apis. (For example, the dom api.)

In particular, this property of the described system makes it trivial for the unknowing or uncaring to subvert it: > It provides a string-management kernel that lets you create “safe strings” by certifying a regular string as representing either text or a fragment of a known language.

From what I understood, the certification is an unchecked assertion made by the program. One of the comments gives a great example of how this will go wrong in practice. The other aspect of this that is glossed over is that many data schemas represent all these things as "text". It is again an exercise for the program to get this right at the io boundaries.

i am perhaps biased, since my day job is working on static type inference for python[0], but i genuinely do believe that encoding properties like this into the type system gives you not just an extra level of safety, but an extra level of expressiveness when modelling your data in code. it's the equivalent of having units in physics.

i agree that it's not foolproof, but it's better than treating everything as an undifferentiated string.

[0] https://github.com/google/pytype

The idea is to make security reviews easier. You can easily find all the places "safe strings" are created to see if they are doing the right parsing or sanity checks. The code that only uses the safe api needs less scrutiny, at least for the class of bugs this design is supposed to help with.

Off topic: the link in your profile seems to no longer have its intended contents

thanks, removed it!

Hey, author here.

1) Including the "Onyx holding a hard stone executing Earthquake in a Sandstorm against a Flygon with the ability Hover?" state is just doing an N-constraint solver. Since multiple dispatch is a generalized system, we can dispatch on N different types.

Take the "Dual Type" in Pokémon for example: https://pokemondb.net/type/dual. You'll notice that instead of just an NxN grid, we're dealing with an NxNxN. Where a single attack needs to be related against 2 different defenses.

Simple enough `eff(atk::T1, def1::T2, def2::T3) = ...`, the we can just encapsulate this second type within a `Pokémon` structure and route to the correct function dynamically.

2) The "Super Effectiveness" of a MD system is that you don't _need_ to put everything into a singular table, something that's functionally impossible to extend. The idea is that we can build up the correct relationships between types completely independent of one another. The issue is, who owns that table? How do you merge more than one new type in? (see my section about Composition in the post)

If someone else wants to make a new `Foo` type Pokémon, and another person is doing `Baz`, they can work completely separately, only defining the `eff` functions _only_ concerning their type. And there's _zero_ integration work to use both, just import the new types and their functions. This is incredibly extensible!

> Take the "Dual Type" in Pokémon for example: https://pokemondb.net/type/dual. You'll notice that instead of just an NxN grid, we're dealing with an NxNxN. Where a single attack needs to be related against 2 different defenses.

> Simple enough `eff(atk::T1, def1::T2, def2::T3) = ...`, the we can just encapsulate this second type within a `Pokémon` structure and route to the correct function dynamically.

This doesn't look like a good approach to me. One thing that bothers me is that it draws a distinction between def1 and def2 that doesn't, in reality, exist. You should not be handling the cases of "fire attack deals damage to grass/ice" and "fire attack deals damage to ice/grass" separately, because those are not separate cases. No type has a different effect when listed first than it does when listed second. No pair of types has any effect other than the independent effects of each type considered individually.

The same issue reoccurs at a higher level: fundamentally, you aren't dealing with an NxNxN grid. You're free to represent the data that way, but it's redundant -- the NxNxN grid contains no information that isn't already present in the NxN grid. You could reapply the same logic and produce an NxNxNxN grid detailing what would happen if a single-typed attack hit a triple-typed defender, or if a dual-typed attack hit a dual-typed defender, but... why would you do that?

So, it's an Nx(NxN/2) half grid. This is easily solved on the implementation side by making sure, for example, that the enum values for the second 2 arguments are always in ascending order.

> So, it's an Nx(NxN/2) half grid.

No, it's an NxN grid. Look at the second half of my comment.

> This is easily solved on the implementation side by making sure, for example, that the enum values for the second 2 arguments are always in ascending order.

So that when somebody invokes your function and passes the defender's types in the order listed for the Pokemon rather than sorting them beforehand, you crash?

Well the real issue is that we're using N instead of A and D. It is A X (D X D / 2).

And why the sudden helplessness? Just sort the 2 arguments before passing them to the internal Impl.

> Well the real issue is that we're using N instead of A and D. It is A X (D X D / 2).

No, it isn't. It's AxD, where A and D are always equal. There is no reason to add another dimension to the result table when the defense or offense might pick up another type. The expanded table will never contain any more information than the two-dimensional table already does.

(Dividing by 2 isn't correct either, even from your perspective; you're forgetting about the table's diagonal. In the "space is no object" approach you're advocating, the diagonals need to be filled by special-casing, since they represent a phenomenon that doesn't exist (a Pokemon which bears multiple instances of the same type) and obscure a phenomenon that does exist (a Pokemon which bears fewer types than the maximum possible number).)

You can just define a generic fallback method like `eff(p, d1, d2) = eff(p, d2, d1)`

I disagree - the question is how much fit is there between the type system and the logic that is being implemented using it.

Reusing a solver rather than writing a solver is a powerful approach, because the type system as a solver is common across all Julia projects - there is one Julia type system.

If you or I write a solver and use it in our project then everyone who comes to that project has to learn the solver.

However, this logic breaks if the use of the type system is so stretched and arcane that almost no engineer has seen it before.

Rules can and absolutely should be encoded in the type system if your language is powerful enough to allow it. Look at Type Driven Development in say Idris or F#.

> “what if you have an Onyx holding a hard stone executing Earthquake in a Sandstorm against a Flygon with the ability Hover?”

This is kind of a strange example -- the only two parts of it that interact are the Onyx, which is ground type, and the Earthquake, which is also ground type and will deal increased damage because the Onyx shares its type. So we could replace the question with "what if you have an Onyx using Earthquake?"

There is no ability Hover, but if the Flygon had Levitate (as all of them do), that would interact too, causing the Earthquake to have no effect.

This specific example hurts its own cause because it is a huge amount of code and explanation for what would be a screenful in Python.

It reminds me of the folks who have written their fifth rambling blog post about ‘Now I finally understand Monads in Haskell’ and don’t get that that will scare sensible people away and leave just the Don Quixote types.

Thanks for linking to that of post, I always enjoy his articles and hadn't read that one for a long time :)

Although the last paragraph (of episode 5) claims not to give up on oop, the whole article says otherwise.

Episode 5 of what?