[racket-users] "Is Sound Gradual Typing Dead?"

[Matthew Butterick]

Under Betteridge's Law, I was expecting that a paper so titled [1] would 
conclude that the answer is no. But it does ultimately assert that "In the 
context of current implementation technology, sound gradual typing is dead." 
(With a silver lining that some new research questions have been discovered.)

What is the upshot for those of us whose Racketeering is more in the practical 
rather than research realm? On its face, this paper seems to tell me "don't use 
TR." Is that accurate? Is there a category of practical programs that TR 
remains suitable for? 

I ask this as one of the guinea pigs studied in the paper [2]. I originally 
picked up TR because I was curious whether it would be suitable for a project 
where performance is a key consideration. Instead, TR slowed it down. Though I 
was relieved to learn that my bad programming was not entirely the culprit, now 
I feel bad about helping kill TR.



[1] http://www.ccs.neu.edu/racket/pubs/popl16-tfgnvf.pdf

[2] https://github.com/mbutterick/quad

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] "Is Sound Gradual Typing Dead?"

[Benjamin Greenman]

>
> now I feel bad about helping kill TR


Far from it! Quad (and the math library, etc) are inspiring the bright
future*™* of Typed Racket. The next paper should be titled "No!", based on
improvements since today's results.

[[ From an academic perspective, this paper is about establishing an
evaluation framework for gradual typing ]]

The end-user message from this paper is *not* "you should avoid Typed
Racket". Most of the fully-typed versions of our projects ran about the
same as the fully-typed ones, and sometimes faster. The caveats were:

   1. Projects using an untyped library slowed down in the fully-typed case

   2. Quad, which used type-generated predicates to do typechecking at
   runtime. (Predicates are just functions -- they're a slow alternative to
   compile-time typechecking)

The message is: you should be *very careful* about mixing typed and untyped
code. Passing higher-order functions over a boundary is obviously
expensive. Less obvious is that sharing a large list across a boundary
triggers an O(n) check at each crossing.

We already knew these costs were bad. The surprise was that nearly all ways
of gradually typing many programs led to slowdowns of at least 10x. So the
promise that you can freely mix typed and untyped code is an empty one.

[[ Going forward, we're looking into making less-expensive (or smarter)
contracts for types and program analysis tools to help avoid the expensive
boundaries. As a first step, struct predicate functions are now "trusted"
to have (-> Any Boolean) type and we've seen improvements like this

(the bottom graph is current, read it as "almost 60% of gradually-typed
configurations run with at most a 10x slowdown") ]]

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] "Is Sound Gradual Typing Dead?"

[Leif Andersen]

> Most of the fully-typed versions of our projects ran about the same as the 
> fully-typed ones, and sometimes faster.

Yes, the fully-typed ones run as fast as the fully-typed ones. ;)

I think you meant:

"Most of the fully-typed versions of our projects ran about the same
as the fully-untyped ones, and sometimes faster."

~Leif Andersen


On Fri, Dec 4, 2015 at 6:38 PM, Benjamin Greenman
 wrote:
>> now I feel bad about helping kill TR
>
>
> Far from it! Quad (and the math library, etc) are inspiring the bright
> future™ of Typed Racket. The next paper should be titled "No!", based on
> improvements since today's results.
>
> [[ From an academic perspective, this paper is about establishing an
> evaluation framework for gradual typing ]]
>
> The end-user message from this paper is not "you should avoid Typed Racket".
> Most of the fully-typed versions of our projects ran about the same as the
> fully-typed ones, and sometimes faster. The caveats were:
>
> Projects using an untyped library slowed down in the fully-typed case
>
> Quad, which used type-generated predicates to do typechecking at runtime.
> (Predicates are just functions -- they're a slow alternative to compile-time
> typechecking)
>
> The message is: you should be very careful about mixing typed and untyped
> code. Passing higher-order functions over a boundary is obviously expensive.
> Less obvious is that sharing a large list across a boundary triggers an O(n)
> check at each crossing.
>
> We already knew these costs were bad. The surprise was that nearly all ways
> of gradually typing many programs led to slowdowns of at least 10x. So the
> promise that you can freely mix typed and untyped code is an empty one.
>
> [[ Going forward, we're looking into making less-expensive (or smarter)
> contracts for types and program analysis tools to help avoid the expensive
> boundaries. As a first step, struct predicate functions are now "trusted" to
> have (-> Any Boolean) type and we've seen improvements like this (the bottom
> graph is current, read it as "almost 60% of gradually-typed configurations
> run with at most a 10x slowdown") ]]
>
> --
> You received this message because you are subscribed to the Google Groups
> "Racket Users" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to racket-users+unsubscr...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] "Is Sound Gradual Typing Dead?"

[Matthias Felleisen]

> On Dec 4, 2015, at 5:06 PM, Matthew Butterick  wrote:
> 
> Under Betteridge's Law, I was expecting that a paper so titled [1] would 
> conclude that the answer is no. But it does ultimately assert that "In the 
> context of current implementation technology, sound gradual typing is dead." 
> (With a silver lining that some new research questions have been discovered.)
> 
> What is the upshot for those of us whose Racketeering is more in the 
> practical rather than research realm? On its face, this paper seems to tell 
> me "don't use TR." Is that accurate? Is there a category of practical 
> programs that TR remains suitable for? 
> 
> I ask this as one of the guinea pigs studied in the paper [2]. I originally 
> picked up TR because I was curious whether it would be suitable for a project 
> where performance is a key consideration. Instead, TR slowed it down. Though 
> I was relieved to learn that my bad programming was not entirely the culprit, 
> now I feel bad about helping kill TR.



Matthew, 

thanks for bringing up this title/result. As the author of this title (and the 
somewhat sharper edges in the prose),  I owe the mailing list a general 
response. 

The title/paper are set up in this way to get the research community engaged. 
Typed Racket is the first and longest research development project in the 
gradual typing context (though the paper that Sam and I published did not use  
this phrase originally, which was coined in a parallel paper within a month of 
our design pub).  For most of the time since 2006, a fair number of efforts in 
this direction have focused on plain theory or moved toward optional unsound 
typing (you may say Int -> Int but I mean Int -> Real, too bad for you). In 
particular 

  nobody had any idea of how to measure whether a GT language would support the 
imagined gradual conversion of untyped programs into mostly typed ones. 

It is my opinion that semi-practical research questions such as this one call 
for a systematic evaluation, and I wanted to use the title/paper game to wake 
up the selection committee at POPL (our flagship conference in the research 
area). Well it did and the paper will appear there. 

— MAIN RESULT: The main result is really a method for measuring the 
“gradualness” of a GT language. We measure every possible way of tackling the 
conversion of an UNtyped program into a TYPED one for multi-module programs. 
The expectation is that (1) the top and the bottom should have approximately 
the same performance and (2) ideally the points (of partially converted 
programs) in between should perform well enough to be deliverable or at least 
useful. 

— COLLATERAL RESULT: As is, the evaluation method reveals that TR satisfies (1) 
but not (2). So if you use TR as intended — gradually convert a multi-module 
program into a partially typed one — you are extremely likely to experience 
serious performance problems. 

To the Racket/Typed Racket community, this collateral result is not a disaster. 
Instead it sets a research agenda, namely, to get TR to satisfy (2) 
linguistically (that is, as a language) or via IDE support that helps 
programmers identify and eliminate particularly bad trouble points in partially 
typed programs. 

Like everything in our language world, TR is a serious research effort meaning 
we are committed to invest a lot of energy and time into its realization. We 
will report progress as we make it and you’re likely to experience it before we 
say much about it, 

— Matthias



-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.