Belated thesis comments

[timholy]

I know these may be too late to be useful, but I only just got around to reading chunks of the more complete document.

HEAD at 00194015efe2c17f9a0f0bc143027d5f03ee6987

• p. 42, "the code does not mention types anywhere": confusing given the typeassert on the first line
• p. 42, "unlikely that the analysis can determine this": to someone already steeped in Julia this is a little non-obvious, because one might already be thinking in terms of a generic trunc that dispatches on its argument type. Moreover, thinking about how all this would work at the level of machine representation makes me wonder what a "generic" algorithm (say, written in C) would even mean, aside from the matlab answer of encoding all values as Float64s. (I assume you mean Int = "native machine representation of an integer" and not "a Float64 that happens to have integer value.") Stated another way, this whole discussion presupposes that there is already some type information, and hence one wonders why one can't make use of it. I guess much of your point is that the analysis is still harder: for each function you end up having to build a more complex table of inputs and outputs that requires analysis of all checks, whether or not they might be applicable to types you've already discovered. As yet another way to say it, trunc(y) == y is a very indirect way of saying y is an Int, and that hurts you. However, this wouldn't apply to if isa(y, Int). It might clearer to separate out two concepts: difficulty of analysis of functions that have many branch points, and the degree to which numerical behavior is a surrogate for type.
• p. 43, "and might not even know the type of n": must be Int given the typeassert
• p. 43, add a stub for ^ with y::Float (otherwise your statement "we have neither added restrictions" seems false)
• p. 49 (section on predicate dispatch): interesting (I guess this is what I was asking in #8154). Given that Julia's dispatch system can be thought of as predicate dispatch limited to the isa function, isn't the main issue that a general predicate dispatch system allows/encourages users to write complex predicates may not be statically decidable? Given that any dynamic dispatch system allows for this already (and Julia can't always infer types as it is), I think the boundary between what Julia currently does and full predicate dispatch is somewhat fuzzy---in a sense we already have a "second level" (only use the isa function), and that makes it hard to make a strong case against this. Presumably your best argument is that this restriction encourages users to write code for which the large majority of cases are decidable.
• p. 51: defining ADT in main text but the other abbreviations in the caption is confusing.
• p. 52, "Including more than one of these mechanisms makes a language especially complex and difficult to learn." By "mechanisms" I'm presuming you mean "rows of the table." There's the risk of confusion that assessing this involves counting checkboxes. By that metric, Julia has 3 checkboxes, so must be on its way to "especially complex and difficult to learn."
• p. 52, section on subtyping: this seems incomplete and doesn't really go anywhere
• p. 54: not sure how Java works, but I'm guessing this declaration allows the compiler to generate a "generic implementation" that still may not be fully optimal for all inputs? This point could use a little elaboration.
• p. 63: I'm not entirely convinced that "allowing ... in any position" would be entirely straightforward: doesn't it make the algorithm for type intersection more challenging? (Or at least, risk worse performance?) Matching Tuple{Int..., Real..., Int...} against (1, 3.2, 4, 7.3, 5), you have to decide the point at which to stop matching Real and continue on to Int---the fact that 4 is an Int is a red herring, because the next element 7.3 requires that you stick with Real. Naively, this seems to convert the problem of intersection from being O(n) in the caller arguments to O(m*n) in the caller/declaration arguments. However, I'm guessing this algorithm bears certain similarity with Regex matching, and I have the impression that it's possible to better than the naive algorithm. So maybe it's not as bad as it seems. Hmm, it's worse than just performance: in foo(a::Int..., b::Real...), does foo(1,2,3.2) yield a = (1,2), b = (3.2,) or a = (1,), b = (2,3.2)? I guess you'd have to introduce a constraint that vararg types must have empty intersection with the argument that follows.
• p. 64: I'd really like to understand Figure 4-1, but I don't know what the notation means. What are the "fractions"? What does \Gamma denote? What is a \vdash? (I was able to figure it out by going to the latex source and then googling, but that's too hard.) What does the dot mean? Presumably computer scientists won't have trouble with this notation, but your thesis may be read by people outside computer science, so at least a link to a page explaining standard notation would be very helpful. (Googling for "notation for algorithms" gives lots of hits about big-O notation, which doesn't help.)
• p. 64: introduces the term "tag type" (which is used later) without explicit definition
• p. 68/69: the distinction between simple and concrete is not clear to me. Perhaps some examples?
• p. 69, "If B<=A then A is not more specific than B". Really?

julia> ams(a, b) = ccall(:jl_args_morespecific, Cint, (Any,Any), a, b)
ams (generic function with 1 method)

julia> ams(Int, Int)
1

• p. 77: immitate -> imitate

[stevengj]

They are not too late; Jeff is finishing up the text over the next couple of days.

[JeffBezanson]

Thanks, this is helpful! I will incorporate all of this feedback.

As you discovered, yes some sections are still incomplete :)

Re predicates: supporting a single known predicate really does make all the difference!

[timholy]

Re predicates: supporting a single known predicate really does make all the difference!

I believe you :smile:. I just wondered if one might make that point more explicitly.

[JeffBezanson]

I think I incorporated changes for nearly all of this. See if you like my 2-sentence description of sequent calculus! :)

[timholy]

Very helpful 2 lines. Also the name is googleable, in case I or anyone else has further questions.