Dynamic type systems are not inherently more open • Hacker News Board

Re: Dynamic type systems are not inherently more open

#221

Post by choeger » Sun, Jan 19, 2020, 8:54 PM UTC

millstone wrote: post #217

I wrote the pickle.load comment [1]. I want to defend it here. King (the author) places "dynamically typed" and "statically typed" in opposition. But keep in mind that many languages have both: Java, ObjC, TypeScript, C#, etc. I like to say that a a language "has" static and/or dynamic types, but "is" dynamic if it supports runtime features like reflection - of course this is a sliding scale. King observes that stati…

I can easily write you pickle in Haskell. In fact you can easily embed Python's single type in Haskell and thus do everything you can do in python.

The difference to Java has nothing to do with reflection, really, but rather with a uniform object representation (in Java you know the shape of all values by default).

Re: Dynamic type systems are not inherently more open

#222

Post by erik_seaberg » Sun, Jan 19, 2020, 8:54 PM UTC

sethev wrote: post #189

svat wrote: post #90

Six notable things I took away from this post: - Structural typing, i.e. instead of "you eagerly write a schema for the whole universe", just limit to what you need (basically, encode only the same kinds of assumptions you would make in a dynamically-typed language). - It’s easy to discover the assumptions of the Haskell program [...] In the dynamically-typed program, we’d have to audit every code path — Left implici…

I thought the article was good and addressed a real point of confusion, as evidenced by the two included comments (from Reddit and HN). You can consume arbitrary data using a program written in a statically typed or dynamically typed language. Whether it's decoupled from changes in the data depends on how the code is written and the data model, which have nothing to do with static vs dynamic typing. To me the stronge…

> the boundary between programs is dynamically typed

Many interfaces have declared, enforced static types. I don't have to write any code to handle

  SELECT birthdate FROM employees WHERE id = ?

returning "fish" because the database would never let it happen.

Re: Dynamic type systems are not inherently more open

#223

Post by pron » Sun, Jan 19, 2020, 8:54 PM UTC

Silhouette wrote: post #183

pron wrote: post #95

Earlier quoted context omitted.

Not all untyped languages are the same. E.g. Clojure now encourages specifying assumptions with spec annotations, some of them are stronger than those that can be expressed by Haskell's type system: i.e. they can succinctly express more about the "entire code" than Haskell's types. Types are not the only way to write formal assertions and assumptions about code. The difference between the two is in the level of sound…

My guess is that types would be better for enforcing code organization and for tooling ... while contracts are better for correctness I see what you're getting at, but there is one other crucial difference: the types we're talking about here are usually checked at compile time, whereas the contracts we're talking about here are usually checked at run time. Although the latter may be more expressive if other things ar…

> whereas the contracts we're talking about here are usually checked at run time

No, they can be checked in many different ways, hence their power. They can be checked "statically", i.e. at compile-time, or dynamically. One approach is sound but requires more effort, while the other is cheap yet unsound -- and there is a spectrum in between the two extremes.

> If you're writing a program that is going to control a satellite and software maintenance after launch is extremely expensive if not impossible, it might matter a great deal.

Such programs often use formal methods that precisely use such contracts. Rich type systems (like Idris's) are virtually never used in practice in those cases. If you've heard of SPARK, it's a language that provides static verification of properties specified as contracts, not as part of the type system, and it is used in some safety-critical realtime applications.

Re: Dynamic type systems are not inherently more open

#224

Post by yawaramin » Sun, Jan 19, 2020, 8:55 PM UTC

Barrin92 wrote: post #202

hyperpape wrote: post #112

Earlier quoted context omitted.

I think it's absolutely addressed. With either a dynamic or static language, you have to make decisions about which fields are essential, whether you can ignore additional fields, etc. And this post shows how you can do that in Haskell. Versioning is hard, because it's a coordination problem, but it's not the type system that produces the pain.

> And this post shows how you can do that in Haskell. the actual critique of the first post wasn't really that Haskell can't do it in a literal sense, but that ignoring or reasoning about unknowns diminishes the advantages of static typing. Sure, you can define an "unknown" type if you want and make your static language as permissive as possible, but then you lose the actual static guarantees, which is automating rea…

> ignoring or reasoning about unknowns diminishes the advantages of static typing.

Ignoring the unknowns that are unnecessary to solve the problem at hand, is literally the essence of software abstraction. Why would you want to do more work than is necessary to solve a given problem?

> you can define an "unknown" type if you want and make your static language as permissive as possible

And 'unknown' type doesn't make the language permissive. Since the type is 'unknown' it doesn't permit any operations at at all on it. Hence, the opposite of permissive.

> you lose the actual static guarantees, which is automating reasoning about the correctness and capacities of your program at compile time.

You absolutely don't lose the actual static guarantees which are actually relevant to solving the problem your program wants to solve. If your program's job is to add a signature field to a JSON object, why would you want to parse and decode the entire JSON object into a strongly-typed value? You would just parse it into a reasonable Map data structure and add the signature as a key-value pair to the Map.

> you're already conceding that there are so many unknowns which better ought to be dealt with at runtime

That's exactly what we're not doing here, we're creating software abstractions which again, is an essential part of software development. Please see Liskov & Zilles, 'Programming with Abstract Data Types', 1974.

> what is there to be gained from making that explicit in your program

What you always gain from static typing–exposing the assumptions and invariants of your code as first-class parts of the code, making it easy for readers to understand at a glance what they are, making it easy to change the code with compiler assistance to ensure the invariants are honoured.

Re: Dynamic type systems are not inherently more open

#225

Post by leshow » Sun, Jan 19, 2020, 8:56 PM UTC

azhenley wrote: post #163

leshow wrote: post #160

Earlier quoted context omitted.

I'm curious why you quote this like it's a fact when it's an opinion. The understanding of type inference used as the basis for making the argument in that blog post is superficial. Type inference doesn't just allow you to leave off type information from variables. A good inference engine will infer the most generic type for variables (and functions!), it's a discovery that you can query the compiler for in order to…

I quoted the title of my blog post. Do you have any evidence for your claim that it increases readability or usability? A few human-subjects studies from different labs have recently been ran on this and the findings mostly agree with my opinions. Papers forthcoming.

Agree on what? "Type inference" is a broad feature, feel free to post the resources.

edit: In Haskell it goes beyond just locally inferring variables, it enables a new type of development with typed holes that feels more like a back and forth conversation with the compiler. I don't see how "I can leave the types off my C# variables" has anything to do with that.

Re: Dynamic type systems are not inherently more open

#226

Post by meheleventyone » Sun, Jan 19, 2020, 8:59 PM UTC

pchiusano wrote: post #71

simias wrote: post #45

Earlier quoted context omitted.

I haven't given Unison a try so I won't dismiss it outright but to me having to explicitly propagate your change to your entire codebase before you can run anything doesn't suck at all, it's actually the killer feature of statically typed languages. I've written big applications in python, every time I made a significant architectural change (which might not even be huge code-wise, just far-reaching) I feel super unc…

I’d read through the link and see what you think, but TL;DR is that you can still propagate a change everywhere in Unison (and Unison tracks this for you), but even if you’ve partially propagated, you can run all the code that you’ve upgraded so far. So if a change has 500 transitive dependents and you upgrade 7 of them, you can run those 7 (and this might help you figure out that you want to do the change a bit diff…

Surely if the code was unrelated then you wouldn’t have to change it? It might be tangentially related to the change at hand but the fact it breaks means it must be given consideration and not just as a “geez I have to update all these cases” but also in terms of how the change impacts them.

I’m sympathetic to the idea that you want to solve the immediate problem first rather than have to move the entire codebase through several iterations. I’d be interested how well Unison handles that on a complex codebase in reality though.

Re: Dynamic type systems are not inherently more open

#227

Post by Barrin92 » Sun, Jan 19, 2020, 9:03 PM UTC

yawaramin wrote: post #224

Barrin92 wrote: post #202

Earlier quoted context omitted.

> And this post shows how you can do that in Haskell. the actual critique of the first post wasn't really that Haskell can't do it in a literal sense, but that ignoring or reasoning about unknowns diminishes the advantages of static typing. Sure, you can define an "unknown" type if you want and make your static language as permissive as possible, but then you lose the actual static guarantees, which is automating rea…

> ignoring or reasoning about unknowns diminishes the advantages of static typing. Ignoring the unknowns that are unnecessary to solve the problem at hand, is literally the essence of software abstraction. Why would you want to do more work than is necessary to solve a given problem? > you can define an "unknown" type if you want and make your static language as permissive as possible And 'unknown' type doesn't make…

>What you always gain from static typing–exposing the assumptions and invariants of your code as first-class parts of the code, making it easy for readers to understand at a glance what they are

This is essentially what I was getting it. To me the static typing seems to be almost more about naming things that it is about verifying the correctness of your program in the face of unknown or interesting behaviour.

And there is a very obvious cost to this because not all code is 'your code'. That's the problem with a coupling that is mentioned in the first part of the article but not really addressed. With typing, it is very easily possible for someone to create bad abstractions that you have no control over, you simply inherit them. It breaks with the principle of leaving interpretation to the receiver of data who encapsulates it.

And this is a very practical problem in real static code, because people create bad abstractions all the time, so the type system rather than just making valuable claims about what we know produces all sort of entanglements you have no control over.

Here is where the dynamic and static typing distinction crosses over into the OO debate. Alan Kay pointed out that the 'late-binding of all things' is one of the key principles of object oriented programming. Static typing interferes with this in very strong ways by allowing developers to impose meaning on your program way too early.

Re: Dynamic type systems are not inherently more open

#228

Post by roenxi » Sun, Jan 19, 2020, 9:05 PM UTC

yakshaving_jgt wrote: post #110

capableweb wrote: post #100

Earlier quoted context omitted.

Also, the following part isn't necessarily because of dynamic typing vs static > what types all the variables are, what expectations are attached to them, what mutation, if any, each method call performs But more about what the language offers. Clojure for example, goes beyond types with it's abstractions (like seq, that can be applied to strings, lists, maps and so on) and normally stays away from mutation, but when…

> Clojure for example, goes beyond types with it's abstractions (like seq, that can be applied to strings, lists, maps and so on) Goes beyond types? Statically-typed languages can have polymorphism.

Spec is at heart a data modelling system. So for example,

  (s/def ::integer integer?)

is very explicitly not a definition of an "integer" type. It is preparation to model some data x and check that the data will evaluate to true if someone uses the predicate (integer? x). However, this is obviously enough to implement a type system.

But you can also do some very loose things with spec that aren't done in a type system (I speak with a cheerful ignorance of type systems). Eg, I can spec a function so that one argument is smaller than the second. This allows my testing system to automatically generate the correct data to test my function.

So spec can used to implement a type system but also to implement things that aren't type systems.

Re: Dynamic type systems are not inherently more open

#229

Post by shrimp_emoji » Sun, Jan 19, 2020, 9:07 PM UTC

brabel wrote: post #166

hhas01 wrote: post #150

Earlier quoted context omitted.

Yep. Being able to work fast and dirty is a huge boon when testing ideas and figuring out the initial design, and it is deeply annoying that so many typed languages refuse to permit this. The faster you can write code, the faster you can throw it away again; and arriving at good code almost invariably requires† writing lots of bad code first. If writing bad code is made expensive (another example of Premature Optimiz…

If you think it helps to quickly write some code without types (I don't really agree with that in general, maybe in some specific cases), but you want to, when you're happy with the design, just add the types, there are many languages that support that! On the top of my head: * Dart (just don't give a type and the variable is dynamic) * Groovy (add @CompileStatic or @TypeChecked when you're ready) * Racket (start usi…

Look at this C++ code:

  std::vector> s;
  s.push_back(Pair("a", MyInt(1)));
  s.push_back(Pair("b", MyInt(2)));
  s.push_back(Pair("c", MyInt(3)));

Gross. I'm being punished.

Look at this Rust code:

  let mut s = Vec::new();
  s.push(Pair::new("a", 1));
  s.push(Pair::new("b", 2));
  s.push(Pair::new("c", 3));

Both are statically typed, but one uses inference. It practically feels like Python everywhere except where type declarations matter most to me -- function signatures:

  fn foo(x: f64, y: f64) -> Point {...}

In Python, those aren't very helpful.

  def foo(x, y): ...

:c

Re: Dynamic type systems are not inherently more open

#230

Post by sethev » Sun, Jan 19, 2020, 9:18 PM UTC

erik_seaberg wrote: post #222

sethev wrote: post #189

Earlier quoted context omitted.

I thought the article was good and addressed a real point of confusion, as evidenced by the two included comments (from Reddit and HN). You can consume arbitrary data using a program written in a statically typed or dynamically typed language. Whether it's decoupled from changes in the data depends on how the code is written and the data model, which have nothing to do with static vs dynamic typing. To me the stronge…

> the boundary between programs is dynamically typed Many interfaces have declared, enforced static types. I don't have to write any code to handle SELECT birthdate FROM employees WHERE id = ? returning "fish" because the database would never let it happen.

You know that but your compiler doesn't (generally speaking).