12 ms·

Why Static Languages Suffer from Complexity (2022)

138 points by mpweiher 3y ago

recursivedoubts 3y ago
i have to be totally honest that I understand about 5% of this post nonetheless, I will offer my obviously uninformed opinion on the topic (hey, it's hacker news): a big problem w/ static languages is that the developers of these languages are not willing to compromise type-safety for simplicity: there are very few 80/20 type systems out there that just say "Well, that's too hard to deal w/ you can bail out to unsafe code" when the implementation gets too crazy. My experience here is with going through the java generics cluster and helping write a statically typed scripting language that integrates w/ it effectively. As a positive example of what I'm talking about with respect to an 80/20 type system, consider a type system that supported covariant generics + function types that were contravariant wrt their argument types and covariant wrt their return types. This, I believe, would capture most of the correctness value of types and certainly provide good infrastructure for code completion and tooling, and it would be very simple to implement. It would not, however, be sound, and, thus, would be laughed out of any serious statically typed language discussions.
- FrustratedMonky 3y ago
  Like auto type conversions. Instead of barfing when assigning a Float to an Int, just auto round? Or but then if assigning a string to a float, then barf. Does this get 80%? I think anything beyond the simple cases, static enforcement is better, or you could be just getting garbage.
  - recursivedoubts 3y ago
    no, i don't think that's where the type system implementation complexity usually explodes, in fact that's a more complicated type system than requiring explicit type conversions (which I am usually in favor of, except in cases of toString)
  - junon 3y ago
    Auto round is rarely the operation you want.
    - FrustratedMonky 3y ago
      Guess that is what I am asking. The original post was highlighting it is easier using non-strict types. Like Python. So I was asking, what would that look like, you still loose data, have problems. At least with static checking, the compiler will catch it and then you can add explicate casting.
  - JohnFen 3y ago
    > Instead of barfing when assigning a Float to an Int, just auto round? Rounding involves a loss of data. If an operation would result in data loss, that operation should not be automatic. It should only be possible by the dev intentionally choosing it.
    - throwawaymaths 3y ago
      Technically float + float can result in data loss.
      - JohnFen 3y ago
        True, but that's a case where you're doing it on purpose by choosing to do floating point math, where that's standard behavior. That's a bit different than data loss resulting from an assignment operation, where data loss is not standard behavior.
  - Someone 3y ago
    > Instead of barfing when assigning a Float to an Int, just auto round? Because you can’t really round many floats to Int. A float can be larger than 10^38. If you ‘round’ that to a 64-bit signed integer, you have to return something that’s smaller than 10^19. For doubles, it’s even worse. They can be larger than 10^308. I think that indicates that “just auto round” isn’t an option. The option “if a reasonable conversion exists, make it, otherwise bail out” IMO is a lot worse than having a way to try that conversion and somehow indicate to the programmer when it failed.
  - FrustratedMonky 3y ago
    Guess that is what I am asking. The original post was highlighting it is easier using non-strict types. Like Python. So I was asking, what would that look like, you still loose data, have problems. At least with static checking, the compiler will catch it and then you can add explicate casting.
- bedobi 3y ago
  Not sure what you're getting at? Even in Haskell you can easily pass data around as untyped maps of maps if you want. But usually you don't. But maybe you're talking more about when generics and obsession with not duplicating any code ever makes that part of the type system needlessly complex
  - recursivedoubts 3y ago
    i'm talking about the type system itself: keeping the type system implementation itself simple rather than just offering an unsafe work-around this means foregoing system-enforceable type safety and features in some cases as the language level, in order to keep the type system fast and understandable to normies.
    - ses1984 3y ago
      The type system can be understandable to normies while the implementation is not. I would rather have a type system that is correct and consistent, with the complexity hidden away, than to have to know where the boundary is in the 80/20 system, which seems like the perfect place for bugs to enter your code.
      - ragnese 3y ago
        Agreed. Consistent is WAY better for me than inconsistent. One of the reasons I hate TypeScript so much is that it provides type safety except when it doesn't, and it takes a lot of experience to actually track down the MANY (non-obvious) places where it doesn't.
        CodeSgt 3y ago
        Could you provide some examples of where it doesn’t (assuming strict = true)?
        ragnese 3y ago
        I could provide a novel, but I'll try to keep it to just a few. Class methods have incorrect variance, even with the 'strictFunctionTypes' setting: https://www.typescriptlang.org/tsconfig#strictFunctionTypes https://www.typescriptlang.org/tsconfig#strictFunctionTypes. What's even more insane is that interface/type methods will have different variance depending on the syntax used to write them: type SafeFoo = { // This will have correct type variance foo: (x: string | number) => void } type UnsafeFoo = { // This will have incorrect type variance foo(x: string | number): void } The `readonly` feature doesn't fully work for object types: type Foo = { foo: number } type ReadonlyFoo = { readonly foo: number } function useFoo(f: ReadonlyFoo) { // f.foo = 4 // compile error const f1: Foo = f f1.foo = 4 // trololol, I just mutated the input even though I promised it was readonly } Classes are kind-of also an interface, which leads to inconsistent/surprising behavior: class Foo {} function useFoo(f: Foo) { if (f instanceof Foo) { console.log('Cool, a Foo.') } else { console.log('Uh, wut?') } } useFoo(new Foo()) // prints: 'Cool, a Foo.' useFoo({}) // prints: 'Uh, wut?' "TypeScript is structurally typed"... except when it's not. In my above example with the class pseudo-interface, you can "fix" it by including a private field in the class: class Foo { #nominal: undefined } function useFoo(f: Foo) { if (f instanceof Foo) { console.log('Cool, a Foo.') } else { console.log('Uh, wut?') } } useFoo(new Foo()) // prints: 'Cool, a Foo.' useFoo({}) // This is now a compile error! Record types are incorrectly typed/handled. A Record<string, string> implies that for ANY string key, there will be a string value. What you almost always actually mean is: Record<string, string | undefined>. Yes, there is a compiler setting (https://www.typescriptlang.org/tsconfig#noUncheckedIndexedAccess https://www.typescriptlang.org/tsconfig#noUncheckedIndexedAc...) to make all array and record accesses treated as possibly undefined, but that should only be necessary for arrays. The Array type has only one type parameter: the codomain. It has no way of communicating what the domain is (what indexes have values). A Record, on the other hand, DOES allow us to specify both the domain and codomain, so when I write Record<string, string> I'm telling the type system that every string key will be mapped to a string value. Therefore, it should not allow me to assign something that clearly cannot fulfill that contract to it, but it does: const x: Record<string, string> = {} In a type system sense, Record<K, V> is more-or-less equivalent to a function type: (K) => V. Imagine if TypeScript handled actual functions similarly: const x: (s: string) => string = (s) => {} There's more, but like I said, I don't want to spend all day typing...
- dinosaurdynasty 3y ago
  TypeScript is like this (can just give up and `as any` anything).
  - BenoitP 3y ago
    An actual positive in my book. If you consider back propagation of constraining types wrt the derivative of developer effort you get smooth gradients. Program works and is correct, but developer gets yelled at by its IDE (IntelliJ does) until there's a proof of it to some degree. I wish that types and proofs were more progressive. For example in Java, why can't we have the compiler tell us what's missing for proving a variable does not escape and we have to wait runtime to see if we had the optimization? Sometimes we'd like to guarantee it, and not just get it opportunistically.
  - the_gipsy 3y ago
    I find that 99% of my `as any` are due to some type definition limitation. The remaining 1% is due to something not expressable in typescript (or not worth it).
  - consilient 3y ago
    > (can just give up and `as any` anything) You should never do this: `any` is infectious. Assert the particular type judgement you want instead: `as number`, `as ({dispatch: () => void})`, etc.
- ramesh31 3y ago
  >there are very few 80/20 type systems out there that just say "Well, that's too hard to deal w/ you can bail out to unsafe code" when the implementation gets too crazy. This is what I love so much about Objective-C (and superset languages in general, including Typescript). You can play around all you want in ARC world, but drop straight down into C whenever it gets too bloated.
- dkarl 3y ago
  > there are very few 80/20 type systems out there that just say "Well, that's too hard to deal w/ you can bail out to unsafe code" when the implementation gets too crazy Scala is built on an OO/imperative functional foundation, with powerful enough types to build pure FP constructs on top. The problem with tradeoffs is not that the language won't let you, but in the culture: it's hard to get different Scala programmers to agree on tradeoffs when weighing type safety and FP purity against code complexity.
- ragnese 3y ago
  > a big problem w/ static languages is that the developers of these languages are not willing to compromise type-safety for simplicity: there are very few 80/20 type systems out there that just say "Well, that's too hard to deal w/ you can bail out to unsafe code" when the implementation gets too crazy. Well, this is the internet, so there will always be someone to disagree with you. In this case, I get to be one of those people for you! Yay, you. :) I find that most statically typed languages do bail out on type safety for simplicity for very many cases. Take arithmetic. Just about every statically typed language allows you to add two `int32`s together to get another `int32` with no acknowledgement in the type system that this operation my fail (overflow/underflow). Some languages will wrap the value around, and some will actually abort, but those are "runtime" decisions and not in the static type systems. Similarly, most languages allow us to compare IEEE float values for equality with no complaints from the type checker. Most languages allow us to index an array and assume that we will always receive a value. It's funny that you mention Java's generics, because they are kind of implemented in the exact 80/20 way you describe. Java's generics are type-erased at compile time, so all of these generic values and functions actually end up working in terms of `Object` (the base/root reference type) and doing runtime casts where needed. The only reason that's possible is because of the JVM's type system allowing for all of that loosey-goosey stuff.
  - alcover 3y ago
    > Some languages will wrap the value around, and some will actually abort What if a language had clamped int and modular mod types ? Overflow on mod would work as advertised and, if you disabled abort, overflow on int would be closer to its virtual value than if wrapped. mod32 m = UINT_MAX+1 //-> 0 int32 i = INT_MAX+1 //-> INT_MAX
    - Jtsummers 3y ago
      Ada offers modular types (ranging from 0 to modulus-1 as expected) with the overflow and underflow behavior you want, but not a clamped type as you describe it. So you can get the first but not the second behavior.
- munificent 3y ago
  > As a positive example of what I'm talking about with respect to an 80/20 type system, consider a type system that supported covariant generics + function types that were contravariant wrt their argument types and covariant wrt their return types. Java and C# are that with respect to array types. Arrays in both are covariant , which is unsound since arrays are mutable, and erroneous uses are checked at compile time. Dart is exactly the language you describe: All generic type parameters are treated covariantly and we use runtime checks to preserve soundness. It's... OK. It works out mostly OK in practice because the generic types that users happen to use variantly are conveniently used in a safely covariant way: Reading stuff out of Iterables and Maps. But there is a significant performance cost to the runtime checks needed to preserve soundness. And when you using a type in a covariant way incorrectly, it is deeply confusing to users. I think the right 80/20 approach is to do what C# 2.0 and just make all generics invariant.
- Someone 3y ago
  > a big problem w/ static languages is that the developers of these languages are not willing to compromise type-safety for simplicity: there are very few 80/20 type systems out there that just say "Well, that's too hard to deal w/ you can bail out to unsafe code" when the implementation gets too crazy. Very few? Many languages allow you to cast references to other types at will. C# does one better with its ‘dynamic’ keyword, which makes it much clearer where you are using runtime method lookup. https://learn.microsoft.com/en-us/dotnet/csharp/advanced-topics/interop/using-type-dynamic https://learn.microsoft.com/en-us/dotnet/csharp/advanced-top...: “The dynamic type is a static type, but an object of type dynamic bypasses static type checking. In most cases, it functions like it has type object. The compiler assumes a dynamic element supports any operation” I think Swift copied that. https://docs.swift.org/swift-book/documentation/the-swift-programming-language/declarations/ https://docs.swift.org/swift-book/documentation/the-swift-pr...: “When you mark a member declaration with the dynamic modifier, access to that member is always dynamically dispatched using the Objective-C runtime.“
  - brabel 3y ago
    Add Dart to your list.
  - KaiserPro 3y ago
    I do like c#'s dynamic and unsafe bits. it clearly telegraphs that someone is doing something either clever, stupid, desperate or all three.
  - Akronymus 3y ago
    F# goes even further than c# and allows you to embed IL. Which allows you to do really fun things.
    - akkad33 3y ago
      I'm very curious about F#. Can you give some code examples of how this allows dynamic typing?
      - 3y ago
- seanmcdirmid 3y ago
  TypeScript is obviously one of those 80/20 languages, and I like programming in it accordingly. But fighting the type system is one of the easier tasks a programmer could spend their time on if reliability was significantly improved via type safety. For example, null pointer static checking is a bit of a pain but has a significant pay off that probably makes it worth it.
- xwowsersx 3y ago
  Interesting. I think that many statically typed languages bail out too early! That's obviously a subjective view, but I suspect there's a large enough group of people who feel this way which is why much stricter and more unforgiving static type systems are developed and popularized.
- deleted 3y ago
  [deleted]
SkyMarshal 3y ago
> People in the programming language design community strive to make their languages more expressive, with a strong type system, mainly to increase ergonomics by avoiding code duplication in final software; I’ve never heard this, thought the reason was to eliminate classes of errors at compile time and to make large-scale refactoring easier, among other things. Or did I just miss this rationale? Here’s the lede: > Let us think a little bit about how to workaround the issue. If we make our languages fully dynamic, we will win biformity and inconsistency 13, but will imminently lose the pleasure of compile-time validation and will end up debugging our programs at mid-nights. The misery of dynamic type systems is widely known. The only way to approach the problem is to make a language whose features are both static and dynamic and not to split the same feature into two parts. Thus, the ideal linguistic abstraction is both static and dynamic; however, it is still a single concept and not two logically similar concepts but with different interfaces 14. A perfect example is CTFE, colloquially known as constexpr: same code can be executed at compile-time under a static context and at run-time under a dynamic context (e.g., when requesting a user input from stdin.); thus, we do not have to write different code for compile-time (statics) and run-time (dynamics), instead we use the same representation. One possible solution I have seen is dependent types. With dependent types, we can parameterise types not only with other types but with values, too. In a dependently typed language Idris, there is a type called Type – it stands for the “type of all types”, thereby weakening the dichotomy between type-level and value-level. Having such a powerful thing at our disposal, we can express typed abstractions that are usually either built into a language compiler/environment or done via macros. Perhaps the most common and descriptive example is a type-safe printf that calculates types of its arguments on the fly, so let give us the pleasure of mastering it in Idris 15! … Overall, the design of Zig’s type system seems reasonable: there is a type of all types called type, and using comptime, we can compute types at compile-time via regular variables, loops, procedures, etc. We can even perform type reflection through the @typeInfo, @typeName, and @TypeOf built-ins! Yes, we can no longer depend on run-time values, but if you do not need a theorem prover, probably full-blown dependent types are a bit of overkill. … Everything is good except that Zig is a systems language. On their official website, Zig is described as a “general-purpose programming language”, but I can hardly agree with this statement. Yes, you can write virtually any software in Zig, but should you? My experience in maintaining high-level code in Rust and C99 says NO. … Zig can still be used in large systems projects like web browsers, interpreters, and operating system kernels – nobody wants these things to freeze unexpectedly. Zig’s low-level programming features would facilitate convenient operation with memory and hardware devices, while its sane approach to metaprogramming (in the right hands) would cultivate understandable code structure. Bringing it to high-level code would just increase the mental burden without considerable benefits. … Final Words Static languages enforce compile-time checks; this is good. But they suffer from feature biformity and inconsistency – this is bad. Dynamic languages, on the other hand, suffer from these drawbacks to a lesser extent, but they lack compile-time checks. A hypothetical solution should take the best from the both worlds. Programming languages ought to be rethought.
Pet_Ant 3y ago
I always assumed that complex type systems were driven by enabling better optimization through program analysis since there is more information about guarantees to work with.
- feoren 3y ago
  That's basically wrong. Type systems are driven by something that is much harder and much more valuable than optimization: writing correct programs. Optimization is "strictly" less important than correctness, which means that there is no amount of improvement to optimization that is worth any loss of correctness. Okay, okay, there are a million caveats and side-notes to this, as there always are. This topic could (and does) fill textbooks. Let's get just a few out of the way: * Accepting lower precision in results is, of course, often done in the name of optimization. In these cases, there is a narrow band of "acceptable" outcomes; a small level of acceptable error that is still called "correct enough", so I'd argue correctness is still massively at a premium. In 3D games, very minor graphic artifacts on the level of 1% loss of "quality" are acceptable if it means a 5x speedup; 2% is probably not. So accuracy is "merely" 5,000 times more important. Getting within a factor of 10^-6 of the "true" result is acceptable in numerical analysis if it results in a 10x speedup, so accuracy is "merely" 10,000,000 times more important. * New graduates and entrants into software development massively over-prioritize optimization and performance, largely because the techniques to accomplish it are a lot more generic (and therefore teachable, and therefore over-represented in their classes) than the techniques to get correct behavior, which is highly specific to every domain. O(n^2) vs. O(log(n)) matters, but as long as you're hitting the correct complexity classes, performance is just not a big deal -- almost always, almost nobody cares. The (1 - almost)^2 times it does matter, you often drop down a safety level and work around the type system. * Static type systems have massively more power to help ensure correctness (by proving certain classes of errors aren't happening) than to improve optimization. You can mathematically prove that your type system prevents X, Y, and Z, and it's up to the programmer to decide if that's worth the restrictions your type system imposes. But optimization? That's all done through thousands of unrelated heuristics that may or may not help, increase the "quirkiness" of your compiled code, are a big source of compiler bugs, and depend on how the programmer writes the code. It is theoretically impossible (halting problem) to prove that any given heuristic is actually helping. Note that you can have a (valuable and loved) type-checker that is not actually a compiler (e.g. TypeScript's). As a rough, 90% correct soundbite: correctness is hard for people but easy for compilers; performance is easy for people but hard for compilers. This is why the few people who are working on bleeding-edge performance tasks are not using higher-level languages that are pushing the boundaries of type theory. They are using C and assembly.
valenterry 3y ago
First: > whenever you introduce a new linguistic abstraction to your language, it may reside either on the statics level, on the dynamics level, or on the both levels. In the first two cases, where the abstraction is located only on one particular level, you introduce inconsistency to your language; in the latter case, you inevitably introduce the feature biformity (...) Then: > One possible solution I have seen is dependent types. With dependent types, we can parameterise types not only with other types but with values, too. In a dependently typed language Idris (...) Great article overall!
nabla9 3y ago
Peter Norvig demonstrated it well using design patterns as an example. Design Patterns in Dynamic Languages http://norvig.com/design-patterns/design-patterns.pdf http://norvig.com/design-patterns/design-patterns.pdf
voidhorse 3y ago
Interesting article. I agree that this double language phenomenon of "biformity" can be a source of complexity, but I actually think the majority of complexity comes from one level higher: the paradigm, as the paradigmatic level is ultimately where assumptions about the modeling of problem spaces lie. The go example in the article is actually an instance of this: kubernetes went ahead and implemented an oop system in golang—why? because they felt go's assumption about the problem space (that it can be modeled and solved as imperative programs) was not a good fit for their actual problem space. Haskell's assumption of purity leads to a problem/solution space that's a good fit for problems that are primarily themselves pure and mathematical, but leads to complexity when it comes to having to solve problems that are not in this space (having to use monads or effects for io) Java's problem/solution space assumes you can model everything as objects and classes and runs into complexity when we attempt to use it for problems that are actually better modeled by other means. Many languages that are "multiparadigm" or "general purpose" really have an underlying problem/solution model driving the organization of programs. When our particular problem is not a good fit for this model, we have to contort and wind up spending more time dealing with language constructs themselves than actually expressing our problem and solution. Couple this with the fact that languages have different performance properties, which may also be a constraint you need to satisfy and things get...complicated. A lazy pure language might be the best modeling system for your problem (e.g. dealing with infinite sequences) but a non-starter due to memory constraints (not enough resources).
- klodolph 3y ago
  > having to use monads or effects for io Speaking as a Haskell programmer, this is not a problem. You put “IO” in the function signature and “do” in the body, and that’s workable. Or some other Monad. You get so many choices, which is its own problem, but “having to use monads” is not a problem in practice. There are other problems that make Haskell hard to work with. This just happens to not be it.
  - staunton 3y ago
    > There are other problems that make Haskell hard to work with. What are the biggest or most important ones in your opinion?
paulddraper 3y ago
> I cannot imagine a single language without the if operator, but only a few PLs accommodate full-fledged trait bounds, not to mention pattern matching. This is inconsistency...Combining statics and dynamics in a single working solution is also complicated since you cannot invoke dynamics in a static context. In terms of function colours, dynamics is coloured red, whereas statics is blue. Yeah, but unless you have some fancy totality checker, that's just the way it is. > Idris: The way out? Yeah okay, like that. > A hypothetical solution should take the best from the both worlds. Programming languages ought to be rethought. --- You can have static checking, "uniformity", or simplicity. Choose two.
- lmm 3y ago
  One could argue that Idris ends up a lot simpler, through being uniform, than a language like C++ or LiquidHaskell that has to implement the same thing multiple times because of that separation between compile- and runtime.
marcosdumay 3y ago
The lack of union between validating and executing things has been bothering me relatively often, on several different contexts, for many years already. Want to write some CRUD? The relationship between the code and the database is left hanging, and as a result not only the system is prone to failure, but you also have to repeat yourself all the time. Want to write a simulation library? The language won't help you checking the simulation data at all, you have to do that yourself. Want to describe some system for DevOps? There's a reason people use shitty custom languages for it instead of just reusing a dev one. Part of that reason is that you can check things compiling the custom language, but that implies you write the entire compiler. And the list goes on. Somehow it always eluded me that the entire definition of a dependent type system is one that solves this kind of problem. I guess I'm learning Idris soon.
kazinator 3y ago
> Dynamic languages, on the other hand, suffer from these drawbacks to a lesser extent, but they lack compile-time checks. I.e. "The two or three popular dynamic programing languages I know don't have any compile-time checks". Even my modest dialect (utterly not focused on type at all) Lisp can do a thing or two: 1> (compile-toplevel '(let (x) (cons a))) ** expr-1:1: warning: unbound variable a ** expr-1:1: warning: cons: too few arguments: needs 2, given 1 ** expr-1:1: warning: let: variable x unused #<sys:vm-desc: 8da2ac0> 2> (compile-toplevel '(awk ((let (x y) (rng x y)) (prn)))) ** expr-2:1: warning: rng: form x is moved out of the apparent scope and thus cannot refer to variables (x) ** expr-2:1: warning: rng: form y is moved out of the apparent scope and thus cannot refer to variables (y) ** expr-2:1: warning: unbound variable x ** expr-2:1: warning: unbound variable y ** expr-2:1: warning: let: variable y unused ** expr-2:1: warning: let: variable x unused #<sys:vm-desc: 8e6f3c0> 3> (compile-toplevel 'foo.bar) ** expr-3:1: warning: qref: bar isn't the name of a struct slot ** expr-3:1: warning: unbound variable foo #<sys:vm-desc: 8e8dc80> Common Lisp implementations like SBCL have sophisticated type inference. Dynamic programs can do things wrong in ways that are statically obvious.
- lmm 3y ago
  You can catch the low hanging fruit, sure. But that ends up being pretty useless at scale, because your "checks" can't be relied upon. Or, worse, the programmer ends up having to understand the rules of your type system without having any way to probe or express the types of parts of their program, since your language is pretending that it doesn't have a type system.
  - quaunaut 3y ago
    That's only if you don't design your language to be easily inferred. While I don't know the case for SBCL, a language like Elm has very heavy type inference that you can rely on better than most type systems.
    - lmm 3y ago
DarkNova6 3y ago
Dynamic languages have the same type of complexity, but you are not aware of it because it is well hidden. That's a big no-no for building applications.
- riku_iki 3y ago
  > Dynamic languages have the same type of complexity, but you are not aware of it because it is well hidden I would say you can ignore it until it fails in production.
  - DarkNova6 3y ago
    I would HOPE it fails in production. Even better is if you don't validate your response data and suddenly send the wrong data, no data or in the wrong format. Your consumers will love you for it. Of course you can build your own schema + validation logic... or just accept static types and get it for free.
rsrsrs86 3y ago
Author writes about types being applied for ergonomy, which is interesting. Types add static information that can be used by IDEs. But there are other reasons for using type systems: correctness and performance (unboxing, optimization)
Vt71fcAqt7 3y ago
>the statics level is where all linguistic machinery is being performed at compile-time. Similarly, the dynamics level is where code is being executed at run-time. Thence the typical control flow operators, such as if/while/for/return, data structures, and procedures, are dynamic int x = getFizBuz(1) is static, (or should be, in a smart enough compiler) despite `getFizBuz` having if/else in it's definition (if (x % 3 == 0)). This can happen in the real world. For example `button(size: 10)` could have some size dependent logic in its constructor that could be inlined. Any function that is called with static arguments could be inlined and run control flow at compile time.
bbwbsb 3y ago
Dependently typed languages can still develop a degree of biformity via 'tactic' languages. In Coq, for example, you have Gallina and Ltac, which are basically separate languages. This occurs because even with an elegant theorem proving system, you eventually want proof search, and proof search = macros. I'm not sure there is a way out. That said, if dependently typed languages had passable ecosystems I'd use them as is. Not sure if that is more stubbornness than good sense.
cryptonector 3y ago
This is an amazing article. It is the best advert for Idris and Zig, and it is very convincing. The gist, for those who lack the patience, is that a programming language should not have separate languages for defining code to run at compile-time, i.e. types (which can be code, because the type system could be [should be!] Turing complete), and code to run at run-time. That having the same language for both is not just very powerful, but that it leads to less repetition and less frustration and -most importantly- lower cognitive load. TFA is a masterpiece.
- chongli 3y ago
  I’ll stick with decidable type systems and compilation, thanks. Having to decide whether to kill my compiler because it’s either gone into an infinite loop or it’s got exponential blow up is not very reassuring.
Ericson2314 3y ago
Whenever I see like this, I ask, "have you ever worked on a team? Have you ever worked code without anyone who originally wrote it being around?" Dynamic typing only works small / solo projects and those that love to be obscure for fun. The things they want to do are...largely ill-advised. Because the problem they talk is about is less static typing, but structural vs normal (or transparent vs abstract) types. You can't "reverse an Automobile" for good reason! It is good they are aware of dependent types, but > Additionally, Idris features computational effects, elaborator reflection, coinductive data types, and many-many stuff for theorem proving. With This is attacking a strawman. Yes, Idris is a kitchen sink. But they also don't need any of those features. They could have used Agda for the example, and Agda is quite a small language! And still, I return to the stuff at the top. Reflection, breaking parametricity, etc. are all banned for good reason -- their midwit meme is off it is Zig etc. which are the midwits. Monotonicity (e.g. with traits) and parametricity are important metatheoretic properties for reasoning about code. Bottom line is this person wants to do things I would reject in code review regardless of the language.
leipie 3y ago
The starting premise (paraphrasing here) "strong typing to avoid duplication" for me is simply false. In my experience its main purpose is to reduce mistakes, increase discoverability/predictability and allows for easier refactoring
- leipie 3y ago
  also strong typing and static typing are two different things
renox 3y ago
What's a bit sad is that now with Zig/Idris you can finally easily make a type checked printf but in the meantime Python use fstrings which are much more ergonomic than prinf and AFAIK you can't make statically checked fstring in Zig nor Idris..

138 points by mpweiher 3y ago

i have to be totally honest that I understand about 5% of this post nonetheless, I will offer my obviously uninformed opinion on the topic (hey, it's hacker news): a big problem w/ static languages is that the developers of these languages are not willing to compromise type-safety for simplicity: there are very few 80/20 type systems out there that just say "Well, that's too hard to deal w/ you can bail out to unsafe code" when the implementation gets too crazy. My experience here is with going through the java generics cluster and helping write a statically typed scripting language that integrates w/ it effectively. As a positive example of what I'm talking about with respect to an 80/20 type system, consider a type system that supported covariant generics + function types that were contravariant wrt their argument types and covariant wrt their return types. This, I believe, would capture most of the correctness value of types and certainly provide good infrastructure for code completion and tooling, and it would be very simple to implement. It would not, however, be sound, and, thus, would be laughed out of any serious statically typed language discussions.

FrustratedMonky 3y ago
Like auto type conversions. Instead of barfing when assigning a Float to an Int, just auto round? Or but then if assigning a string to a float, then barf. Does this get 80%? I think anything beyond the simple cases, static enforcement is better, or you could be just getting garbage.
- recursivedoubts 3y ago
  no, i don't think that's where the type system implementation complexity usually explodes, in fact that's a more complicated type system than requiring explicit type conversions (which I am usually in favor of, except in cases of toString)
- junon 3y ago
  Auto round is rarely the operation you want.
  - FrustratedMonky 3y ago
    Guess that is what I am asking. The original post was highlighting it is easier using non-strict types. Like Python. So I was asking, what would that look like, you still loose data, have problems. At least with static checking, the compiler will catch it and then you can add explicate casting.
- JohnFen 3y ago
  > Instead of barfing when assigning a Float to an Int, just auto round? Rounding involves a loss of data. If an operation would result in data loss, that operation should not be automatic. It should only be possible by the dev intentionally choosing it.
  - throwawaymaths 3y ago
    Technically float + float can result in data loss.
    - JohnFen 3y ago
      True, but that's a case where you're doing it on purpose by choosing to do floating point math, where that's standard behavior. That's a bit different than data loss resulting from an assignment operation, where data loss is not standard behavior.
- Someone 3y ago
  > Instead of barfing when assigning a Float to an Int, just auto round? Because you can’t really round many floats to Int. A float can be larger than 10^38. If you ‘round’ that to a 64-bit signed integer, you have to return something that’s smaller than 10^19. For doubles, it’s even worse. They can be larger than 10^308. I think that indicates that “just auto round” isn’t an option. The option “if a reasonable conversion exists, make it, otherwise bail out” IMO is a lot worse than having a way to try that conversion and somehow indicate to the programmer when it failed.
- FrustratedMonky 3y ago
  Guess that is what I am asking. The original post was highlighting it is easier using non-strict types. Like Python. So I was asking, what would that look like, you still loose data, have problems. At least with static checking, the compiler will catch it and then you can add explicate casting.
bedobi 3y ago
Not sure what you're getting at? Even in Haskell you can easily pass data around as untyped maps of maps if you want. But usually you don't. But maybe you're talking more about when generics and obsession with not duplicating any code ever makes that part of the type system needlessly complex
- recursivedoubts 3y ago
  i'm talking about the type system itself: keeping the type system implementation itself simple rather than just offering an unsafe work-around this means foregoing system-enforceable type safety and features in some cases as the language level, in order to keep the type system fast and understandable to normies.
  - ses1984 3y ago
    The type system can be understandable to normies while the implementation is not. I would rather have a type system that is correct and consistent, with the complexity hidden away, than to have to know where the boundary is in the 80/20 system, which seems like the perfect place for bugs to enter your code.
    - ragnese 3y ago
      Agreed. Consistent is WAY better for me than inconsistent. One of the reasons I hate TypeScript so much is that it provides type safety except when it doesn't, and it takes a lot of experience to actually track down the MANY (non-obvious) places where it doesn't.
      - CodeSgt 3y ago
        Could you provide some examples of where it doesn’t (assuming strict = true)?
        ragnese 3y ago
        I could provide a novel, but I'll try to keep it to just a few. Class methods have incorrect variance, even with the 'strictFunctionTypes' setting: https://www.typescriptlang.org/tsconfig#strictFunctionTypes https://www.typescriptlang.org/tsconfig#strictFunctionTypes. What's even more insane is that interface/type methods will have different variance depending on the syntax used to write them: type SafeFoo = { // This will have correct type variance foo: (x: string | number) => void } type UnsafeFoo = { // This will have incorrect type variance foo(x: string | number): void } The `readonly` feature doesn't fully work for object types: type Foo = { foo: number } type ReadonlyFoo = { readonly foo: number } function useFoo(f: ReadonlyFoo) { // f.foo = 4 // compile error const f1: Foo = f f1.foo = 4 // trololol, I just mutated the input even though I promised it was readonly } Classes are kind-of also an interface, which leads to inconsistent/surprising behavior: class Foo {} function useFoo(f: Foo) { if (f instanceof Foo) { console.log('Cool, a Foo.') } else { console.log('Uh, wut?') } } useFoo(new Foo()) // prints: 'Cool, a Foo.' useFoo({}) // prints: 'Uh, wut?' "TypeScript is structurally typed"... except when it's not. In my above example with the class pseudo-interface, you can "fix" it by including a private field in the class: class Foo { #nominal: undefined } function useFoo(f: Foo) { if (f instanceof Foo) { console.log('Cool, a Foo.') } else { console.log('Uh, wut?') } } useFoo(new Foo()) // prints: 'Cool, a Foo.' useFoo({}) // This is now a compile error! Record types are incorrectly typed/handled. A Record<string, string> implies that for ANY string key, there will be a string value. What you almost always actually mean is: Record<string, string | undefined>. Yes, there is a compiler setting (https://www.typescriptlang.org/tsconfig#noUncheckedIndexedAccess https://www.typescriptlang.org/tsconfig#noUncheckedIndexedAc...) to make all array and record accesses treated as possibly undefined, but that should only be necessary for arrays. The Array type has only one type parameter: the codomain. It has no way of communicating what the domain is (what indexes have values). A Record, on the other hand, DOES allow us to specify both the domain and codomain, so when I write Record<string, string> I'm telling the type system that every string key will be mapped to a string value. Therefore, it should not allow me to assign something that clearly cannot fulfill that contract to it, but it does: const x: Record<string, string> = {} In a type system sense, Record<K, V> is more-or-less equivalent to a function type: (K) => V. Imagine if TypeScript handled actual functions similarly: const x: (s: string) => string = (s) => {} There's more, but like I said, I don't want to spend all day typing...
dinosaurdynasty 3y ago
TypeScript is like this (can just give up and `as any` anything).
- BenoitP 3y ago
  An actual positive in my book. If you consider back propagation of constraining types wrt the derivative of developer effort you get smooth gradients. Program works and is correct, but developer gets yelled at by its IDE (IntelliJ does) until there's a proof of it to some degree. I wish that types and proofs were more progressive. For example in Java, why can't we have the compiler tell us what's missing for proving a variable does not escape and we have to wait runtime to see if we had the optimization? Sometimes we'd like to guarantee it, and not just get it opportunistically.
- the_gipsy 3y ago
  I find that 99% of my `as any` are due to some type definition limitation. The remaining 1% is due to something not expressable in typescript (or not worth it).
- consilient 3y ago
  > (can just give up and `as any` anything) You should never do this: `any` is infectious. Assert the particular type judgement you want instead: `as number`, `as ({dispatch: () => void})`, etc.
ramesh31 3y ago
>there are very few 80/20 type systems out there that just say "Well, that's too hard to deal w/ you can bail out to unsafe code" when the implementation gets too crazy. This is what I love so much about Objective-C (and superset languages in general, including Typescript). You can play around all you want in ARC world, but drop straight down into C whenever it gets too bloated.
dkarl 3y ago
> there are very few 80/20 type systems out there that just say "Well, that's too hard to deal w/ you can bail out to unsafe code" when the implementation gets too crazy Scala is built on an OO/imperative functional foundation, with powerful enough types to build pure FP constructs on top. The problem with tradeoffs is not that the language won't let you, but in the culture: it's hard to get different Scala programmers to agree on tradeoffs when weighing type safety and FP purity against code complexity.
ragnese 3y ago
> a big problem w/ static languages is that the developers of these languages are not willing to compromise type-safety for simplicity: there are very few 80/20 type systems out there that just say "Well, that's too hard to deal w/ you can bail out to unsafe code" when the implementation gets too crazy. Well, this is the internet, so there will always be someone to disagree with you. In this case, I get to be one of those people for you! Yay, you. :) I find that most statically typed languages do bail out on type safety for simplicity for very many cases. Take arithmetic. Just about every statically typed language allows you to add two `int32`s together to get another `int32` with no acknowledgement in the type system that this operation my fail (overflow/underflow). Some languages will wrap the value around, and some will actually abort, but those are "runtime" decisions and not in the static type systems. Similarly, most languages allow us to compare IEEE float values for equality with no complaints from the type checker. Most languages allow us to index an array and assume that we will always receive a value. It's funny that you mention Java's generics, because they are kind of implemented in the exact 80/20 way you describe. Java's generics are type-erased at compile time, so all of these generic values and functions actually end up working in terms of `Object` (the base/root reference type) and doing runtime casts where needed. The only reason that's possible is because of the JVM's type system allowing for all of that loosey-goosey stuff.
- alcover 3y ago
  > Some languages will wrap the value around, and some will actually abort What if a language had clamped int and modular mod types ? Overflow on mod would work as advertised and, if you disabled abort, overflow on int would be closer to its virtual value than if wrapped. mod32 m = UINT_MAX+1 //-> 0 int32 i = INT_MAX+1 //-> INT_MAX
  - Jtsummers 3y ago
    Ada offers modular types (ranging from 0 to modulus-1 as expected) with the overflow and underflow behavior you want, but not a clamped type as you describe it. So you can get the first but not the second behavior.
munificent 3y ago
> As a positive example of what I'm talking about with respect to an 80/20 type system, consider a type system that supported covariant generics + function types that were contravariant wrt their argument types and covariant wrt their return types. Java and C# are that with respect to array types. Arrays in both are covariant , which is unsound since arrays are mutable, and erroneous uses are checked at compile time. Dart is exactly the language you describe: All generic type parameters are treated covariantly and we use runtime checks to preserve soundness. It's... OK. It works out mostly OK in practice because the generic types that users happen to use variantly are conveniently used in a safely covariant way: Reading stuff out of Iterables and Maps. But there is a significant performance cost to the runtime checks needed to preserve soundness. And when you using a type in a covariant way incorrectly, it is deeply confusing to users. I think the right 80/20 approach is to do what C# 2.0 and just make all generics invariant.
Someone 3y ago
> a big problem w/ static languages is that the developers of these languages are not willing to compromise type-safety for simplicity: there are very few 80/20 type systems out there that just say "Well, that's too hard to deal w/ you can bail out to unsafe code" when the implementation gets too crazy. Very few? Many languages allow you to cast references to other types at will. C# does one better with its ‘dynamic’ keyword, which makes it much clearer where you are using runtime method lookup. https://learn.microsoft.com/en-us/dotnet/csharp/advanced-topics/interop/using-type-dynamic https://learn.microsoft.com/en-us/dotnet/csharp/advanced-top...: “The dynamic type is a static type, but an object of type dynamic bypasses static type checking. In most cases, it functions like it has type object. The compiler assumes a dynamic element supports any operation” I think Swift copied that. https://docs.swift.org/swift-book/documentation/the-swift-programming-language/declarations/ https://docs.swift.org/swift-book/documentation/the-swift-pr...: “When you mark a member declaration with the dynamic modifier, access to that member is always dynamically dispatched using the Objective-C runtime.“
- brabel 3y ago
  Add Dart to your list.
- KaiserPro 3y ago
  I do like c#'s dynamic and unsafe bits. it clearly telegraphs that someone is doing something either clever, stupid, desperate or all three.
- Akronymus 3y ago
  F# goes even further than c# and allows you to embed IL. Which allows you to do really fun things.
  - akkad33 3y ago
    I'm very curious about F#. Can you give some code examples of how this allows dynamic typing?
    - 3y ago
seanmcdirmid 3y ago
TypeScript is obviously one of those 80/20 languages, and I like programming in it accordingly. But fighting the type system is one of the easier tasks a programmer could spend their time on if reliability was significantly improved via type safety. For example, null pointer static checking is a bit of a pain but has a significant pay off that probably makes it worth it.
xwowsersx 3y ago
Interesting. I think that many statically typed languages bail out too early! That's obviously a subjective view, but I suspect there's a large enough group of people who feel this way which is why much stricter and more unforgiving static type systems are developed and popularized.
deleted 3y ago
[deleted]

SkyMarshal 3y ago

> People in the programming language design community strive to make their languages more expressive, with a strong type system, mainly to increase ergonomics by avoiding code duplication in final software; I’ve never heard this, thought the reason was to eliminate classes of errors at compile time and to make large-scale refactoring easier, among other things. Or did I just miss this rationale? Here’s the lede: > Let us think a little bit about how to workaround the issue. If we make our languages fully dynamic, we will win biformity and inconsistency 13, but will imminently lose the pleasure of compile-time validation and will end up debugging our programs at mid-nights. The misery of dynamic type systems is widely known. The only way to approach the problem is to make a language whose features are both static and dynamic and not to split the same feature into two parts. Thus, the ideal linguistic abstraction is both static and dynamic; however, it is still a single concept and not two logically similar concepts but with different interfaces 14. A perfect example is CTFE, colloquially known as constexpr: same code can be executed at compile-time under a static context and at run-time under a dynamic context (e.g., when requesting a user input from stdin.); thus, we do not have to write different code for compile-time (statics) and run-time (dynamics), instead we use the same representation. One possible solution I have seen is dependent types. With dependent types, we can parameterise types not only with other types but with values, too. In a dependently typed language Idris, there is a type called Type – it stands for the “type of all types”, thereby weakening the dichotomy between type-level and value-level. Having such a powerful thing at our disposal, we can express typed abstractions that are usually either built into a language compiler/environment or done via macros. Perhaps the most common and descriptive example is a type-safe printf that calculates types of its arguments on the fly, so let give us the pleasure of mastering it in Idris 15! … Overall, the design of Zig’s type system seems reasonable: there is a type of all types called type, and using comptime, we can compute types at compile-time via regular variables, loops, procedures, etc. We can even perform type reflection through the @typeInfo, @typeName, and @TypeOf built-ins! Yes, we can no longer depend on run-time values, but if you do not need a theorem prover, probably full-blown dependent types are a bit of overkill. … Everything is good except that Zig is a systems language. On their official website, Zig is described as a “general-purpose programming language”, but I can hardly agree with this statement. Yes, you can write virtually any software in Zig, but should you? My experience in maintaining high-level code in Rust and C99 says NO. … Zig can still be used in large systems projects like web browsers, interpreters, and operating system kernels – nobody wants these things to freeze unexpectedly. Zig’s low-level programming features would facilitate convenient operation with memory and hardware devices, while its sane approach to metaprogramming (in the right hands) would cultivate understandable code structure. Bringing it to high-level code would just increase the mental burden without considerable benefits. … Final Words Static languages enforce compile-time checks; this is good. But they suffer from feature biformity and inconsistency – this is bad. Dynamic languages, on the other hand, suffer from these drawbacks to a lesser extent, but they lack compile-time checks. A hypothetical solution should take the best from the both worlds. Programming languages ought to be rethought.

Pet_Ant 3y ago

I always assumed that complex type systems were driven by enabling better optimization through program analysis since there is more information about guarantees to work with.

feoren 3y ago
That's basically wrong. Type systems are driven by something that is much harder and much more valuable than optimization: writing correct programs. Optimization is "strictly" less important than correctness, which means that there is no amount of improvement to optimization that is worth any loss of correctness. Okay, okay, there are a million caveats and side-notes to this, as there always are. This topic could (and does) fill textbooks. Let's get just a few out of the way: * Accepting lower precision in results is, of course, often done in the name of optimization. In these cases, there is a narrow band of "acceptable" outcomes; a small level of acceptable error that is still called "correct enough", so I'd argue correctness is still massively at a premium. In 3D games, very minor graphic artifacts on the level of 1% loss of "quality" are acceptable if it means a 5x speedup; 2% is probably not. So accuracy is "merely" 5,000 times more important. Getting within a factor of 10^-6 of the "true" result is acceptable in numerical analysis if it results in a 10x speedup, so accuracy is "merely" 10,000,000 times more important. * New graduates and entrants into software development massively over-prioritize optimization and performance, largely because the techniques to accomplish it are a lot more generic (and therefore teachable, and therefore over-represented in their classes) than the techniques to get correct behavior, which is highly specific to every domain. O(n^2) vs. O(log(n)) matters, but as long as you're hitting the correct complexity classes, performance is just not a big deal -- almost always, almost nobody cares. The (1 - almost)^2 times it does matter, you often drop down a safety level and work around the type system. * Static type systems have massively more power to help ensure correctness (by proving certain classes of errors aren't happening) than to improve optimization. You can mathematically prove that your type system prevents X, Y, and Z, and it's up to the programmer to decide if that's worth the restrictions your type system imposes. But optimization? That's all done through thousands of unrelated heuristics that may or may not help, increase the "quirkiness" of your compiled code, are a big source of compiler bugs, and depend on how the programmer writes the code. It is theoretically impossible (halting problem) to prove that any given heuristic is actually helping. Note that you can have a (valuable and loved) type-checker that is not actually a compiler (e.g. TypeScript's). As a rough, 90% correct soundbite: correctness is hard for people but easy for compilers; performance is easy for people but hard for compilers. This is why the few people who are working on bleeding-edge performance tasks are not using higher-level languages that are pushing the boundaries of type theory. They are using C and assembly.

valenterry 3y ago

First: > whenever you introduce a new linguistic abstraction to your language, it may reside either on the statics level, on the dynamics level, or on the both levels. In the first two cases, where the abstraction is located only on one particular level, you introduce inconsistency to your language; in the latter case, you inevitably introduce the feature biformity (...) Then: > One possible solution I have seen is dependent types. With dependent types, we can parameterise types not only with other types but with values, too. In a dependently typed language Idris (...) Great article overall!

nabla9 3y ago

Peter Norvig demonstrated it well using design patterns as an example. Design Patterns in Dynamic Languages http://norvig.com/design-patterns/design-patterns.pdf http://norvig.com/design-patterns/design-patterns.pdf

voidhorse 3y ago

Interesting article. I agree that this double language phenomenon of "biformity" can be a source of complexity, but I actually think the majority of complexity comes from one level higher: the paradigm, as the paradigmatic level is ultimately where assumptions about the modeling of problem spaces lie. The go example in the article is actually an instance of this: kubernetes went ahead and implemented an oop system in golang—why? because they felt go's assumption about the problem space (that it can be modeled and solved as imperative programs) was not a good fit for their actual problem space. Haskell's assumption of purity leads to a problem/solution space that's a good fit for problems that are primarily themselves pure and mathematical, but leads to complexity when it comes to having to solve problems that are not in this space (having to use monads or effects for io) Java's problem/solution space assumes you can model everything as objects and classes and runs into complexity when we attempt to use it for problems that are actually better modeled by other means. Many languages that are "multiparadigm" or "general purpose" really have an underlying problem/solution model driving the organization of programs. When our particular problem is not a good fit for this model, we have to contort and wind up spending more time dealing with language constructs themselves than actually expressing our problem and solution. Couple this with the fact that languages have different performance properties, which may also be a constraint you need to satisfy and things get...complicated. A lazy pure language might be the best modeling system for your problem (e.g. dealing with infinite sequences) but a non-starter due to memory constraints (not enough resources).

klodolph 3y ago
> having to use monads or effects for io Speaking as a Haskell programmer, this is not a problem. You put “IO” in the function signature and “do” in the body, and that’s workable. Or some other Monad. You get so many choices, which is its own problem, but “having to use monads” is not a problem in practice. There are other problems that make Haskell hard to work with. This just happens to not be it.
- staunton 3y ago
  > There are other problems that make Haskell hard to work with. What are the biggest or most important ones in your opinion?

paulddraper 3y ago

> I cannot imagine a single language without the if operator, but only a few PLs accommodate full-fledged trait bounds, not to mention pattern matching. This is inconsistency...Combining statics and dynamics in a single working solution is also complicated since you cannot invoke dynamics in a static context. In terms of function colours, dynamics is coloured red, whereas statics is blue. Yeah, but unless you have some fancy totality checker, that's just the way it is. > Idris: The way out? Yeah okay, like that. > A hypothetical solution should take the best from the both worlds. Programming languages ought to be rethought. --- You can have static checking, "uniformity", or simplicity. Choose two.

lmm 3y ago
One could argue that Idris ends up a lot simpler, through being uniform, than a language like C++ or LiquidHaskell that has to implement the same thing multiple times because of that separation between compile- and runtime.

marcosdumay 3y ago

The lack of union between validating and executing things has been bothering me relatively often, on several different contexts, for many years already. Want to write some CRUD? The relationship between the code and the database is left hanging, and as a result not only the system is prone to failure, but you also have to repeat yourself all the time. Want to write a simulation library? The language won't help you checking the simulation data at all, you have to do that yourself. Want to describe some system for DevOps? There's a reason people use shitty custom languages for it instead of just reusing a dev one. Part of that reason is that you can check things compiling the custom language, but that implies you write the entire compiler. And the list goes on. Somehow it always eluded me that the entire definition of a dependent type system is one that solves this kind of problem. I guess I'm learning Idris soon.

kazinator 3y ago

> Dynamic languages, on the other hand, suffer from these drawbacks to a lesser extent, but they lack compile-time checks. I.e. "The two or three popular dynamic programing languages I know don't have any compile-time checks". Even my modest dialect (utterly not focused on type at all) Lisp can do a thing or two: 1> (compile-toplevel '(let (x) (cons a))) ** expr-1:1: warning: unbound variable a ** expr-1:1: warning: cons: too few arguments: needs 2, given 1 ** expr-1:1: warning: let: variable x unused #<sys:vm-desc: 8da2ac0> 2> (compile-toplevel '(awk ((let (x y) (rng x y)) (prn)))) ** expr-2:1: warning: rng: form x is moved out of the apparent scope and thus cannot refer to variables (x) ** expr-2:1: warning: rng: form y is moved out of the apparent scope and thus cannot refer to variables (y) ** expr-2:1: warning: unbound variable x ** expr-2:1: warning: unbound variable y ** expr-2:1: warning: let: variable y unused ** expr-2:1: warning: let: variable x unused #<sys:vm-desc: 8e6f3c0> 3> (compile-toplevel 'foo.bar) ** expr-3:1: warning: qref: bar isn't the name of a struct slot ** expr-3:1: warning: unbound variable foo #<sys:vm-desc: 8e8dc80> Common Lisp implementations like SBCL have sophisticated type inference. Dynamic programs can do things wrong in ways that are statically obvious.

lmm 3y ago
You can catch the low hanging fruit, sure. But that ends up being pretty useless at scale, because your "checks" can't be relied upon. Or, worse, the programmer ends up having to understand the rules of your type system without having any way to probe or express the types of parts of their program, since your language is pretending that it doesn't have a type system.
- quaunaut 3y ago
  That's only if you don't design your language to be easily inferred. While I don't know the case for SBCL, a language like Elm has very heavy type inference that you can rely on better than most type systems.
  - lmm 3y ago

DarkNova6 3y ago

Dynamic languages have the same type of complexity, but you are not aware of it because it is well hidden. That's a big no-no for building applications.

riku_iki 3y ago
> Dynamic languages have the same type of complexity, but you are not aware of it because it is well hidden I would say you can ignore it until it fails in production.
- DarkNova6 3y ago
  I would HOPE it fails in production. Even better is if you don't validate your response data and suddenly send the wrong data, no data or in the wrong format. Your consumers will love you for it. Of course you can build your own schema + validation logic... or just accept static types and get it for free.

rsrsrs86 3y ago

Author writes about types being applied for ergonomy, which is interesting. Types add static information that can be used by IDEs. But there are other reasons for using type systems: correctness and performance (unboxing, optimization)

Vt71fcAqt7 3y ago

>the statics level is where all linguistic machinery is being performed at compile-time. Similarly, the dynamics level is where code is being executed at run-time. Thence the typical control flow operators, such as if/while/for/return, data structures, and procedures, are dynamic int x = getFizBuz(1) is static, (or should be, in a smart enough compiler) despite `getFizBuz` having if/else in it's definition (if (x % 3 == 0)). This can happen in the real world. For example `button(size: 10)` could have some size dependent logic in its constructor that could be inlined. Any function that is called with static arguments could be inlined and run control flow at compile time.

bbwbsb 3y ago

Dependently typed languages can still develop a degree of biformity via 'tactic' languages. In Coq, for example, you have Gallina and Ltac, which are basically separate languages. This occurs because even with an elegant theorem proving system, you eventually want proof search, and proof search = macros. I'm not sure there is a way out. That said, if dependently typed languages had passable ecosystems I'd use them as is. Not sure if that is more stubbornness than good sense.

cryptonector 3y ago

This is an amazing article. It is the best advert for Idris and Zig, and it is very convincing. The gist, for those who lack the patience, is that a programming language should not have separate languages for defining code to run at compile-time, i.e. types (which can be code, because the type system could be [should be!] Turing complete), and code to run at run-time. That having the same language for both is not just very powerful, but that it leads to less repetition and less frustration and -most importantly- lower cognitive load. TFA is a masterpiece.

chongli 3y ago
I’ll stick with decidable type systems and compilation, thanks. Having to decide whether to kill my compiler because it’s either gone into an infinite loop or it’s got exponential blow up is not very reassuring.

Ericson2314 3y ago

Whenever I see like this, I ask, "have you ever worked on a team? Have you ever worked code without anyone who originally wrote it being around?" Dynamic typing only works small / solo projects and those that love to be obscure for fun. The things they want to do are...largely ill-advised. Because the problem they talk is about is less static typing, but structural vs normal (or transparent vs abstract) types. You can't "reverse an Automobile" for good reason! It is good they are aware of dependent types, but > Additionally, Idris features computational effects, elaborator reflection, coinductive data types, and many-many stuff for theorem proving. With This is attacking a strawman. Yes, Idris is a kitchen sink. But they also don't need any of those features. They could have used Agda for the example, and Agda is quite a small language! And still, I return to the stuff at the top. Reflection, breaking parametricity, etc. are all banned for good reason -- their midwit meme is off it is Zig etc. which are the midwits. Monotonicity (e.g. with traits) and parametricity are important metatheoretic properties for reasoning about code. Bottom line is this person wants to do things I would reject in code review regardless of the language.

leipie 3y ago

The starting premise (paraphrasing here) "strong typing to avoid duplication" for me is simply false. In my experience its main purpose is to reduce mistakes, increase discoverability/predictability and allows for easier refactoring

leipie 3y ago
also strong typing and static typing are two different things

renox 3y ago

What's a bit sad is that now with Zig/Idris you can finally easily make a type checked printf but in the meantime Python use fstrings which are much more ergonomic than prinf and AFAIK you can't make statically checked fstring in Zig nor Idris..