From the blurb you quoted, it sounds like Lua doesn't check function argument arity natively, and fennel can. This means that fennel applies a runtime check to validate if a function was called with an expected arity, and if not, propagates an error (however Lua does that, I do not know), hence why arity checked functions are not as performant.
Your point about underlying data structures is spot on, in my view.
> Last quip to reflect on. "What's true of every bug found in the field? ... It passed the type checker. ... It passed all the tests. Okay. So now what do you do? Right? I think we're in this world I'd like to call guardrail programming. Right? It's really sad. We're like: I can make change because I have tests. Who does that? Who drives their car around banging against the guardrail saying, "Whoa! I'm glad I've got these guardrails because I'd never make it to the show on time."
I've been avoiding bringing up this point/example, but this is what prompted me to start thinking more deeply about types and their tradeoffs. Great talk, IMO.
> Are you familiar with the idea of "making illegal states unrepresentable", and "parse, don't validate"?
I haven't heard of those concepts/ideas before. Thanks for linking the article to define those concepts. With your example, and the article mentioning that "parsing should take place at the boundaries" (paraphrase), I can see how types (a la ML families) can be defined and composed give internal coherence once an external input has been parsed and hence validated.
Really interesting approach which I haven't considered before!
> I wouldn't say it's "extreme", it's very normal and natural. You just stick everything in the types and it works.
Ah, then I seem to be missing the point/intention. Thanks for illuminating that it should feel "natural". I think I need to spend more time with ML/Haskell families.
> ... the vast majority of the time you can construct your types in ways that force your logic to be correct because you just don't offer the ability to do the wrong thing
I think that is where I haven't had experience, nor much exposure to, when it comes to "static typing" in the true sense/intention of making a program correct. More so (which I think I loosely alluded to), is that the type system was being used to "model objects in the real world".
> what kind of logic errors are you seeing that you think wouldn't be eliminated by using types?
Classic "logic" stuff. Forgetting to modify and return a map given some other information. Accidentally returning the inverse of a boolean (i.e. !isSomething(x) vs isSomething(x)), incorrect adds or bit shifts, concurrent access to shared data structures (shared memory may be a more apt term), reconciling two different pieces of data into a shared one, algorithmic implementations (though I think you touched on this being less likely when using a type system designed to encourage correct algorithms by applying type theory, so it may be moot).
To maybe give some clarity to what I mean by correctness, I mean does the program match the expected behavior of the programmer. In playing around with F#, I've written buggy F#, but the types all matched up. I had a guarantee that my program would run in a non-faulty manner (bar any system fault), but the program was not correct.
> and found types to be very effective
I'm very curious where you've seen this be very effective (if you're able to share), and with what language/technology.
---
Also, as a last quip, I am enjoying learning about your perspective with type systems. There are some points you have brought up which have caused me to think harder and in more depth about the concept and it's application, and want to voice that I appreciate you putting in the time to have this exchange. Want to this up before I forget, since it is getting late in my neck of the woods.
> Types validate whatever you use them to validate, which can certainly include what we usually call "logic".
I'd love an example of this! I concede that I could be wrong on the point's of ML/Haskell families, however, it relies on the practitioner correctly using the type system to the extreme (at least, that is my impression). C++ and other similar OO's, the type system isn't as compelling as a correctness measure.
> On the contrary, they're still the most effective technique we've found for improving program correctness
In which domain are you working in where this has been the case? It may be my experience, but types as I have seen them used in industry have been more as "data containers with some behaviors".
I'd appreciate some examples of where you think I may be getting types wrong or missing the point.
In OO languages (Java, C#, C++, etc...), and functional ones (F#, Haskell, OCaml, etc...) types do not validate the correctness of logic, they evaluate the correctness of data structures and their access/mutation as they are manifested in the language.
OO languages consider data correctness as access patterns of encapsulated primitives (or other data structures) through defined behaviors on a "class".
Functional languages consider data correctness as access patterns which preserve previous version of data which a caller may still need to reference, or another part of the system references. Functional languages (in most cases) disallow direct mutation without some sort of immutability or persistence.
Types have little (or nothing) to do with program correctness, or data correctness as it relates to external storage engines and their concurrency guarantees (i.e. FoundationDB, PostgreSQL, MySQL, etc...).
Therefore, in this scenario, what matter's most is the correctness of underlying storage (including the rigor of validating expected behavior) and the event sourcing/messaging systems, not on the internal data structures and their idioms conveyed by the language.
From the blurb you quoted, it sounds like Lua doesn't check function argument arity natively, and fennel can. This means that fennel applies a runtime check to validate if a function was called with an expected arity, and if not, propagates an error (however Lua does that, I do not know), hence why arity checked functions are not as performant.