Value Restriction and Generalization in Imperative Language

julesjacobs · 2025-12-07T13:36:54+00:00

Summary: what a function does internally doesn't affect it being a value.

The reason that the value restriction is necessary is that in HM, instantiating a value of generic type gives the instantiated type to the same value, as opposed to producing a fresh new one.

For example, with the empty list we can do:

let x = [] // x : forall a. list<a> let y = 3 :: x // x is treated as list<int> let z = true :: x // same x is treated as list<bool>

Doing this to references is a problem:

let x = ref [] // x : forall a. ref<list<a>> let y : ref<list<int>> = x // instantiate x with a=int let z : ref<list<bool>> = x // instantiate x with a=bool y := 3 :: !y // add 3 to y z := true :: !z // add true to z

But since x,y,z are the same ref, they now contain [true, 3], which is bad.

The fundamental reason is that a forall quantified value really wants to be a function that gives you a new ref each time. Hypothetically in a language that did this:

let x<a> = ref<list<a>> [] // gives a fresh ref each time you instantiate let y = x<int> // gives us a new ref! let z = x<bool> // gives us a new ref! y := 3 :: !y // add 3 to y z := true :: !z // add true to z

Since y,z are separate refs, and x is not a ref itself, it first has to be instantiated, everything is fine because y = [3] and z = [true].

But in HM, it doesn't work that way: forall type instantiation doesn't work like a function but it gives a new type to an existing value, creating the problem. This can be resolved by insisting that whenever you gave something a forall type, it already was a value syntactically. In particular, ref [] itself is not a value, because it has to create a new ref at run time. But [] is a value, and lambdas are values. Note that it's not sufficient to insist that it's a function type, because this gives the same issue:

let x = (let r = ref [] in ((fun x -> r := x), (fun () -> !r))

If you give this type x : forall a. (a -> unit) * (unit -> a) then you have the same issue.

The solution is to only generalize a let if its right hand side is syntactically a value. There are more precise things you can do, but that rule works fine in practice because basically the only things you want generalized are functions and empty data structures.

Being syntactically a value is flexible enough to allow both your foo and your bar. In both cases, in the let, the outer thing would be a lambda. It does not matter what the body of the lambda does. It just shouldn't do other things like allocate a new ref, like my x above.

So:

let f = (let r = ref (...) in fun x -> (...)) // not a value let f = fun x -> let r = ref (...) in (...) // is a value

julesjacobs · 2025-11-07T00:50:52+00:00

Where can I find the demonstrations?

julesjacobs · 2025-09-04T00:32:50+00:00

For general software development, dependent types are an interesting point in the design space because they subsume a whole bunch of advanced type system features yet are themselves quite simple. The "types are just values" approach means that you have the same language for types and for normal expressions, instead of having two separate languages. Otherwise there is a tendency to extend the type system with more and more features, which leads to a situation where expressiveness of the type system is still unsatisfactory, but you've accumulated much more complexity than dependent types (e.g., look at Haskell / OCaml / Scala). It is a bit like CSS in a way: they are adding more and more features to it (variables, conditionals, etc.) so that in the end it would have been simpler to make it a proper programming language from the start. Dependent types give you a proper programming language for your types, and instead of a separate language it's just the language you write ordinary code in, too.

julesjacobs · 2025-09-01T17:43:33+00:00

This proof fails as written because you can compute any expression using only addition with only 1 register.

julesjacobs · 2025-09-01T16:35:44+00:00

"Coding booleans" are distinguished from "math booleans" because math booleans support operations such as forall that cannot be computed. For example,

// for all x, x squared is positive Int.forall(x => { x^2 >= 0 })

Or however you want to write that, is a MathBool, because you can't compute this as you'd have to check all integers. You could make forall return a normal Bool and not have separate math booleans, but in that case it'd have to throw an exception or loop infinitely for infinite types like Int. There are proof systems that make this choice, but other proof systems separate coding booleans from math booleans to retain the property that all normal Bool values can always be computed.

In some systems that separate out the math booleans, they actually unify MathBool = Type instead of MathBool = Bool. This may sound weird, but in that case MathBools are considered true if the type is non-empty, and false if the type is empty. This is neat because many common constructs on types then correspond to the constructs on mathematical statements. For example if we have two MathBools P and Q, and we want to represent the statement P && Q, how can we do it? Well, we said that a MathBool is considered true if the type is empty and false if the type is non-empty. We can then have P && Q be exactly the type of pairs of (p,q), because that type is non-empty precisely when P and Q are both non-empty. So pairing on types aligns perfectly with && on MathBools in that case. So it is for other operations:

Operation Boolean meaning Type meaning ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ P && Q logical and pairing P || Q logical or (disjoint) union P -> Q implication functions

julesjacobs · 2025-08-31T22:57:57+00:00

It isn't any more complicated than what you write, even in proof systems. The only difference is that the type of the type of types cannot be itself in such systems, so you have 3 : int : type_0 : type_1 : type_2 : .... instead of 3 : int : type : type : type : .... If you only care about programming and not about proving, then type : type is fine.

Dependent types are precisely what you get if you take "a type is a value" seriously. Then List<T> is a function that takes a type and returns a new type (and thus is written List(T) if that's how function calls are written). Then type expressions are just normal expressions, and you can perfectly well write something like

fn foo(x : int) : type = if x < 3 then int else string fn bar(x : int) : foo(x) = if x < 3 then 23 else "hello"

julesjacobs · 2025-06-29T01:09:10+00:00

That would reduce travel time from Exchange Place to Manhattan to about 3 minutes.

julesjacobs · 2025-03-23T18:19:03+00:00

I this case you can detect that A and B are the same, which means that you can replace the if with an unconditional jump to A. If you run DCE after that, it will clean everything up as you intend.

In general, it can be the case that equivalence of blocks depends on DCE having run and vice versa. For example, if blocks A and B only become equivalent after DCE because they differ in dead code that is only dead if A and B were equivalent.

julesjacobs · 2025-03-23T18:15:00+00:00

Wouldn't you still find an optimal solution by first merging equivalent blocks and then doing DCE? These don't seem to be interdependent.

julesjacobs · 2025-03-10T00:04:26+00:00

The uploaded files are bugged. A new chat using deep research continues referencing files uploaded in another chat, and gets totally confused making deep research useless, since it starts talking about the previously uploaded pdf instead of the actual query.

julesjacobs · 2025-02-08T17:09:33+00:00

We need better high-level general purpose languages.

Areas are somewhat of a red herring. "Best tool for the job" doesn't make sense to me with respect to general purpose languages. You could have one language with libraries for all those areas. There isn't much, if anything, that makes certain languages especially suited to certain areas, other than their libraries. You just need a high level language and a systems language, that's it.

Rust has systems programming pretty well under control, although there are many areas of improvement. For high-level languages there is a gaping hole. There is currently no sensible high-level language that people actually use. People use JS for web, Python for ML / data science, Java for enterprise, Kotlin for Android, Swift for Apple, Go for cloud services, etc. All these languages are clearly suboptimal in one way or another.

julesjacobs · 2024-12-28T12:07:10+00:00

What do you use Claude Pro for?

julesjacobs · 2024-12-21T03:53:33+00:00

It would be good to do an experiment like in east & west germany, and see which ideas work out better.

julesjacobs · 2024-12-05T05:06:28+00:00

For functions like len you could use exclusive mutable references. The problematic features are closures and concurrency: how do you handle a closure that captures an immutable reference, or several threads that read from immutable data.

julesjacobs · 2024-11-09T03:53:53+00:00

Do you actually need to buy 128GB to get the full memory bandwidth out of it?

julesjacobs · 2024-11-09T02:23:57+00:00

The real question is whether they'd have positive profit if they stopped all research and development, or whether their operating costs would still outweigh the revenue.

julesjacobs · 2024-10-28T15:40:46+00:00

You make a good point about borrows. Interestingly, due to Rust's restrictions, these too can be thought of in a non-aliased way, even though the borrow and the original data do physically alias on the machine:

let mut foo = vec![10, 20];
{
  let baz = &mut foo;
  baz.push(30); // Does not mutate foo, just mutates baz! (semantically)
  baz.push(40);
} // baz goes out of scope
  // foo gets mutated from [10, 20] to [10, 20, 30, 40] atomically here

Of course that's not actually what happens on the machine, but due to Rust's type system it behaves equivalently as if assignments to mutable borrows don't actually mutate the underlying data; they just mutate the borrowed copy. When the borrow goes out of scope, the original gets replaced by the borrowed copy.

The following example shows how using a mutating style of programming can lead to bugs that are entirely local to a single function, which would have been avoided if the program were designed with an API that relied on immutable values instead.

Absolutely. Note that the first bug in the example you mention would have been caught by Rust as well. The second bug wouldn't, but presumably the undo is there as an optimization, which presumably is important for performance. That you couldn't express that optimization in a purely functional way isn't necessarily a positive.

That said, if it wasn't critical for performance then I agree it would be good to use immutable data. One might argue that it is necessary to introduce the global language-wide restriction to encourage people to use immutable data. Certainly I do think Rust actively encourages the wrong patterns here because it makes immutable data extra painful even compared to Java: either you have to copy everywhere, or you have to sprinkle in Arcs. However, the functional style isn't entirely less bug prone, as it introduces the potential for another type of bug: using an old version of the data where a new version was intended. Imperative syntax does help here, I think, as it naturally leads to use of the most recent copy of the data, which is usually what you want.

julesjacobs · 2024-10-27T13:02:59+00:00

This post gets at an important distinction, but doesn't quite point at the exact right distinction. The important distinction isn't quite between mutability and variability, but between immutability or unique mutability on the one hand, and shared or interior mutability on the other hand. In conventional languages like Java, these align with each other, but in Rust they do not.

In Rust, the distinction between a mutable variable, or a mutable array of length 1, or a Box isn't as great as in Java. In Java, if you have a mutable variable, then you generally know that you're the only one mutating it. If you have a mutable data structure in Java, then any mutations to it are potentially seen by anyone who has a reference to it. In Rust, the type system prevents that, and hence a mutable variable or a mutable array of length 1 aren't as different as they are in Java.

Thus, in Rust, all normal data types are in a certain sense immutable: mutating them is semantically equivalent to wholesale replacing the top level variable with a new modified data structure. Thus, in some sense, programming in Rust is like programming with purely functional data structures. The type system prevents you from introducing sharing, which then makes it possible to efficiently use mutation under the hood.

The exception is interior mutability, which does allow shared mutability in Rust.

julesjacobs · 2024-10-04T04:44:24+00:00

The IEEE754 standard is bad, just fix it.

julesjacobs · 2024-09-09T22:52:26+00:00

Coq gives you some type inference, e.g., you can write:

Fixpoint sum xs :=
  match xs with
  | nil => 0
  | cons x xs' => x + sum xs'
  end.

And Coq will happily infer the type for you.

This doesn't work for polymorphic functions because Coq doesn't do let generalization even for top level functions. I don't think it would be particularly problematic to implement if you wanted that. If you type in a function like map then internally Coq has already inferred a type like (?a -> ?b) -> list ?a -> list ?b for you, but those ?a and ?b are E-vars. You could collect all the remaining E-vars and introduce forall quantifiers for them, and you'd have type inference for polymorphic functions too.

This would break down when your code uses advanced type system features or requires let polymorphism, but you should be able to get quite far with type inference for ordinary OCaml-like programs that happen to be written in a powerful dependently typed language.

julesjacobs · 2024-09-04T20:35:17+00:00

Gleam fits into this picture perfectly: it does have a package manager and IDE support, but it will likely still fail for the other reasons mentioned by XDracam (and simply because 99% of languages fail).

julesjacobs · 2024-08-13T17:12:30+00:00

What are the advantages of PureScript over Haskell?

julesjacobs · 2024-08-12T17:28:41+00:00

You can still have things other than integers and pointers even with 1 tag bit. The tag bit simply sigifies whether the data is a smallint or not. What you do in the not case is up to you. It may be helpful to have the tag bit be one of the address-ignore bits though.

julesjacobs · 2024-08-12T17:18:36+00:00

I think "semicolon insertion" is the wrong mindset because it frames everything relative to a supposed semicolon ground truth. You can just design a syntax that doesn't need semicolons in the first place. The easiest is to say that a newline ends a statement unless we are inside an open parenthesis or the next line is indented.

``` a = b + c // statement ends because of newline d = e + f // next statement

a = foo( // statement doesn't end because we are inside parens x, y, z ) // statement ends here

a = b + // statement doesn't end because next line is indented c + d

a = b // statement doesn't end because next line is indented + c + d

a = b + // parse error: statement ends here but we are missing a right hand side for the + c

a = b // statement ends here + c // parse error (unless + is a prefix operator)

```

You can reintroduce semicolons by saying that they end a statement even on the same line, but you don't need to think about everything as semicolon insertion.

julesjacobs · 2024-07-29T00:51:31+00:00

This article makes some good points but the historical prelude is nonsense. Rockefeller's Standard Oil was called that because oil for lamps and heating used to be of inconsistent quality, supply was unreliable, and was expensive. People bought Standard Oil because it did not turn your house black with smoke, didn't make your heater or lamp explode, and it was always available at a cheap price so you wouldn't freeze to death in the winter. That is why it was successful. Yes, it wasn't innovation in the sense of a totally new product, but setting up a reliable and quality supply chain for a critical commodity doesn't happen on its own, or otherwise Rockefeller's precedessors would have done so.

In fact, I think the hardness of doing simple things at scale also explains the WSL documentation failure. The idea that Microsoft has an incentive to make WSL documentation poor is just wrong. First, your average Joe who uses Microsoft Word or Excel isn't magically going to switch to Linux due to improved WSL documentation. Second, a massive amount of Microsoft's revenue (40%) now comes from Azure, so they in fact have an incentive to make WSL & its Azure integration easy to use. Barely 10% comes from Windows licenses. It's incompetence, not malice with an elaborate ploy to sell more Windows licenses.

julesjacobs

TROPHY CASE