Live data from Hacker News

Dynamic type systems are not inherently more open

lexi-lambda.github.io

111–120 of 286 posts

Re: Dynamic type systems are not inherently more open

#111
post #3

Disclosure: dynamic typer here. The way I understand it, a part of the issue is about possibly deferring the time at which the type of data is known to the time at which the data is operated upon, since calling a numeric addition function on not-numbers, e.g. strings, is a type violation, no matter which programming language you are writing in. The question is where you want your parsing-or-validating to occur, since…

I actually really enjoy your views on dynamic typing. But, if we agree on this definition then is it not an admittance that "dynamic type systems" don't actually exist and instead we are simply talking about evaluation/validation being programatically specified by the programmer instead of embedded evaluation/validation by the compiler and/or runtime? And since it is being specified by the programmer, then we run int…

> "dynamic type systems" don't actually exist

One definition of a "dynamic type system" that I am aware of is that there is runtime-existent information about types of particular pieces of data - or, somewhat equivalently, that types are information associated with values, not variables. Therefore, one could imply that e.g. Java has a dynamic type system.

The way I understand the question you're asking is: if a language has an "eval" function that accepts arbitrary code as input, what prevents it from having static-type-system-class parsing and type safety guarantees as a part of its functioning? It essentially means that the compiler for a language must both be permanently present in memory (like for Javascript, or Lisp, or Smalltalk) and it must implement the static type checks for all code that it parses (like for Haskell).

I think that these two requirements are orthogonal to each other and therefore they don't really clash with each other. Either there will be languages which implement both of these paradigms at the same time, or there already are such languages, and I am not yet aware of their existence.

Re: Dynamic type systems are not inherently more open

#112
post #97

The author doesn’t really address the issue raised in the first (longer) quoted post. Given a set of reasonable requirements I think pretty much no one would claim a general-purpose language couldn’t satisfy them without too much trouble. In fact, that might be a fair definition of a general-purpose language. I’m fine with strong and expressive static type-checking, but you need to hold the main limitation in mind as…

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.

Re: Dynamic type systems are not inherently more open

#113
post #43

I think there's a perhaps irreconcilable disconnect between 2 camps here, but I also think that's ok and different people are allowed to like different things. My experience, having gone from dynamic typing to static typing and now pining for more expressive type features in my chosen language is that static typing changes where you have to spend the cognitive complexity budget. To my mind if I return to a piece of d…

Yes. Perhaps this is an indication that we actually need automated type annotation. E.g. you initially write/prototype your program in a dynamically typed form, then you click a "magic" button, and a tool converts your program into statically typed style.

Unless your type system is very weak -- and in effect, an untyped language can be considered to already be doing what you said only in a type system that has a single type -- this is generally impossible (halting problem and its extensions). So you have the choice of something that's not very useful or something that's impossible -- take your pick.

Type inference, as others have suggested, does not do what you want. If your program is well-typed according to a particular type system which you must have in mind while writing the program, they'll save you from writing explicit type annotations, but they cannot come up with "correct" type for a correct program that's not written for that particular type system.

Re: Dynamic type systems are not inherently more open

#114
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…

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…

Why is seq “beyond types”? Isn’t it like a Rust Iterator trait?

Re: Dynamic type systems are not inherently more open

#115
post #106
post #97

The author doesn’t really address the issue raised in the first (longer) quoted post. Given a set of reasonable requirements I think pretty much no one would claim a general-purpose language couldn’t satisfy them without too much trouble. In fact, that might be a fair definition of a general-purpose language. I’m fine with strong and expressive static type-checking, but you need to hold the main limitation in mind as…

Wouldn't that boil down to the communication between the distributed components? I think this author's solution to that is well detailed in his post "parse, don't validate".

Her* post.

Re: Dynamic type systems are not inherently more open

#116

I think there's a perhaps irreconcilable disconnect between 2 camps here, but I also think that's ok and different people are allowed to like different things. My experience, having gone from dynamic typing to static typing and now pining for more expressive type features in my chosen language is that static typing changes where you have to spend the cognitive complexity budget. To my mind if I return to a piece of d…

Your comment is spot on. But the opposite can also be true. I totally have the same issues you do at times by trying to understand types (which I feel type hinting, editors, and good variables names go a long way to help with). But I also find myself using a lot of cognitive load trying to get a correct type definition, etc (for the non simple tasks). Whether its trying to figure out how to get a certain object, because of the interfaces, factories, etc. Or trying to create a new object and trying to map things correctly. What if I just want to have a hash map full of varying object structures? (I am not saying its not possible, I am saying its a use of cognitive load)

Re: Dynamic type systems are not inherently more open

#117
post #97

The author doesn’t really address the issue raised in the first (longer) quoted post. Given a set of reasonable requirements I think pretty much no one would claim a general-purpose language couldn’t satisfy them without too much trouble. In fact, that might be a fair definition of a general-purpose language. I’m fine with strong and expressive static type-checking, but you need to hold the main limitation in mind as…

> I’m fine with strong and expressive static type-checking, but you need to hold the main limitation in mind as you use it in a distributed environment: the guarantees are static. They pertain only to your little binary and don’t say anything about the rest of the system.

To argue that a static type system is not valuable because it doesn't enforce constraints on other external systems it doesn't know about is a pretty wild case of moving the goalposts.

Re: Dynamic type systems are not inherently more open

#118

Earlier quoted context omitted.

You don't need row polymorphism to write a function which operates on a collection of key/value pairs and expects a specific key to exist at runtime. This works in Haskell, just as it does in Clojure.

Please write the Haskell type signature of such a function, as an example.

    f :: Map String String -> Map String String

Re: Dynamic type systems are not inherently more open

#119
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…

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…

What do you mean with going beyond types? Is it possible to define some unique compile time constraints on Clojure not related to the type system?

Re: Dynamic type systems are not inherently more open

#120

Dynamic type systems are inherently more open. This article really bends over in strange ways to say otherwise. Fact is: dynamic typing is all about making fewer claims in your code about what you expect about the world around you. With dynamic types, to load a property you might just have to say the property name and receiver. With static types, you usually also have to say the type of all other properties of the re…

Wrong. There are statically-typed languages with polymorphism.
Post reply on HN