3 ms·

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

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 9y ago
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 9y ago
  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_ 9y ago
    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 9y ago
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 9y ago
  > Why is that required? Say, because you want to use that reference cell in two different threads.
  - evincarofautumn 9y ago
    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 9y ago
      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 9y ago
        If your program doesn't have a race condition, then you're fine. And if it does, then the list being monomorphic is not going to help (try your scenario with a C++ vector or Java ArrayList).

evincarofautumn 9y ago

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 9y ago
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_ 9y ago
  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 9y ago

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 9y ago
> Why is that required? Say, because you want to use that reference cell in two different threads.
- evincarofautumn 9y ago
  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 9y ago
    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 9y ago
      If your program doesn't have a race condition, then you're fine. And if it does, then the list being monomorphic is not going to help (try your scenario with a C++ vector or Java ArrayList).