3 ms·

From just skimming the intro, this seems like very exciting work. And the formulation of the problem in terms of data flow was really novel to me. I was surpri

From just skimming the intro, this seems like very exciting work. And the formulation of the problem in terms of data flow was really novel to me. I was surprised that I couldn't find any references to Martin Odersky in the paper, whose work for years at EPFL has been focused on unifying functional and object oriented programming under a sound type system. This work produced the Scala programming language. More recently, he reworked the foundations of Scala using a system he developed called the calculus of dependent object types (DOT) [1]. I couldn't seem to find any references to this in the thesis. It's hard to imagine the author was unaware of this work, but I'm really interested in hearing more about how the two approaches compare. Anyway, I'm imagining this work could have great applications for things like TypeScript, and maybe even Scala. [1] http://scala-lang.org/blog/2016/02/03/essence-of-scala.html http://scala-lang.org/blog/2016/02/03/essence-of-scala.html

richard_todd 10y ago
Exactly, the first thing I searched for was scala, to see how the paper's ideas relate to scala's approach. I was surprised to see no obvious references. One would think it would be high on the list of existing material for anyone researching this area.
Jweb_Guru 10y ago
I'm really enjoying the thesis (it's super awesome!), but it does do a very, very bad job of citing related work. For example, it completely fails to cite logical relations literature despite using a bunch of techniques from it.
ezyang 10y ago
Scala's type inference is not complete; it is marketed as a way to "omit certain type annotations". One of the reasons why Hindley-Milner is so influential is because you really don't need any type annotations: the inference algorithm always works. As for DOT https://www.cs.purdue.edu/homes/rompf/papers/amin-wf16.pdf https://www.cs.purdue.edu/homes/rompf/papers/amin-wf16.pdf DOT is an explicitly typed calculus (similar to System F), for which no attempts at type inference are made. So... they're not really comparable at all.
- acjohnson55 10y ago
  Thanks for the insight. So, I suppose the follow-up question would be whether the techniques of the paper would make it possible to reformulate DOT without explicit types. Sorry if that's an ignorant question.
nuclx 10y ago
I had Oderski in mind as well when i skimmed this. Likewise I expected a Wadler referenced.
phaedrus 10y ago
It's an interesting coincidence seeing this paper and talks about data flow, because I'm interested in applying typing to logic programming for a practical system and also came to the conclusion that my type system needs to be aware of data flow. This is because variables in logic programming are usually individually bidirectional, but may not support all combinations. For instance, consider the logic relation "half(a, b) -> a = b/2 or b = 2a". If you pass in "a,_" it fills in the blank for "b" with the number which "a" is half of. If you pass in "_,b" it fills in the blank for "a" with the number that is half of "b". So, individually each "argument" to the relation is an input and an output. (What in C# would be called a "ref" arg, as opposed to an "out" arg or undecorated in arg.) However calling "half( _ , _ )" is not a valid use of this relation, and we would like the type checker to complain if it is used in this way. (What would one expect if both arguments are unset? Should it produce all pairs (n, 2n) in Z? Or perhaps all pairs ((float)0.5 n, (int)n)? An uncountably infinite set of pairs of Reals?) Clearly just marking individual arguments as "in" or "out" is not enough. The typing has to be more like "if I have this data I can get to that data" and "if I have this other data I can get to something else." I can't figure out a way to represent this in static types, but I believe it could be typed checked with dependent types. The examples with "select" near the beginning of the paper are not exactly the same thing, but are a similar problem and solution: data flow and the direction of the arrows matters.

richard_todd 10y ago

Exactly, the first thing I searched for was scala, to see how the paper's ideas relate to scala's approach. I was surprised to see no obvious references. One would think it would be high on the list of existing material for anyone researching this area.

Jweb_Guru 10y ago

I'm really enjoying the thesis (it's super awesome!), but it does do a very, very bad job of citing related work. For example, it completely fails to cite logical relations literature despite using a bunch of techniques from it.

ezyang 10y ago

Scala's type inference is not complete; it is marketed as a way to "omit certain type annotations". One of the reasons why Hindley-Milner is so influential is because you really don't need any type annotations: the inference algorithm always works. As for DOT https://www.cs.purdue.edu/homes/rompf/papers/amin-wf16.pdf https://www.cs.purdue.edu/homes/rompf/papers/amin-wf16.pdf DOT is an explicitly typed calculus (similar to System F), for which no attempts at type inference are made. So... they're not really comparable at all.

acjohnson55 10y ago
Thanks for the insight. So, I suppose the follow-up question would be whether the techniques of the paper would make it possible to reformulate DOT without explicit types. Sorry if that's an ignorant question.

nuclx 10y ago

I had Oderski in mind as well when i skimmed this. Likewise I expected a Wadler referenced.

phaedrus 10y ago

It's an interesting coincidence seeing this paper and talks about data flow, because I'm interested in applying typing to logic programming for a practical system and also came to the conclusion that my type system needs to be aware of data flow. This is because variables in logic programming are usually individually bidirectional, but may not support all combinations. For instance, consider the logic relation "half(a, b) -> a = b/2 or b = 2a". If you pass in "a,_" it fills in the blank for "b" with the number which "a" is half of. If you pass in "_,b" it fills in the blank for "a" with the number that is half of "b". So, individually each "argument" to the relation is an input and an output. (What in C# would be called a "ref" arg, as opposed to an "out" arg or undecorated in arg.) However calling "half( _ , _ )" is not a valid use of this relation, and we would like the type checker to complain if it is used in this way. (What would one expect if both arguments are unset? Should it produce all pairs (n, 2n) in Z? Or perhaps all pairs ((float)0.5 n, (int)n)? An uncountably infinite set of pairs of Reals?) Clearly just marking individual arguments as "in" or "out" is not enough. The typing has to be more like "if I have this data I can get to that data" and "if I have this other data I can get to something else." I can't figure out a way to represent this in static types, but I believe it could be typed checked with dependent types. The examples with "select" near the beginning of the paper are not exactly the same thing, but are a similar problem and solution: data flow and the direction of the arrows matters.