- Is there any special reason why Bob decides to phrase the runtime typechecking as is_num and is_fun judgments rather than phrasing it closer to a typing judgment?
[SCW: I think it bothers Bob that this is called runtime type checking in the first place. Operationally, we're just checking tags on data. Furthermore, the tag checking is shallow---it doesn't look deeply at the structure of its argument like a typing judgment might.]
- In DPCF, we only have num, fun, nil and cons and we already need to define more rules for run-time type checking. If there are more types, will the increasing number of rules be a problem?
[SCW: Dynamic languages either stick with a relatively small set of types (i.e. numbers, characters, strings/symbols, functions, nil, pairs, and thats it) or include a mechanism for adding new user defined types defined in terms of this small set, such as Haskell's "newtype" mechanism.]
- In Section 22.3, I feel that the disadvantages pointed out outweigh the advantages pointed out regarding dynamic typing. In such a case, where and how does dymanic typing stand wrt static typing? And also, is it not a good thing to catch mistakes as early as possible?
[SCW: Bob has made up his mind here. You are not going to get a thorough discussion about the advantages of dynamic typing from him. Or from me, for that matter.]
- I am not clear of the critique of dynamic typing given by Bob. Does he mean that the dynamic typing needs redundant check which should be avoided when possible? However, there are some dynamic typing languages which have been widely used. Moreover, static language have some features for dynamic typing, right?
[SCW: These are all good points. Static languages are more expressive because they can eliminate runtime checks (which are required for safe execution of dynamic languages). Furthermore, dynamic languages can be embedded in static ones: see Haskell's Data.Dynamic library, for example. However, there is a "paradox" that some dynamic languages, like Javascript and Python, are currently very popular. We should discuss this paradox in class.]
-
What's the reason for the check that there are no free variables in our expression? Since we're working in a dynamic language that allows error states, wouldn't it be fine to check this at runtime as well? This seems kind of inconsistent to me.
[SCW: There is such a thing as dynamic scoping, where variables are resolved at runtime. This often leads to confusing semantics for higher-order functions. For example, what result should this code return:
let x = 2 in let f = \y -> x in let x = 3 inf ()
With static scoping, we get 2, and with dynamic scoping we get 3. Experience has shown that dynamic scoping is hard for users to reason about --- so elisp is the only language that I know of that still support it. (Well, Haskell can encode a form of it via type classes, but in that case it is controlled by the type system.) All other dynamic languages stick with static scoping.
Perhaps it would also be possible to report errors from static scoping at runtime, but there would be no benefit for it. All you would be doing is delaying errors.]
-
To what degree are the performance problems pointed out in 22.3 solvable by optimization/static analysis?
[SCW: Many dynamic languages do use static analysis for optimization, in order to remove dynamic checks. The difficulty lies in making these optimizations interprocedural---in Haskell/ML function types allow this information to flow naturally across function calls. But this can be a challenge to static analysis.]
-
Not that I like dynamic typing, but it feels like the criticism of dynamic typing in the book feels rather weak. I mean, yes, DPCF can't express the invariants necessary to avoid some of the runtime overheads, but it is not hard to imagine an extended version of the language that does. There is even work on adding type-system-like behavior as layer above dynamic languages (e.g. http://learnyousomeerlang.com/dialyzer). I guess, my question is why we focus so much on why DPCF is bad instead of why dynamic typing in general is bad (programmer sanity?).
[SCW: Good question. Programmer sanity is harder to gather evidence for than performance. On one hand you have to run user studies, on the other, you only need to time your compiler.]
-
The book says that the safety theorem holds for DPCF, and “every piece of abstract in DPCF is well-formed”. I don’t understand the reason of defining safety theorem in this way. Wouldn’t that make the safety theorem kind of weak? Because now it seems any language would be safe as long as all the runtime errors are well specified in the dynamics.
[SCW: That is exactly the point. The safety theorem is weak! What it means is that if someone comes to you and tells you that their language is safe, you have to look closely at their semantics to be able to gauge the import of that statement. (Regardless though, safe is always better than unsafe. Safety means that you have correctly identified all possible runtime errors.)]
-
Bob claims that DCPF has only one type, albeit multiple classes of values? What is this type? For the untyped lambda calculus, the terms had type D where D is a solution to the type equation t = t -> t. But now we have numbers in DCPF, and we can extend it with other base types such as bool, so what exactly is the type of DCPF? Is it t = (t -> t) + nat?
[SCW: Yes. We just add new alternatives to D as we add more classes of values.]
-
Isn't labeling a value just giving it a run-time type? Why would one give a value a type at run-time and not a compile time? What's the advantage?
[SCW: Bob doesn't go into the merits of dynamic typing, only the disadvantages.]
-
If DCPF was to be extended to have a rich type system like OCaml or Haskell, how would we tag and define dynamics for an arbitrary type ?
[SCW: See Haskell's Data.Dynamic, which goes the other way. In general, it requires compiler support.]
-
In what sense is the safety theorem of DCPF an advantage of dynamic over static typing? It seems to me that you'd want to rule out ill-typed programs immediately, even if they are well-defined according tho the abstract syntax. In general, why dynamically typed languages? Surely statically typed languages are much safer to use no?
[SCW: There are programs that are ill-typed according to static typing, but do not have dynamic errors.]
-
In the chapter of Variations and Extensions, Bob suggested that one could give s[] and z different classes, and the semantics of ifz becomes such that it only checks if the input is of class z, or the outer most structure of the input is s[] of something. What is the advantage of this approach over the original one where both of them had label num? There seems to be a sense of laziness here, but the total number of class checks one a given number when using ifz seems to be the same.
[SCW: The second approach is more common in dynamic languages.It is laziness, and like with laziness it allows you to work with code with errors as long as you don't trigger the errors. I.e. if you never take the predecessor of succ (true) then you're ok.]
-
In 22.2: Why have the conditional cond distinguish between "nil and all other values"? Why not provide such "this or everything else" elimination forms for every form in the language? This seems nicer than the nil? cons? num? etc... predicates he discusses.
[SCW: You are talking about the end of 22.2 where Bob proposes this treatment of if, which gives special preference to the "nil" value.
v not nil ----------------------------- if v then e1 else e2 -> e1 v nil ----------------------------- if v then e1 else e2 -> e2What you propose is possible, but I've not seen it in practice.]
-
I don't understand the role of the negative class-checking rules in the dynamics. Can we discuss why we need both positive and negative characterizations of class-membership?
[SCW: we need the neagative versions to know when to signal an error in the 22.1 semantics. We could expand it into the complement of the other forms (i.e. isnt_num v == is_fun v || is_bool v || ... ) so it is not strictly necessary.]
-
In Python, we can use types to form boolean expressions as: if type(a) != type(b): raise "Arguments not of the same type" This makes it possible to infer the type during compilation and avoid runtime type error. What is the advantage of replacing such methods with errors?
[SCW: I don't understand your question. Isn't this a dynamic type test?]
-
Another thought: In Coq, we cannot do pattern matching on types. Is it theoretically possible to do so?
[SCW: Yes! There are statically typed languages that do so. (Perhaps even Haskell one day.) ]