Live data from Hacker News

Dynamic type systems are not inherently more open

lexi-lambda.github.io

281–286 of 286 posts

Re: Dynamic type systems are not inherently more open

#281

Earlier quoted context omitted.

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 declar…

You mean this C++ code? std::vector > s; s.push_back({"a", 1}); s.push_back({"b", 2}); s.push_back({"c", 3}); I mean let's compare apples to apples here.

Damn, I forgot about uniform initialization. D:

That IS better than Rust since it migrates the type from n container members to just the 1 container. It doesn't seem possible to replicate that in Rust[0].

My Rust evangelism IS hurt by this. But its HP bar is big[1].

0: https://news.ycombinator.com/item?id=10891892

1: https://www.reddit.com/r/rust/comments/bya8k6/programming_wi...

Re: Dynamic type systems are not inherently more open

#282
post #204

Earlier quoted context omitted.

Right, and the type system is such a big help in refactoring - especially in small projects - that you don't have to be all that right in your first N cuts at the model. You can write code and find out where you're wrong, and fix it fast.

It’s even more help in larger projects :) The dividends of type-checher aid refactoring really start paying off once the project is above a a certain size/age.

Yeah, I think I was unclear. Given a need to refactor, it's a bigger help on a bigger refactor.

But a large refactor on a large project is still a pain. By the time you get there, you still want your model stable and/or flexible enough that you don't need to do that much.

On a small enough project, every refactor is easy enough that you can lean into it. Make a bunch of assumptions you're not confident about, setting up the types so you're sure you'll know what needs fixing when they're wrong. Then you test those assumptions as you write - and run - more code.

Re: Dynamic type systems are not inherently more open

#283
post #280
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…

After giving it enough time and rereading, I feel I have a better understanding. The crux IMO is here: > The above JavaScript code makes all the same assumptions our Haskell code does: it assumes event payloads are JSON objects with an event_type field, and it assumes signup payloads include data.user.name and data.user.email fields. What the post points out is that these exact same assumptions, and the same behaviou…

Now for the flip side. IMO the post also contains "enough rope" to hang static typing with. The picture that emerges is that programming in a statically typed language, as the author conceives it, consists of separate phases of "data modelling" (making assumptions about the external world, and at each module/function level about the inputs and outputs), and writing code. Often the former is the hard part to get clear, and this explains the phenomenon familiar to programmers in a statically typed language like Haskell, that once you get the types exactly right, the code basically writes itself: the types guide you towards the right code, like gravity.

But unanswered are questions like:

1. Should they be separate? In a dynamically typed language the two are blended, you write and run code (with representative inputs) to discover and refine your assumptions. You don't have to switch between two modes of thought. In a statically typed language, bugs in your assumptions will be pointed out by the compiler, and bugs in your logic will be pointed out by the program's execution.

2. Is it always worth being explicit about your assumptions? One can often get useful work done even with unclear, undefined, or even inconsistent assumptions.

3. Fine, the same set of assumptions can be encoded in both kinds of languages, but how different is the experience of arriving at the right assumptions?

Look at these quotes from the post, and think about the words "only", "just", "simply":

> static type systems only make already-present assumptions explicit

> We just have to be explicit about ignoring it.

> A static type system doesn’t require you eagerly write a schema for the whole universe, it simply requires you to be up front about the things you need.

Being explicit or "up front" in this way surely has a cost. At the same time, not being explicit also has a cost (of bugs). What the trade-off? (One does not always operate in environments where bugs have a high cost. For example, even code that does the right thing for 90% of users, but something catastrophic for 10% of them--like lose all their data--may be ok, depending on the importance of the "data" (previous scores in your game?), what expectations you've made clear, etc.)

In fact, too-enthusiastic data modeling can also lead to its own kinds of bugs:

> Suppose we’re consuming an API that returns user IDs, and suppose those IDs happen to be UUIDs. A straightforward interpretation of “parse, don’t validate” might suggest we represent user IDs in our Haskell API client using a UUID type [..] this representation is overstepping our bounds. [...] This is a case of improper data modeling, but the static type system is not at fault—it has simply been misused.

The claimed benefits are also all similar, and may not often be wanted:

> easy to discover the assumptions of the Haskell program just by looking at the type definitions [...] In the dynamically-typed program, we’d have to audit every code path

> If we want to ensure it [UserId field inside SignupPayload type] isn’t actually needed [..] we need only delete that record field; if the code typechecks, we can be confident...

> ensure application logic doesn’t accidentally assume too much

> the type system helped us here: it caught the fact that we’re assuming the payload is a JSON object, not some other JSON value, and it made us handle the non-object cases explicitly.

> The runtime representation of a UserId is really just a string, but the type system does not allow you to accidentally use it like it’s a string

> the parsing style of programming has helped us out, since if we didn’t “parse” the JSON value into an object by matching on the Object case explicitly, our code would not compile, and if we left off the fallthrough case, we’d get a warning about inexhaustive patterns.

Whether this is really a help is probably the big question. Incidentally, while I was rereading and thinking about this, came across a related paragraph in an unrelated article:

> requires covering 100% of the conditions, not just 99%. Edge cases must have applicable code, even when the programmer doesn’t yet know what the happy path should do. During early development, these edge cases can often be addressed by causing the program to crash, and then rigorous error handling can be added at a later point. This is a different workflow than in languages such as Ruby, where developers often try out code in a REPL and then move that to a prototype without considering error cases at all.

(From https://stackoverflow.blog/2020/01/20/what-is-rust-and-why-i... )

Ultimately, there's selection bias:

> programmers in statically-typed languages are perfectly happy to supply their assumptions up front

-- of course: programmers who are happy to supply their assumptions up front tend to be happier with statically-typed languages.

Re: Dynamic type systems are not inherently more open

#284
post #279

Earlier quoted context omitted.

> If dependent types would accept unsound proofs, the soundness of the entire type system would be compromised to the point of undefined behavior. This seems like too strong of a statement. Every language that allows for nontotal functions has a type system allowing for unsound proofs. This does not mean the type system is compromised to the point of undefined behavior. Dependent Haskell is explicitly going to be uns…

> If you lie to the type system you just blow up at runtime, e.g. with an exception. Same as in any other language. That depends on the runtime type system. If you can switch an int for a string (which is not hard in a dependent type system -- rely on the output of some silly arithmetic function that you only tested and omit a proof and use it in some function that indexes types by integers, and you just might cast a…

Well sure if you lie to your specs all bets are off. Buffer overflows, bounds checking, use after free (if you're in a non-GCed language), resource leakage, etc. You're always at the mercy of your runtime system as soon as you lie about your pre-runtime checks, no matter what system you use, types or otherwise.

That's different than UB in the type system itself, which if you lie to it at worst just becomes inconsistent, but although that sounds quite scary, it's not really a big deal if you're not using dependent types as a theorem prover and you know where the inconsistency stems from.

Now perhaps your contention is that dependently typed systems tend to have weaker runtime checking, which I still disagree with. You do have weaker runtime guarantees with Idris 1's native code generator and of Agda's code extractor, but this is not true of Idris 1 on JS or its other code generators, which inherit their hosts' runtime systems, or Idris 2's native code generator, which inherits Chez Scheme's runtime system.

RE computations and functions yeah I definitely overreached. I somehow completely forgot that Hoare Logic has the ability to have unrestricted first-order logic. I got too fixated on JML, where in retrospect the difficulties only come from the awkward way that Java tries to handle higher-order methods like reduce (that was my initial impetus, verification of parallel reduce). I totally forgot I've done the isAssociative property in Dafny before and there it's exactly as you say, it's a function that you then put on top of a method (Dafny's notion of "computations").

The Lamport quote is a good reminder not to poo-poo different formalisms, but I've had a great time with systems like Dafny. I don't think dependent types are the holy grail of verification. My contention in fact is that the gulf between dependent types and contracts is not as large you're making it out to be.

Dependent types break down if you have pervasive mutability, i.e. as in an imperative language, for which Hoare Logic is very well-suited for. You have to express the mutability at a type level that's also is transparent enough to the type system to make assertions which makes things very annoying. (And no I don't use mutability/imperative as dirty words, most of my day-to-day work is in imperative languages and that's just fine by me, a lot of algorithms flow more naturally as imperative ones).

But if you have a language where everything is immutable, dependent types are fantastically expressive. And as long as you don't use the type inhabitants at runtime, their "proofs" or lack thereof are also very flexible. Hell, you could even generate a runtime assertion from a dependent type if you wanted to and have the compiler automatically insert those in place! You could even do that generation in a user-defined library without compiler support if dependently typed languages supported typecasing and didn't impose parametric polymorphism in all cases (useful in a non-dependently typed language, less useful in a dependently typed one). They don't, but that's a different story (for all my excitement about dependently typed languages, there's so many other ergonomic hurdles to get over first, as is true of a lot of the current state of code-based verification tools).

Indeed, dependent types and contracts converge in many ways if you have pervasive immutability. The main difference is that dependent types are more integrated into the language and don't have as many contract-isms. An invariant required by a function becomes just another argument. A lemma is just another function. Those contract-isms are necessary in a mutable environment (it would be rather painful to try to drum up some sort of type-indexed loop monad to try to express the notion of a loop-invariant in a dependently typed language, especially if the loop accesses non-local resources), but are not so much in an immutable one.

Oh BTW, speaking of limitations of formalisms, I'm pretty sure you're right on Twitter that Hillel Wayne's hyper-property isn't actually truly a hyper-property and can be described with the temporal quantifiers TLA+ has. A better example (that I don't think can be expressed in TLA+) is something like "variable independence," the statement that for any behavior where a variable "a" takes on some trace, there is another behavior such that "a" has a different trace, but all other parts of the behavior are the same. That is you can delete "a" from your spec and nothing would look different, no behavior would ever change (this requires either quantifying over all predicates or manipulating behaviors directly). Another example would be something like "x 'usually' takes n steps" for some definition of usually (mode, median, average, anything that's not a strict upper bound). Even expressing "n steps" in TLA+ is kind of wonky, but do-able with an additional counter variable (although that makes TLC unable to check termination).

Oh and of course since you've linked your own TLA+ link, many many thanks for your TLA+ series. It was an invaluable source right alongside Lamport's own materials when I was learning TLA+ on my own.

Re: Dynamic type systems are not inherently more open

#285

Earlier quoted context omitted.

> Static type systems will typically require you to state the full type of o. This is not the case for languages with support for structural typing (as the article mentions in the appendix), and most modern statically typed languages have some degree of support for abstract interfaces of some sort which also support writing functions with only partially known information about the type. I think one of the core insigh…

Structural typing doesn’t save you unless you add other stuff to it. Example: var o = ...; // Value comes from somewhere, doesn’t matter where so long as it’s opaque if (p) ... = o.f else ... = o.g In dynamic typing, we only assert that o has f on the then, and only assert that o has g on the else. Structural typing or abstract base classes or whatever would only save you here if you were very careful about giving o…

Yes, for that situation you additionally want sum types.

Re: Dynamic type systems are not inherently more open

#286

Earlier quoted context omitted.

> Companies do have policies against using type inference (e.g., the use of var in C#). That's a language that historically has not had type inference. Any examples of companies mandating type annotations in historically type-inferred languages?

Yes! Any company that has adopted MyPy or TypeScript often have policies for this. One team I spoke to at Facebook said that any new code should have type annotations. I believe Dropbox had a nice blog post about new code should have type annotations too. It is hard to get these details from companies/teams (and be allowed to talk about it).

Typescript will infer the 'any' type by default in a lot of cases, that's the reason teams will mandate type annotations. It's really just not the same thing. These are bolt on type systems to dynamic languages where if you fail to put a type annotation you're actually losing information. That's not the case in Haskell, type inference causes no loss of precision for types.
Post reply on HN