[didibus]

> On the other hand, this means that typed systems are in some sense strictly less expressive than their untyped counterparts.

This happens quite often. Take datastructures. It is often very useful to structure different types of data together in a common structure. Now in most cases, you don't know in advance which type will go where in the datastructure, as the data might only be known or derived at runtime.

In fact I'd say dynamic behavior is the major expressiveness loss. Granted, I'm not sure how runtime vs static type system relate to type theory. Anyone can educate?

[cel1ne]

> It is often very useful to structure different types of data together in a common structure.

"Very useful" often just means: coding a properly typed, easily-understandable solution takes longer than doing it untyped.

I argue that is the case only when using a plain-text editor. When you have a good IDE for a typed-language at hand that can refactor, complete, analyed and follow code on the press of a button, you lose this "advantage" of untyped languages.

[didibus]

How do you define expressiveness? To me, it means saying more with less. Applied to code it means doing more with less work. Which directly translates to productivity gains.

Now, what IDE and language are you referring too? The best one I've used was VisualStudio for C#. While I'd say typing wasn't adding too much overhead in it, its type system is also poor, and it's arguable that it may not really prevent much bugs. Now, it does help make C# faster.

[cel1ne]

IDEA with Kotlin or Java is fantastic.

[evincarofautumn]

It’s partly just coincidence that dynamically typed languages tend to have less expressive type systems. You could run any typechecker at runtime if you wanted. There’s no reason you couldn’t have a Python-like language where the “list” type dynamically keeps track of the types of its elements, function types keep track of the types of their inputs and outputs, and so on, to give you more precise & useful dynamic type errors. That would let you do some interesting things like creating a type from runtime data, such as a database schema.

It’s just that historically people have found it markedly more useful to have that information available statically, because it lets you prove things about your code that hold “for all” cases (universals), not just “for some” that are executed (existentials). And static information can be used for optimisations because of those guarantees—if you have proof, you don’t need a fallback.

[leshow]

Can you explain what you mean by comparing universal and existential quantification to dynamic languages? Existential quantification is often used in statically typed languages and can be valuable in some cases (no pun intended). In Rust, for instance, you can say fn f() -> impl Fn(u8) -> u8 or something similar. This is existential quantification, because you're saying that f returns a type that is some Fn(u8) -> u8. This can expressiveness can be powerful in a type system. I don't see how it relates to dynamic languages.

[evincarofautumn]

I’m not referring to existentially quantified types—which are definitely useful & interesting in statically typed languages. What I mean is that with static types you can prove universal properties of functions.

If you give me an unknown function f : ∀T. T → T in a statically typed language, then I know it always returns a value of the same type as its argument. With some assumptions (purity, parametricity, halting) I even know it must be the identity function.

Whereas doing what I’m suggesting in a dynamically typed language, running inference dynamically, I could only recover existential properties: that there are some types for which f returns a value of the same type as its input. So I could recover more and more information (in the form of an intersection type) by calling the function with different inputs:

f : int → int

f : (int → int) ∧ (string → string)

f : (int → int) ∧ (string → string) ∧ (Foo → Foo)

But I could never arrive at ∀T. T → T, because that’s essentially an infinite intersection.

ETA: actually I might not even be able to get this much information; I only know the output type for each input value, not each input type.

[leshow]

I see what you were getting at now, thanks.

[catnaroek]

You create a reference cell containing an empty list. Because the cell is mutable, it can't have a polymorphic type - it must have a monomorphic one. How do you determine at runtime the type of this cell, before the first time you mutate it?

[evincarofautumn]

What I’m suggesting is that you could literally just run HM or another typechecker at runtime. You’d give an empty list the type “list<T>” for a fresh type variable T; appending an integer would introduce the constraint T = int; appending a string would introduce T = string and raise a runtime error. (Or not—it’s up to the typechecker if it wants to degrade to “int|string” or something.)

[catnaroek]

At runtime, the original program (i.e., the syntax tree, or some other representation from which the syntax tree is recoverable) may well not exist anymore. If you don't have a syntax tree, you can't type-check anything.

Now, you may say “okay, the original program doesn't exist anymore, but my language implementation is a term rewriting engine, so I have a current program that I can submit to the type checker”. Alas, most type checkers, Hindley-Milner included, operate on self-contained program fragments (i.e., not containing unbound variables), so you can't just submit any arbitrary program fragment. And, if you didn't want to type-check your original program, how likely is it that you will want to type-check the entire syntactic representation of the current program state?

[fao_]

Who says you need a syntax tree? You just store a byte of metadata next to each variable with the type. There should be more than enough data from that to recover the parts that you can't store like that and do type inference on them.

[johncolanduoni]

Why is that required? There's nothing stopping you from only giving the list a precise type after an element has been added. This mirrors the way statically typed languages with inference handle the same situation (except they wait for evidence that it's being used as a list of Ts, instead of the actual act).

[catnaroek]

> Why is that required?

Say, because you want to use that reference cell in two different threads.

[evincarofautumn]

I think I see what you’re getting at. If I create an empty mutable list and send a reference to it to two different threads A and B, where A adds an integer to the list and B adds a string, then it’s nondeterministic which thread raises a type error.

And degrading the type to a union (int ∨ string) as I mentioned is still nondeterministic even though unions form a lattice—I can recover determinism when writing to the list in both A and B, but supposing A writes first, B writes second, and then A reads expecting only integers, it gets a type error because it hasn’t checked for the string case.

But I’d argue that 1. this is bad form and you want a type error somewhere and 2. you have this problem already with type-changing mutable references in a dynamically typed multithreaded language. (Say just “int” and “string” instead of “list of int” and “list of string”.)

[catnaroek]

I need a container type that can be empty, because I need the monomorphic type of the cell to be undecided until the reference has been handed out to the worker threads.

[johncolanduoni]

If your standard for a possible programming language that supports concurrency is that no data races are possible, then there's very few languages to be had.

[catnaroek]

This particular discussion wasn't about ruling out data races (although, of course, that is important too). It was about ruling out trying to read a list of strings from a reference cell containing a list of ints.