> Thanks for all the info! I definitely do want to learn more about this kind of thing, it's always interesting and I'm always glad for more links :) No proble

> Thanks for all the info! I definitely do want to learn more about this kind of thing, it's always interesting and I'm always glad for more links :) No problem. Most of my blog posts start out as rambling HN comments ;) > how do you type-check it at compile-time without "shadow types"? From my understanding of the article, the 2 rules allow type checkers to refer to the value names. To me, the key parts of the (typed) example are these lines: public var List = (function(T : Class) { ... public datum : T; ... public add:(e : T) : T { ... In the expression (type annotation) `T : Class`, we're introducing a function argument called `T`. `T` refers to a value, which we can tell because it's on the left-hand-side of the type annotation (`Class` is on the right-hand-side, so we know `Class` is a type). In the other two lines, `T` is being used as a type (again, since it's on the right-hand-side of a type annotation). This is what the first "rule" lets us do. As far as I can tell, this (along with the second "rule", which lets us refer to method names in our types) avoids the need for "shadow types" (or a "shadow language" for types), since we only introduce/define/pass-around things using the normal value-level machinery (functions, methods, classes, etc.), and our type annotations simply refer to those value-level names (we don't re-implement functions, methods, classes, etc. for types). My concern is that "rule 2" lets us write things like: function pickAType(T1 : Class, T2 : Class) : Class { if (canProve(collatzConjecture)) { return T1; else { return T2; } } var x : pickAType(Int, String) = 42; This is well-typed if and only if the Collatz conjecture is provable (e.g. by enumerating all proofs in some formal logic and checking whether any is a proof or disproof of collatzConjecture). If it's provable, then `pickAType(Int, String)` reduces to `Int`, which matches the type of `42`. If it's not provable then `pickAType(Int, String)` reduces to `String`, which doesn't match the type of `42`. This is just an example: we can replace "prove Collatz conjecture" with any arbitrarily-difficult calculation. The point is that checking these types requires running the function which, in this case, requires the type checker to understand `if/then/else`, functions like `canProve` which don't fit the constraints of "rule 2" (that inputs and output should be `Class`); presumably `canProve` will use things like recursion, and `collatzConjecture` will be some sort of datastructure, which a type checker would also need to understand. In short, we'd need an awful lot more rules than just the 2 in the article. The straightforward way to do this is to just have our type checker just invoke the normal language interpreter, but that raises more issues. For example, side-effects: what if `pickAType` chooses its output based on, say, reading a random number from the OS kernel? It seems unwise to allow side-effects when type-checking (except maybe for "type providers" https://docs.microsoft.com/en-us/dotnet/fsharp/tutorials/type-providers https://docs.microsoft.com/en-us/dotnet/fsharp/tutorials/typ... ). However, if we're running arbitrary value-level code as part of the type-checking process (e.g. by invoking the normal interpreter), that would require the value-level language to also be free of side-effects (or else we would need an alternative interpreter, which raises the "shadow language" problem again). In particular, object oriented systems, especially those like Smalltalk, Self and the author's Newspeak, model function calls, property lookup, value construction, method calls, etc. as 'sending messages between objects', which is an I/O effect that can have all sorts of repercussions for the meaning of other code. For example, imagine the method call `True become: False` ( https://gbracha.blogspot.com/2009/07/miracle-of-become.html https://gbracha.blogspot.com/2009/07/miracle-of-become.html ; or in Newspeak, where booleans are immutable "value objects", some equivalent behaviour-changing call). Even in a system with no I/O, I think this would make types non-compositional, i.e. if the expression `f` type-checks to type `A -> B` and `x` type-checks to type `A`, the expression `f(x)` might not type-check, and even if it does it might not have type `B`, since the code run while type-checking one sub-expression may alter the behaviour of code run while type-checking the other. Note that these aren't insurmountable problems: we could approach it like most other things in dynamic languages and say "yes it can be broken by doing that; so don't do that". Alternatively, perhaps more in keeping with Bracha's ideas of pluggable type systems, we might be OK with type systems that are limited (e.g. unable to reduce `pickAType(Int, String)` to either `Int` or `String`), or uncomputable (if we do run `pickAType`), or even containing "shadow" interpreters which may, for example, over- or under-approximate types (e.g. allowing `42` since it might have type `pickAType(Int, String)`, or disallowing it because it might not), or which implement some alternative evaluation method or effect system (e.g. calling out to SMT solvers or proof assistants, mocking I/O calls, etc.). If they're pluggable, then we're free to ignore those which aren't appropriate for our project (based on how much confidence we want in the result, whether we'll be doing shenanigans like `pickAType`, etc.)