Hacker News Reader

> What thing that violates a type check would be "perfectly fine to do"?

One good example is where you might treat records or "product types" as maps

Let's say you want to write a function that can capitalize all the string fields in the object passed in. In a dynamic language, you could map over the values and apply capitalization trivially. It would be a one-liner.

In a static language, you'd have a few options, but none are great:

1. You could use "reflection" or some dynamic feature to do this, but lose type-safety

2. You could make the function take in the union of all possible data types in your system, and then write a mapping function for each one. Then you're duplicating the logic N times, or at the least writing a lot of conversion boilerplate.

3. You could write two functions for each data type in your system to convert to a Map<String, Object> or some such and back, which lets you operate on the maps. Again, lots of boilerplate. Maybe you use code-generation for this? That would add complexity.

In reality, you probably wouldn't even try to write such a function in a typed language because of how awkward it is. Maybe you'd just write specific translation functions for the records you know you happen to need. But I think that's what people mean when they say you're restricted by the type-system - because it can't verify those types of operations, you find workarounds when maybe that would have been the easiest way to implement something.

It's pretty easy to do in Typescript and loses no type safety (without needing to assert or cast anything)

    type T = { [k: string]: number };
    
    const t: T = {
      one: 1,
      two: 2,
      three: 3,
    };
    
    const makeUpperCaseKeys = (v: T): T => {
      const keys = Object.keys(v);
      return keys.reduce((p, c) => {
        const key = c.charAt(0).toUpperCase() + c.slice(1);
        return { ...p, [key]: v[c] };
      }, {});
    };
    
    console.log(makeUpperCaseKeys(t));
    // {
    //   One: 1,
    //   Two: 2,
    //   Three: 3
    // }

That's great! Are you making the argument that I won't be able to find an example where doing some transform in a type-safe way is awkward in TypeScript, or just that this one example can be done in TypeScript?

By the way, my example was meant to be more like User -> User where there are some string values and some other types of value. You want to do the transformation in a generic way, but still have the type-safe object come out the other end with all the expected keys.

You can try this with typescript 4.1 :

interface User { name: string; age: number; }

type CapitalizeProperties<T> = { [Property in keyof T as Capitalize<string & Property>]: T[Property]; };

type CUser = CapitalizeProperties<User>;

var c : CUser = { Age: 17, Name: "john" }

You can check that the autocompletion works on the c variable.

https://www.typescriptlang.org/play?ssl=1&ssc=1&pln=15&pc=2#...

There is no limit on the number of problems easier to solve using dynamically typed languages. For an individual hacker, dynamically typed languages make a lot of sense. I don't forget what types my functions accept as I am writing a program. All static typing can accomplish is slow me down when I'm trying to bang out something. This is why Python (for instance) is loved by data scientists, researchers, and startups. And they're right to love it! Purely anecdotal, but I can accomplish more faster (from a clean slate) with a dynamic language like Python than I can with Haskell, Go, or Rust. The difference is small, but non-negligible.

But static typing has a few key benefits:

* No searching through comments for type constraints.

* Better autocompletion.

* Better compilation.

* Better serialization/deserialization.

I do think static typing pays for itself in the long term. Sometimes, we shouldn't care about that. Engineering means managing tradeoffs: short-term velocity vs long-term performance and maintainability?

>There is no limit on the number of problems easier to solve using dynamically typed languages.

So, some examples? Also examples where "easier" is not just "you don't need to write types". That goes without saying...

how about using something like clojure.spec where you need it most to help make that long term payment?

It's an interesting take. e.g. provide specs/types across module boundaries only. Gradual typing is certainly becoming popular. Meanwhile, statically typed languages are adopting type inference. Some people only write the types for the exports in their modules. The two worlds are coming closer. More statically typed languages are adding dynamic type information (like Go). More dynamically typed languages are supporting static type markup (like Python).

The auto-completion is purely Python's dynamic-dispatch problem though. Lisp has symbol-based auto-completion which doesn't suffer from the same issue (search is a different story!).

This sounds terribly controversial, but I would love to know /when/ the static-typing pays off compared to a looser approach like sound-gradual typing (where you basically export types at a boundary and make sure that you don't violate those).

I do wonder whether a better approach is to prove your code in some other language (say Z3, Agda, Coq) - then implement it in something else, making sure you can prove isomorphism. This has quite a few benefits; you're not tied to a constructive proof on the type-level ala Haskell, Rust, Go etc... and you can automate a large part of trivial proofs.

> I would love to know /when/ the static-typing pays off compared to a looser approach like sound-gradual typing (where you basically export types at a boundary and make sure that you don't violate those).

When you are in a codebase where you don't know which modules have been soundly typed, and which ones are still in the 'gradual' phase.

The fascinating thing about Python is the ability to write functions where the parameter can intake multiple data types.

I haven’t quite seen another language handle it this elegantly as Python does.

Then, inside the function, you can check the parameter’s data type, and handle it appropriately. And error out immediately if the wrong type is passed in.

This allows you to operate on the data at a more logical level (what it implies), as opposed to just at the technical level (what data type it is).

For example, you can pass in a single string, or a list of strings. And your function can check the type and handle it appropriately.

In C++ and Java, because of the rigidity of the function declaration, in order to do something like this, then you would need to create multiple functions to handle each of the different types that you want to allow. Then you’d need to create a wrapper function to dispatch it to its appropriate sub function. That becomes a complete mess after a while.

C# has an is operator as well. I found it useful with generics.

Coming back to even your own ~+1KLOC project after 3 months of working on other things, compiler enforced types can help you jump right in

> There is no limit on the number of problems easier to solve using dynamically typed languages

40+ years of programming experience here + a language geek. I have for years programmed in both dynamic and static languages to find out what works best for me. My conclusion is that problems are easier to solve with statically typed languages. So clearly different languages works for different personalities.

One more that people easily forget. An IDE or LSP can detect much more errors as you type, saving quite a lot of context switch of mind.

Clojure gives you tools like spec https://clojure.org/guides/spec or Mali https://github.com/metosin/malli for schemas on data. Beats static typing IMHO.

As a proponent of static typing (at least for larger programs): thank you, that was a very enlightening example for when dynamic typing can be superior to static typing.

>1. You could use "reflection" or some dynamic feature to do this, but lose type-safety

By using reflection you only lose type-safety for this particular function. With a dynamic language, you lose it everywhere.

And it's still an one-liner or close in a language without much ceremony (e.g. not Java 1.5).

Example implementation (pseudo-code):

  fun capitalize (o: object) -> [f.toUpper() for f in 
  reflection.fields(o) if reflection.type(f) == "string"]

I reject the claim that it is reasonable to capitalize all the string fields of arbitrary objects.

But it can still be done, like you mention, by using reflection. Now, you claim that it is unsafe. This is untrue, it depends how the reflection works. Even if it were unsafe, it would be no worse than in Python, where you get a TypeError or in JavaScript where you get undefined, which probably leads to a crash later.

For an example of reflection which is safer than just a string-dictionary like JavaScript or Python, see GHC.Generics. It works by compile-time generating a type safe structure which is not just a dictionary. The function you want would have a signature involving this constraint, "Generic x => x -> x", which means it works for any "object" implementing the Generic interface.

Now you may say "but I asked for a function that handles all objects", but I don't see the point. In statically typed languages you get an additional option of using generics when you want. It doesn't make sense to me to require all types to implement reflection when you don't actually need it everywhere.

That's not a very compelling example - in most statically typed languages the object field names are not actually stored in member, so it makes no sense to want to do runtime operations on them, because they don't exist by the time the code is compiled.

That's why you find it hard to do in a compiled statically typed language - because it's not something that really makes any sense.

> Let's say you want to write a function that can capitalize all the string fields in the object passed in. In a dynamic language, you could map over the values and apply capitalization trivially. It would be a one-liner.

That's fair, but can you explain the context here? I.e. why are we trying to capitalize all the field names of a record object? This may be an 'XY' problem--you may be trying to accomplish some final goal and 'capitalize all the field names of a map' seems like an obvious intermediate step to you, while to a statically typed language programmer they may take a very different approach.

> In reality, you probably wouldn't even try to write such a function in a typed language because of how awkward it is.

In reality, you probably wouldn't because of how contrived and completely removed from any conceivably realistic practical goal this example is. In what situation would I actually need to solve this problem for every type in my program?

> If value is not a numeric type, square is not going to be happy.

That is not necessarily true. In Common Lisp, with its generic-function based object system, you can extend the operation of any function at any time to cover new types. So, for example, one could define a method for SQUARE that operates on matrices.

> What thing that violates a type check would be "perfectly fine to do"?

(define (self-apply fn) (fn fn))

> (define (self-apply fn) (fn fn))

Out of curiousity, what would be a practical application of this?

See:

http://www.flownet.com/ron/lambda-calculus.html

That didn't answer my question. Let me rephrase it: When would you use

    (define (self-apply fn) (fn fn))

in an actual, real-life situation (outside of teaching lambda calculus)?

Without additional arguments? Never. With additional arguments, it provides the function with access to itself.

This could be used "under the hood" in an implementation to bootstrap the ability of named local functions to have themselves in scope, which is useful for writing ordinary recursion.

Compilers and interpreters can achieve such a thing without any such jig like a Y combinator, because interpreters and compilers work with environments that are re-ified as objects. They are free to manipulate environments and evaluate/compile any piece of code in any environment they see fit.

Personally, I consider teaching the lambda calculus to be a real-life situation. Teaching the lambda calculus is no less real to me than any other part of my life. But OK, self-apply is not something you're likely to see in production code, and neither are Church numerals, which is where this problem shows up for real. But MAP, REDUCE, and APPLY are, and they all have the same problem as self-apply: their static types are infinite.

This is a general problem with all static type systems. There are only two possibilities: either your type system is Turing complete or it is not. If it is not, then there are things that one might reasonably want to express that cannot be expressed, and if it is, then it is undecidable. Static typing is either constraining, or it is a Turing Tarpit (https://en.wikipedia.org/wiki/Turing_tarpit).

> But MAP, REDUCE, and APPLY are, and they all have the same problem as self-apply: their static types are infinite.

Huh? Any semi-decent static type system has no problems modeling higher-order functions, and static types can easily be infinite via parametric polymorphism ("generics").

> Static typing is either constraining, or it is a Turing Tarpit

You're letting the perfect be the enemy of the good. Static type systems can be beneficial even when they don't solve every conceivable problem.

> Static type systems can be beneficial

I don't deny that. The problem is not with the idea, it's with the (usual) implementation, which is that if you don't appease the type-checker it won't let you run your program. I'm perfectly fine with a type checker that only gives me warnings but still allows me to run the code even if it isn't satisfied.

Most implementations of Common Lisp prevent shadowing builtin symbols. You get compile/runtime error like "lock on COMMON-LISP package violated". So, unless author went to extra lengths to work around it, you can rely on the standard stuff like * when you read the code.

Even for user-defined functions, it's not an usual practice to extend operation of any function (although again, it's kind of possible). There are CLOS generic functions for that.

> Most implementations of Common Lisp prevent shadowing builtin symbols.

So? Make your own package.

What's your point? In CL it is trivial to determine both at compile and at runtime the package of all symbols involved. Same for generic methods, you can query the runtime which methods it is going to use for some concrete combination of parameters. Much easier than to determine how which overload of a C++ operator does the compiler/linker deem to fit in given context.

My point is that this:

> Most implementations of Common Lisp prevent shadowing builtin symbols.

is irrelevant. It's actually irrelevant for two reasons. First, the example under discussion was SQUARE which is not a CL builtin, and second, even if it was, you could just do this:

Just make your own package and do:

(in-package :my-package)

(defmethod square ((n number)) (* n n))

Now you can extend SQUARE to work on things other than numbers. Or, to pick a more realistic example:

(defmethod sqrt ((n number)) (cl:sqrt n))

Oh that's the misunderstanding, I was talking about overloading of the '*' operator and the consequent confusion, not overloading of 'square'.

* is not an operator in Lisp. It's a function. Lisp doesn't have operators.

To be more precise, cl:* is a function. But you can make a symbol named "*" in another package and define it however you like.

> What thing that violates a type check would be "perfectly fine to do"?

Here is an example limitation of typescript's type system that I routinely run into while developing real code [1].

I look at it like this. If you consider all possible programs, some are invalid, some are valid, and some are valid and useful. A type system's job is to reject as many invalid programs as possible while accepting as many valid programs as possible and trying to optimize for useful valid programs. Due to the halting problem this is impossible to do perfectly, so any given type system will likely accept some invalid programs and reject some useful valid programs. If the type system happens to reject your useful valid program, you'll likely have a bad day :)

[1] https://www.typescriptlang.org/play?#code/PTAEHUFNQCwQwG7TgO...

Sometimes the type system is forcing you to think in terms of what it is that you are passing around. In this case, getEmails() isn't expecting a group of students or a group of faculty, but rather a group of people that can be emailed. You can introduce an interface of that type and have it inherited by both Student and Faculty and use that in the method for clarity and type-safety without over-relying on union types: https://www.typescriptlang.org/play?ssl=1&ssc=1&pln=38&pc=30...

I appreciate the effort you’ve both put in to concrete examples. I think yours gets to a point that I haven’t often seen stated. You’ve named your interface Person, but perhaps even Emailable could serve the purpose. The problem is that you had to name it. Naming well is hard, and I believe strong type systems often create a need for more names. It’s a cost I don’t often see considered in the tradeoff.

Instead of giving the interface an explicit name, I think you could instead use something like this:

    function getEmails(group: Array<{email: string}>) {
        return group.map((p) => p.email)
    }

which leaves the function more open ended than relying on an explicitly named interface that other types then have to inherit from.

> And such errors happen all the time, the same way without syntax checks typos happen all the time.

No they don't, because syntax is richly varied and nested, even in programs whose "type story" is bland.

For instance, in some numerical program, there are lots of opportunities to make typos in the syntax, but the type of just about everything may be either float or else array of float (possiby string, if it has any error-handling code with messages, and bool if there are some logical operations).

If you pass an array of float where a scalar float is expected, such that an error occurs, and if you don't catch this in your testing, it means you're not testing the code.

Untested code is of a dubious status, even if it compiles with a static type system; testing is not negotiable.

Note that functions like sin and cos have exactly the same type signature, yet it is disastrous if you mix them up. Static type checking doesn't help. Static type checking also doesn't help with mixed up variables: calling f(x, y) which should have been f(y, x) or something else, where x and y have the same type.

In programs, chunks of code that are put together into the same module or function often work with multiple instances of the same type. It's more important not to mix up those instances, than to worry about type errors. The code could be wrong in all sorts of ways, yet statically check.

That's where you need to step up the the argument into "True Scotsman's type systems territory": a sufficiently advanced type system can encode all those properties that prevent the mixups that the everyday type system doesn't. Yeah, well, nobody uses that; nobody understands it outside of a narrow slice of academia. Examples of the technique are such that encoding even a trivial property like "list is in sorted order" results in an a considerable increase of program complexity all concentrated in one place, and less easy to understand than a set of test cases against the obvious program. Yet, it doesn't eliminate the need for testing; nothing does. There can now be a bug in the way the desired property was encoded into the program. Perhaps the sorted property was correctly encoded, but it should have been descending order. The test case will catch it.

When you have a language that is available at compile time, you can execute test cases as part of compilation. Test cases are therefore static checks. Anything happening at build time is a static check. Heck, how a git commit message is formatted is a static check, if a repository commit hook validates it.

> Note that functions like sin and cos have exactly the same type signature, yet it is disastrous if you mix them up. Static type checking doesn't help.

I agree with you. I am hard-pressed to imagine types (where it's static analysis or anything at all) offering any help in catching inadvertent swaps of sin and cos.

One thing that types could help with is avoiding confusion between e.g. radians and degrees. Even this I believe is quite a challenge, because the quintessential (in my opinion) example of static analysis and types as they arise in science and engineering, the SI units and dimensional analysis, take radians to be dimensionless and therefore do not distinguish the input and the output types of e.g. sin (Radians).

I personally believe this problem is rectifiable beyond the SI type system (or who knows, within it), but not at no cost. I believe the choice to not distinguish the input and output types of e.g. sin (Radians) is rooted in many different practical considerations, and points to the difficulty of formalizing types in practice.

> Test cases are therefore static checks.

I don't agree with this unless you are talking about tests that perform some kind of symbolic execution / static analysis within them. What static analysis grants you is checking a "for all x" claim, without literally checking each x. You can argue that for any given static analysis system, the kinds of claims it lets you check are not that useful in practice, and I would agree in many situations. But having a finite number of test cases that tests some x is not the same as testing for all x.

Unit tests, maybe not, but it's commonly accepted even in statically-typed communities that property-based tests are practically as good to guarantee properties which a stronger type-system would catch.

For example in Haskell almost all of the abstractions (Monoid, Semgroup) use property-based testing rather than proofs.

An example:

> y = [1] ++ [2] ;; Assume types List[Int], List[Int]

> y[0] ;; This should return Union[Int, None]

> y[0] + 3 ;; This should fail type-checking

You /know/ the list isn't empty. Sure you can argue that /maybe/ we should be using NonEmptyList, but now imagine this code.

> y = [1, 2] ;; NonEmptyList[Int]

> y = (filter (lambda x: x % 2 == 1) y) ;; Has to return List[Int]

> y[0] ;; Union[Int, None]

Again, we hit into type issues.

The type system is a proof system. In your examples, the types do not imply the invariants that you want.

Does this mean that the type system is faulty? No! It just means that you need to e.g. get a more expressive type system, document code properly, use smart constructors. There are many tools.

Nobody said you can trivially prove everything using type systems. So what are your examples showing?

I see your code, but I don't know what you're actually trying to do. One interpretation could be, that you want to prove that for the naturals (excluding 0), up to and including 2, there is an odd number. Can one prove this using type systems? Definitely. If you read Software Foundations, you will know how.

Sure - but the point is that there are /diminishing returns/ on type-systems. The question is then, /where/ should one draw the line when trying to prove certain properties of code; which properties are worthwhile proving?

Are you /seriously/ suggesting that one should use Agda or Coq for most code?

EDIT. The original comment was suggesting as though dynamic and static type-systems are a dichotomy. I was pointing out that it is a sliding scale from nominally-typed ala Go, all the way to dependently-typed languages; and that's not even including model-checkers!

It depends on how sophisticated your type system is. For a pure HM type system, anything requiring rank-n types won't type check, but are theoretically sound in a type system that supports them.

Squaring is usually value*value.

(a minor nit that shouldn't detract from your point - since in a dynamic language, you'd have potential type errors in addition to this sort of thing...)

>Squaring is usually valuevalue.*

This version is optimized for the value of 2! (thanks, checked).

> What thing that violates a type check would be "perfectly fine to do"?

A typical example, in dynamic programming languages, is to treat numbers as strings and vice-versa; evaluate lists in boolean context; and so on.

> If value is not a numeric type, square is not going to be happy. And that's the case with most (all?) dynamic code.

Some programming languages will be glad to accept a string and treat it as a number -- see Duck Typing (https://en.wikipedia.org/wiki/Duck_typing).

Can you give an example of where doing this is useful?

that sounds really awful, not "fine."

> A typical example, in dynamic programming languages, is to treat numbers as strings and vice-versa

That sounds great until it bites you in the ass really hard. In general, you want to catch unintended behavior as early as possible.

You want to, but they don’t. Those people just want to get stuff done, as opposed to a language like Haskell or stricter where you’ll never be able to get old code to run because newer compilers print errors that take a week to understand. There’s some old Yegge articles about this…

PHP converting between strings and numbers is usually a mistake, but the one data structure doing everything (array and dict) is nice enough.

I don't think that is necessarily a dynamic language thing: that seems like your regular ad hoc polymorphism. Pascal allows it, IIIRC. So does C#. Being able to use a function on different kinds of arguments is orthogonal to the typing discussion.

Scheme, for example, is dynamic yet very monomorphic. You have length (working only on lists), string-length, vector-length, bytevector-length etc.