People seem to think about types completely differently from me ... yes, they do all that, but their MAIN use is: _finding stuff_ - find what is possible; find all places that need to change ...
"what is possible" meaning: what makes sense to do / is correct / what values to pass, what structure to fill out with what-structured values ... what I can do with what it returns ... - and yes, it occasionally checks stuff which is nice, but it's mostly based on the compiler being able to find the rules and then check them - it's still about insight - and he made a good point, that it's about writing down the "types" one thinks ... except even typed languages usually do not allow to write quite what one would want..
I don't understand the difference between type inference, which he dismisses, and the gradual typing which he advocates. His examples look like they involve inference: given some type declarations in part of the code, reason about those types where they are used in the rest of the code.
+birthdayforfrances They are analogous to each other. He didn't dismiss type inference, he said that is not possible to have it in a untyped language. If you are using typed racket then you can have type inference since know you have a type checker but if you then use regular racket in another module you loose that.
+birthdayforfrances Gradual typing only checks what you've actually told the compiler about types, while leaving the rest dynamically typed. Type inference tries to infer types for all expressions, even those you haven't annotated. He's also talking mostly in the context of dynamic languages and putting types on them. It's practically impossible to infer the types for a type system that a language wasn't designed for, especially in a practical way that handles failure to infer.
+birthdayforfrances the problem with type inference that he's talking about (IIUC) is that an error in one part of the code may manifest itself far away, and there is no way to make "good" error messages for these type errors. There is a distinction between local type inference and global type inference; local type inference means that types are inferred throughout a single function body. This helps because type mismatches happen much more closely together. Gradual typing is just optional types + contracts to ensure incorrect data is passed in to typed code. This isn't really related to type inference.
The idea of inference that he dismisses is "Infer all types of an untyped program" because (if my understanding of his criticism is correct), the inferred (composite) types end up being very hard to reason about in error messages. I don't think he dismisses the concept of inference in general as that is quite essential to checking. The racket approach to gradual typing appears to be that contracts are generated for where you use typed code from untyped code - i. e. if you don't add types to your code you have pay with runtime for being guaranteed that the types aren't violated.
Type inference usually means that where a variable is defined, the type annotation can be absent but the static type still present. But in his examples (I don't use Racket at all, so am just postulating), all static types are created only with explicit annotation. If you do not add this annotation, then there is no static typing. Whereas, in a language with type inference, the static typing would still exist even without the annotation. I can understand his objection to type inference, even if I do not entirely agree with it. I suspect part of his objection is simply due to the complexity of implementing it, especially in a dynamic language. Type inference makes code a lot more elegant, and is easier for the developer who writes code, but does add some cognitive overhead to another developer who reads it. C++ introduced type inference in 2011 (with the "auto" keyword), but some practitioners like Scott Myers still provide recommended guidelines for when to not use it, because the explicit type annotation is clearer to the reader. A lot of it is about style.
+kumoyuki Depends on the language. I my experience, 500 LOC in a single file written in Clojure is a lot (enough to make you think about splitting it), but with javascript (or especially with Java!) you're just getting started. Racket is probably quite close to Clojure in this sense.
Yes, I program in a lot of different languages, from the horrors of the C family, through Smalltalk, the Lisp family, and the Hindley-Milner languages. 500KLOC is peanuts in all worlds - at least assuming a relatively constant factor for converting LOC to actual concepts which are being manipulated in the program. In fairness, I write very different programs in HOT languages than I do in glorified assembly languages. The concepts in my HOT code are much more abstract and so, in a sense, feel more complicated. But maintainance difficulty for the code base of HOT programs seems to scale just about at the same rate as for those of more primitive ones. So I don't see an inherent difference in the number of things I have to track mentally.
500,000 lines of lisp code is like 5 million lines of c++/java code. There is a fair 10:1 reduction in code size when using a dynamic vs static language combined with using a functional vs imperative language.
![[ ออกกอง ] วัยหนุ่ม 2544 โลกหลังลูกกรง..ทัวร์กองถ่ายหนังใน "คุกของจริง" | JUSTดูIT.](http://i.ytimg.com/vi/vB--aOkZCpw/mqdefault.jpg)
Finally, a talk on types I can actually get behind!
People seem to think about types completely differently from me ... yes, they do all that, but their MAIN use is: _finding stuff_
- find what is possible; find all places that need to change ...
"what is possible" meaning: what makes sense to do / is correct / what values to pass, what structure to fill out with what-structured values ... what I can do with what it returns ...
- and yes, it occasionally checks stuff which is nice, but it's mostly based on the compiler being able to find the rules and then check them
- it's still about insight
- and he made a good point, that it's about writing down the "types" one thinks ... except even typed languages usually do not allow to write quite what one would want..
35:17 Circle and Square should be exchanged.
I don't understand the difference between type inference, which he dismisses, and the gradual typing which he advocates. His examples look like they involve inference: given some type declarations in part of the code, reason about those types where they are used in the rest of the code.
+birthdayforfrances They are analogous to each other. He didn't dismiss type inference, he said that is not possible to have it in a untyped language. If you are using typed racket then you can have type inference since know you have a type checker but if you then use regular racket in another module you loose that.
+birthdayforfrances Gradual typing only checks what you've actually told the compiler about types, while leaving the rest dynamically typed. Type inference tries to infer types for all expressions, even those you haven't annotated. He's also talking mostly in the context of dynamic languages and putting types on them. It's practically impossible to infer the types for a type system that a language wasn't designed for, especially in a practical way that handles failure to infer.
+birthdayforfrances the problem with type inference that he's talking
about (IIUC) is that an error in one part of the code may manifest
itself far away, and there is no way to make "good" error messages for
these type errors.
There is a distinction between local type inference and global type inference; local type inference means that types are inferred throughout a single function body. This helps because type mismatches happen much more closely together.
Gradual typing is just optional types + contracts to ensure incorrect data is passed in to typed code. This isn't really related to type inference.
The idea of inference that he dismisses is "Infer all types of an untyped program" because (if my understanding of his criticism is correct), the inferred (composite) types end up being very hard to reason about in error messages. I don't think he dismisses the concept of inference in general as that is quite essential to checking. The racket approach to gradual typing appears to be that contracts are generated for where you use typed code from untyped code - i. e. if you don't add types to your code you have pay with runtime for being guaranteed that the types aren't violated.
Type inference usually means that where a variable is defined, the type annotation can be absent but the static type still present. But in his examples (I don't use Racket at all, so am just postulating), all static types are created only with explicit annotation. If you do not add this annotation, then there is no static typing. Whereas, in a language with type inference, the static typing would still exist even without the annotation.
I can understand his objection to type inference, even if I do not entirely agree with it. I suspect part of his objection is simply due to the complexity of implementing it, especially in a dynamic language. Type inference makes code a lot more elegant, and is easier for the developer who writes code, but does add some cognitive overhead to another developer who reads it.
C++ introduced type inference in 2011 (with the "auto" keyword), but some practitioners like Scott Myers still provide recommended guidelines for when to not use it, because the explicit type annotation is clearer to the reader. A lot of it is about style.
Awesome. Bookmarked.
500KLOC is peanuts
+kumoyuki Depends on the language. I my experience, 500 LOC in a single file written in Clojure is a lot (enough to make you think about splitting it), but with javascript (or especially with Java!) you're just getting started. Racket is probably quite close to Clojure in this sense.
Yes, I program in a lot of different languages, from the horrors of the C family, through Smalltalk, the Lisp family, and the Hindley-Milner languages. 500KLOC is peanuts in all worlds - at least assuming a relatively constant factor for converting LOC to actual concepts which are being manipulated in the program.
In fairness, I write very different programs in HOT languages than I do in glorified assembly languages. The concepts in my HOT code are much more abstract and so, in a sense, feel more complicated. But maintainance difficulty for the code base of HOT programs seems to scale just about at the same rate as for those of more primitive ones. So I don't see an inherent difference in the number of things I have to track mentally.
500,000 lines of lisp code is like 5 million lines of c++/java code. There is a fair 10:1 reduction in code size when using a dynamic vs static language combined with using a functional vs imperative language.