2 ms·

Reading this back, I'd also suggest a comparison with Hindley-Milner type systems ( https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system https://en.

Reading this back, I'd also suggest a comparison with Hindley-Milner type systems ( https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_sy... ) These type systems are used by ML and its descendents (OCaml, Haskell, Rust, Reason, etc.) and are generally seen as a "sweet spot". They feature: - Types depending on types (AKA type constructors) - Values depending on types (e.g. type classes) - Type-generic values (AKA parametric polymorphism) - Higher-kinded types (AKA higher-order types, or generics at the type-level) - Inference of all types - Erasure of all types Things which Hindley-Milner can't do include: - Inference of values (AKA implicit arguments, as found in Scala and Idris) - Erasure of values - Types which depend on values (AKA dependent types) These things are important for this article, since it represents types as values (which the two given rules let us access from our type annotations). In particular, if we could infer (some) values, we could avoid having to specify arguments like in `List(Integer)`. Going "beyond" Hindley-Milner is a very active area of research. There's a nice talk about this at https://www.reddit.com/r/haskell/comments/390dyx/conor_mcbride_type_inference_needs_revolution/ https://www.reddit.com/r/haskell/comments/390dyx/conor_mcbri... (which i admit is a bit symbol-heavy); full disclosure, I was in the audience for that talk ;)

Groxx 8y ago
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 :) To circle all the way back around tho, from the intro to the article: >A while back, I discussed the problem of shadow language constructs. I gave examples of shadow constructs such as Standard ML modules, traditional imports etc. Here is another: reified generics. The article seems to be about trying to eliminate shadow types, e.g. meta-type info carried by the compiler but not otherwise visible. By turning generics into type-generator funcs. My question / confusion is around "it seems like you can't type-check that at compile-time without being either so explicit it's no longer generic, or with shadow types, so I don't see how this helps". Or indeed changes anything. Generics as type-generating funcs makes sense, it lets you choose erasure-or-not however you like. Perfectly on board[1]. But how do you type-check it at compile-time without "shadow types"? (if the answer is "read my comments", I'm happy to! I haven't gone through them super carefully yet.) [1]: well... in concept. I'm not sure how libraries would be able to use this in a standard way, seems like it'd lead to multiple competing "generics systems". But that's also useful sometimes. I like languages that let you do that kind of thing, though the ecosystem does not always benefit from it.
- chriswarbo 8y ago
  > 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.)

Groxx 8y ago

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 :) To circle all the way back around tho, from the intro to the article: >A while back, I discussed the problem of shadow language constructs. I gave examples of shadow constructs such as Standard ML modules, traditional imports etc. Here is another: reified generics. The article seems to be about trying to eliminate shadow types, e.g. meta-type info carried by the compiler but not otherwise visible. By turning generics into type-generator funcs. My question / confusion is around "it seems like you can't type-check that at compile-time without being either so explicit it's no longer generic, or with shadow types, so I don't see how this helps". Or indeed changes anything. Generics as type-generating funcs makes sense, it lets you choose erasure-or-not however you like. Perfectly on board[1]. But how do you type-check it at compile-time without "shadow types"? (if the answer is "read my comments", I'm happy to! I haven't gone through them super carefully yet.) [1]: well... in concept. I'm not sure how libraries would be able to use this in a standard way, seems like it'd lead to multiple competing "generics systems". But that's also useful sometimes. I like languages that let you do that kind of thing, though the ecosystem does not always benefit from it.

chriswarbo 8y ago
> 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.)