6 ms·

This post shows MD but it misses the forest for the trees. To riff on the blog post linked below, “what if you have an Onyx holding a hard stone executing Earth

• im_down_w_otp 5y ago
  >"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.
  • zwkrt 5y ago
    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.
    • zem 5y ago
      take a look at https://blog.moertel.com/posts/2006-10-18-a-type-based-solution-to-the-strings-problem.html https://blog.moertel.com/posts/2006-10-18-a-type-based-solut... for a good counterexample
      • anonymoushn 5y ago
        Off topic: the link in your profile seems to no longer have its intended contents
        • zem 5y ago
          thanks, removed it!
      • deschutes 5y ago
        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.
        • zem 5y ago
          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 https://github.com/google/pytype
        • skybrian 5y ago
          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.
    • im_down_w_otp 5y ago
      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/ 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.
  • mpalmer 5y ago
    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.
    • nightski 5y ago
      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.
      • mpalmer 5y ago
        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.
    • myrryr 5y ago
      "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.
  • snicker7 5y ago
    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.
    • dgb23 5y ago
      I like data driven programming too. The code can become more declarative this way and the logic more malleable.
• ThomasMoll 5y ago
  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 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!
  • thaumasiotes 5y ago
    > Take the "Dual Type" in Pokémon for example: https://pokemondb.net/type/dual 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?
• thaumasiotes 5y ago
  > “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.
• exdsq 5y ago
  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#.
• sgt101 5y ago
  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.
• andi999 5y ago
  Although the last paragraph (of episode 5) claims not to give up on oop, the whole article says otherwise.
  • oscardssmith 5y ago
    Episode 5 of what?
• PaulHoule 5y ago
  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.
• Serow225 5y ago
  Thanks for linking to that of post, I always enjoy his articles and hadn't read that one for a long time :)