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>

Dynamic programs can do things wrong in ways that are statically obvious.

It's not about what the types themselves are, it's about how they relate to the rest of the program. A type is something associated with terms (roughly, expressions) in a language - you have to have rules for assigning types to every term, or to put it another way you have to exclude terms that you can't type from your language. So saying 2 is of type integer and + is of type integer -> integer -> integer is a start, but for those to be types you need to be able to say that (2 + 2) is of type integer, not just that 4 is of type integer once you've evaluated it.

Unless you replace is with can, you're just spewing dogma, not computer science.

Under a particular paradigm, we can choose to associate types with the nodes in the program's abstract syntax tree, and to have types nowhere else. Then within that paradigm, when we say type, we refer to information attached only to the nodes in the program, and nowhere else.

While that is valid, it doesn't speak to everything that type is or can be.

Even, say, the .jpeg suffix on a file is a type, in a certain context.

Words have to mean something if we're to communicate at all.

> Under a particular paradigm, we can choose to associate types with the nodes in the program's abstract syntax tree, and to have types nowhere else. Then within that paradigm, when we say type, we refer to information attached only to the nodes in the program, and nowhere else.

This stuff predates programming, it goes back to formal language research. That's what type means! If you want to mean something else you should say something else.

Oh? Which ones?

I believe I can fix that, but I can't make a move without a repro test case.

If the language was able to reliably check types, surely they would express that as an actual language feature. If the language creators don't trust their type system enough to call it a type system (and regard any uncaught error as a bug) then why should any mere user do so?

The soundness question is different to the checking ahead of time question but the two are usually conflated under the name "type system".

That's memory safety, a valuable property but nothing to do with types. If you have a sound type system then you can use that as part of your language's memory safety strategy, but that's not the only way to accomplish that.

> The soundness question is different to the checking ahead of time question but the two are usually conflated under the name "type system".

Misusing "type system" to talk about something that checks some runtime property of values is sadly common, but hopefully HN can rise about such muddled thinking.

No, it isn't. It's safety of the kind which asserts that a value of a certain type can only be operated on by suitably typed functions and operators.

The underlying memory may be safe either way: with or without the bad type punning. E.g. if a fixnum integer were treated as a character, that wouldn't be a memory problem, since they aren't heap allocated and both occupy a valid cell of the same size.

All type safety is "bit safety" at the implementation level, because in the actual semantics of the running program, objects are represented by bits, and type safety ultimately prevents bits intended to be interpreted and used one way as being used in a different way.

Memory safety is related to type safety because bits can represent pointers, and pointers can be valid or invalid, or point to objects of only so many bytes and no more.

All type checks related to pointers are providing some measure of memory safety, because if we use a non-pointer object as a pointer, or an object of one size as an object of a different size (all of which are type mismatch errors), we may end up with corruption or a crash.

Nope. Programs can be interpreted by humans, or by non-bit-based mechanical computers. Type safety can be used to enforce a wide range of properties you might want, which don't necessarily have any connection with "how bits are interpreted" beyond the trivial sense in which that's true of everything you can say about a program.

The runtime property of values being checked by the "type system" is the "type" of the value. Something like "you're adding a number to a list, error". Where 'a number' means 'is an element of the set of numbers', possibly defined implicitly by a predicate or possibly explicitly by an enumeration of elements of that set.

When the error is reported (e.g. 'compile time' for some phase separation thing) is one property, which errors are detected is a different one. You could define "type" as compile time detection of syntactic errors, with some hand waving around what errors are, but that's not the only useful definition.

For concrete examples, lisp and python have similar type systems, and forth and assembly have similar type systems, but python's one isn't very similar to assembly. SML is a different thing again. They all have constraints on values that can occur in various contexts.

The system you're describing sounds rather unlike a type system, but in any case it's certainly not what a given lisp implementation is using at compile time, which was the original context of this dicussion. The thing that is being used at compile time in the original comment is almost certainly a type system (because at compile time one has the expression tree, especially in a lisp, and one needs information that there is no other reasonable way of determining); having a quite different thing called a "type system" only adds to the programmer's confusion when trying to understand what the thing that is being done at compile time does and doesn't guarantee.

A static type system associates the syntactic nodes in a program with type.

A dynamic type system associates run-time objects with a type.

I don't see what is so difficult.

It's all objects anyway: in a static compiler, the terms are objects, and get associated with a type. The program graph or tree is dynamically typed while inside the compiler.

The terms of a dynamically typed program can be identified as having type, and diagnosed as well as optimized accordingly. Just if that analysis is incomplete, the program can be compiled and executed anyway, with the safety net of dynamic typing catching whatever hadn't been diagnosed. (Or even what had been, in cases when the diagnostics are warnings.)

No? This is getting into implementation details, but the compiler will need to form a typed AST at least once in order to typecheck the program (technically we can consider that part of the parsing stage - as you say, it's syntactic in a sense - but either way it has to be done), and will generally keep it in that form for at least some of the analysis stages; like any other program you can do this in a more or less typesafe representation (e.g. maybe you allow a function call node to have any kind of children, but you make it easier for yourself if you represent that only callable things can be called). Of course it eventually needs to be lowered into executable form, but that can happen quite late in the process.

> The terms of a dynamically typed program can be identified as having type, and diagnosed as well as optimized accordingly. Just if that analysis is incomplete, the program can be compiled and executed anyway

But you have to actually represent that in the compiler somehow! Your "analysis is incomplete" AST nodes still have to be compiled, and whatever checking/diagnostics you're doing still has to run on them. So there will be a type (in the true sense, something associated with terms in your language) that your compiler ascribes to them, your compiler really does have a type system that it's using when analysing programs - it's just that this type system is not visible or accessible to you, and is confusingly almost-but-not-quite the same as the "dynamic type" system that your language also has.

Diagnostics which have not been made requirements in a language, and are therefore not implemented, indeed cannot be relied upon to be there, and we can write test cases which show that some situations would benefit from those diagnostics (all else being equal, which it usually isn't). Under TDD, we can write a test case that fails for something that is not implemented and not a requirement (but about to become one).

That's a different claim though.

I am saying that. You can't rely on something that's not part of the specification (formal or otherwise). If I call an unknown function and f(2, 3) = 5 and f(7, 8) = 15, I would still be crazy to trust that f is the plus function if it wasn't actually documented or specified as such, even if I haven't come up with a concrete test case where it isn't yet.

Bullshit. Either it's a sound type system (perhaps with some escape hatches) - in which case why would you ever not expose it as a real static type system - or it's not and you can't rely on it.

(There is no contradiction between having good inference and having a real static type system; e.g. if you're using Hindley-Milner then you have "perfect" type inference where you could remove all the type annotations from your program and it will still be correctly typed. But it's still very useful to have a syntax for annotating expressions with their types!)

And of course if you really want an ML style BDSM type system in Common Lisp there's Coalton[1].

[1] https://github.com/coalton-lang/coalton

Then they're not types. Types go on terms, i.e. expressions, not on values.

> This presents some code generation challenges, but it will warn on correctness just fine.

Warn on correctness it may, but it's simply impossible for a setup like that to reliably error on incorrectness at compile time; a Turing-complete language like Common Lisp cannot determine any nontrivial property of expressions (in a way that works in all cases) without evaluating them. If your types go with your values then you can't check your types without evaluating your values, at which point compile time is long gone.

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).

I don’t think this was ever an objective, can you clarify what you mean by “oop system” and where we implemented it?

We aggressively used composition of interfaces up to a point in the “go way”, but certainly in terms of serialization modeling (which I am heavily accountable for early decisions) we also leveraged structs as behavior-less data. Everything else was more “whatever works”.

> why? because they felt go's assumption about the problem space (that it can be modeled and solved as imperative programs)

You’d have to articulate which subsystems you feel support this statement - certainly a diverse set of individuals were able to quickly and rapidly adapt their existing mental models to Go and ship a mostly successful 1.0 MVP in about 12 months, which to me is much more of the essential principle of Go:

pragmatism and large team collaboration

> Unknown to most, Kubernetes was originally written in Java. If you have ever looked at the source code, or vendored a library you probably have already noticed a fair amount of factory patterns and singletons littered throughout the code base. Furthermore Kubernetes is built around various primitives referred to in the code base as “Objects”. In the Go programming language we explicitly did not ever build in a concept of an “Object”. We look at examples of this code, and explore what the code is truly attempting to do. We then take it a step further by offering idiomatic Go examples that we could refactor the pseudo object oriented Go code to.

The only real abstraction we need from Go is zero-cost serialization frameworks, which I think is an example of where having that would compromise Go’s core principles.

> Golang] Kubernetes, one of the largest codebases in Golang, has its own object-oriented type system implemented in the runtime package.

I would agree that Golang is overall a great language well-suited for solving a large class of problems. The same is true for the other languages I cited. This isn't about immutable properties of languages so much as it is about languages and problems fitting or not fitting well together.

I find it amusing that the runtime registry code is cited as an example for anything other than it’s possible to overcomplicate a problem in any language. We thought we’d need more flexibility than we needed in practice, because humans involved (myself included) couldn’t anticipate the future.

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.

Unfortunately, most programmers trying to learn Haskell have not taken any abstract algebra courses, so these definitions and laws are deemed insufficient. Regular people want to know the exact nature of a thing — not just a list of mathematical properties that hold — and so they insist that there must be something more. But there’s nothing there!

I think chongli is actually in agreement with you

:)

What are the biggest or most important ones in your opinion?

The other common problem I see is not actually a Haskell problem but merely a problem Haskell exacerbates: many students fail to think through their types prior to starting an implementation. I frequently had students in office hours trying to force their way through a problem and when questioned about the types were unable to reason at the type level intuitively. I suspect this reflects larger problems in my university's undergraduate program, but I figured I'd comment on it anyway.

I've only heard that from people who haven't written Haskell or have written 1 app without soliciting code review.

I have written a lot of haskell and it is my favorite language. It is a great language for domains that can be mathematically modeled and such applications can be very practical (e.g. programming language compilers) It is objectively better than pretty much every other language at this. As I also mentioned, Haskell is likewise great for anything that naturally benefits from lazy execution. That said, is it as convenient to write certain classes of applications in haskell? No. I think you'd have to be a delusional fanboy to argue otherwise. You can be a big fan of a language and its ideas while still recognizing that it is not an all-encompassing solution or the best for every possible problem. This language fanaticism mindset is not rational nor what you want from engineers who should be deciding what language to use based on how well its properties fit constraints and not because its their personal favorite.

Certain classes, of course. GPUs, high-performance computing, compile-to-javascript, GUIs- Haskell isn't terrible but there are better alternatives.

But usually what people mean when they go on about how Haskell is "mathematical" and "not pragmatic" is that it's worse than C/Java/Python for ordinary general purpose programming: CRUD, web backends, command line tools, etc. And this simply isn't true.

As a real world programmer your comment is just another "Haskell isn't good for real world IO heavy problems" argument that ironically doesn't hold up in the real world.

Your concession of "good for pure and mathematical" just evokes "ah yeah, the ivory tower language unsuitable for real world applications". It ends up making your view seem balanced and authoritative while bolstering your overall point that you shouldn't use Haskell for serious non-academic things.

Haskell isn't my pet language, it's the language that pays my rent :)

Absolutely the opposite in my experience! Haskell is the best language for effect-heavy code precisely because of the fine-grained control over effects that it provides.

This is why I think devs should know multiple languages, and at least one language from each major paradigm. You don't want a toolbox with only one kind of tool in it.

That's an old understanding by now. Just use interfaces and forget about inheritance.

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.

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.

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

  type Whatever_Name is mod 10;

Like in

  int32 y=INT_MAX
  mod32 x=1
  y+=x

> you can overload the + operator

I fail to see the need. (Sorry I'm a bit tired). In this thread context of static languages, your compiler knows the target type of an assignement (clip/mod) and so applies the right correction.

> in python there's simply no overflow, every int is an object that can be as big as needed

I guess there's a huge speed penalty in wrapping values into objects.

Y=(x+x)+y

What is the target type for x+x?

You could argue that you can have the same problem with operator overloading. But then again, it is best to implement the class just for a specific (type of) algo whithin which you use the overloaded + operator (or maybe better another symbol, resembling a + sign) in an unambiguous way. Also the class might have more functionality specifically suited for that type of algo. The benifits are less ambiguity and, that normal operations keep being fast (directly use the cpu arithmetic functions); the code is only slower where clipping or something the like is needed.

Python is indeed slow and resource intensive, that's where libraries like numpy fit in. It uses vectorized native types (numpy ints and floats are native machine types), together with vector operations running in a precompiled low level language. Python only sees the 'outside' of the vectors as python objects.

I once wondered why my language did not have native support for fixed point type operations. Once i started implementing custom types for and a class supporting fixed point, i noticed the sheer amount of design choices that were needed. A concise generic implementation of it is nearly impossible.

> What is the target type for x+x?

There's no 'target' except the assigned 'y'. The compiler would just do

  y = CLIP((x+x)+y)

> i noticed the sheer amount of design choices that were needed

I was just imagining these types. You are most certainly right that it would be pretty involved to get right.

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-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-pr...:

“When you mark a member declaration with the dynamic modifier, access to that member is always dynamically dispatched using the Objective-C runtime.“

it clearly telegraphs that someone is doing something either clever, stupid, desperate or all three.

An advantage to C#'s dynamic over Reflection.Emit is that it uses System.Linq.Expressions under the hood. There's a lot of cool advantages to do that, including higher level caching and sharing a lot of the same infrastructure of IQueryable (and IQbservable, the Q there is not a typo). The DLR remains an underappreciated bit of great .NET engineering. (It doesn't help that most of the Iron languages went to maintenance bitbuckets.)

(In a past life I did some amazing things with the DLR.)

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.

Class methods have incorrect variance, even with the 'strictFunctionTypes' setting: 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
    }

    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
    }

    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?'

    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!

    const x: Record<string, string> = {}

    const x: (s: string) => string = (s) => {}

Leave the type system simple enough that you can take a rest and let the computer do the typing work for you.

just make everything non null and use option/maybe to indicate absence

wayyyy simpler

This means giving up on first-class functions.

Additionally, why would having only invariant functions mean leaving 'first-class' functions? Even assuming subtyping relations between types (simple or complex), invariant functions would still be 'first-class', just not acknowledging of the subtyping relation.

So... first-class functions with no covariance, contravariance?

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.

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.

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.

You should never do this: `any` is infectious. Assert the particular type judgement you want instead: `as number`, `as ({dispatch: () => void})`, etc.

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.

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.

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.

That's a big no-no for building applications.

I would say you can ignore it until it fails in production.

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.

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.

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.

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.

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.

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.

But people are driven to them for several reasons. They are a flexible tool that you can use to make your programs shorter, easier to read, less repetitive, faster to run, less prone to mistakes, easier to modularize, etc. (But, of course, not all of those at the same time.)

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.

Hmmm. Well, I wouldn't go that far as to say never, not on a warming earth, anyway.

Incorrect, optimized (but non-critical) code that fails .1% of the time, but consumes 1% of the resources of a correct alternative may actually be preferable from a global warming perspective.

Only if it fails in known, predictable ways. In that case, I think it falls under the accuracy tradeoff where you define a narrow band of acceptable correctness (99.9% accurate), and correctness is "merely" orders of magnitude more important than performance. If your code fails in unpredictable ways 0.1% of the time, you basically cannot use it. It doesn't matter if it's non-critical: an idle clicker game that has a 0.1% chance of bricking the user's computer or deleting some random data from their system is not usable.

What’s not true is that just having more information automatically means better optimized.

> 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!

Design Patterns in Dynamic Languages http://norvig.com/design-patterns/design-patterns.pdf

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.

Namely these two do not compute:

> if you choose the C-way manual memory management, you will make programmers debugging their code for long hours with the hope that -fsanitize=address would show something meaningful

> Zig can still be used in large systems projects like web browsers, interpreters, and operating system kernels – nobody wants these things to freeze unexpectedly.

But Zig isn't meaningfully safer than C. So you still get to debug code for long hours hoping you'll spot the error.

it's not? why would anyone bother using it then?

Here is Zig UB in a nutshell

    const std = @import("std");

    pub fn main() !void {
      const warning1 = try powerLevel(9000);
      const warning2 = try powerLevel(10);

      std.debug.print("{s}\n", .{warning1});
      std.debug.print("{s}\n", .{warning2});
    }

    fn powerLevel(over: i32) ![]u8 {
      var buf: [20]u8 = undefined;
      return std.fmt.bufPrint(&buf, "over {d}!!!", .{over});
    }

Nope, you're spot on: better refactoring and increased correctness are the biggest motivators for type systems to exist... I don't even know what the author means by suggesting that a strong type system avoids code duplication (as someone who has used type systems for decades)!! Can someone illuminate?