Collapsible Contracts

Fixing a Pathology of Gradual Typing

Daniel Feltey, Ben Greenman, Christophe Scholliers, Robert Findler, Vincent St Amour

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

The promise of gradual typing is that programmers should get the best of both worlds: the static guarantees of static types, and the dynamic flexibility of untyped programming. This is an enticing benefit, but one that, in practice, may carry significant costs. Significant enough, in fact, to threaten the very practicality of gradual typing; slowdowns as high as 120x are reported as arising from gradual typing.

If one examines these results closely, though, it becomes clear that the costs of gradual typing are not evenly distributed. Indeed, while mixing typed and untyped code almost invariably carries non-trivial costs, many truly deal-breaking slowdowns exhibit pathological performance. Unfortunately, the very presence of these pathological cases---and therefore the possibility of hitting them during development---makes gradual typing a risky proposition in any setting that even remotely cares about performance.

This work attacks one source of large overheads in these pathological cases: an accumulation of contract wrappers that perform redundant checks. The work introduces a novel strategy for contract checking---collapsible contracts---which eliminates this redundancy for function and vector contracts and drastically reduces the overhead of contract wrappers.

We implemented this checking strategy as part of the Racket contract system, which is used in the Typed Racket gradual typing system. Our experiments show that our strategy successfully brings a class of pathological cases in line with normal cases, while not introducing an undue overhead to any of the other cases. Our results also show that the performance of gradual typing in Racket remains prohibitive for many programs, but that collapsible contracts are one essential ingredient in reducing the cost of gradual typing.
Original languageEnglish (US)
Title of host publicationProceedings of the ACM on Programming Languages 2018
Volume2 (OOPSLA)
StatePublished - 2018

Fingerprint

Pathology
Costs
Redundancy
Experiments

Cite this

Feltey, D., Greenman, B., Scholliers, C., Findler, R., & St Amour, V. (2018). Collapsible Contracts: Fixing a Pathology of Gradual Typing. In Proceedings of the ACM on Programming Languages 2018 (Vol. 2 (OOPSLA)). [133]
Feltey, Daniel ; Greenman, Ben ; Scholliers, Christophe ; Findler, Robert ; St Amour, Vincent. / Collapsible Contracts : Fixing a Pathology of Gradual Typing. Proceedings of the ACM on Programming Languages 2018. Vol. 2 (OOPSLA) 2018.
@inproceedings{c3dd36856c26451b9202dda3d79de5a4,
title = "Collapsible Contracts: Fixing a Pathology of Gradual Typing",
abstract = "The promise of gradual typing is that programmers should get the best of both worlds: the static guarantees of static types, and the dynamic flexibility of untyped programming. This is an enticing benefit, but one that, in practice, may carry significant costs. Significant enough, in fact, to threaten the very practicality of gradual typing; slowdowns as high as 120x are reported as arising from gradual typing.If one examines these results closely, though, it becomes clear that the costs of gradual typing are not evenly distributed. Indeed, while mixing typed and untyped code almost invariably carries non-trivial costs, many truly deal-breaking slowdowns exhibit pathological performance. Unfortunately, the very presence of these pathological cases---and therefore the possibility of hitting them during development---makes gradual typing a risky proposition in any setting that even remotely cares about performance.This work attacks one source of large overheads in these pathological cases: an accumulation of contract wrappers that perform redundant checks. The work introduces a novel strategy for contract checking---collapsible contracts---which eliminates this redundancy for function and vector contracts and drastically reduces the overhead of contract wrappers.We implemented this checking strategy as part of the Racket contract system, which is used in the Typed Racket gradual typing system. Our experiments show that our strategy successfully brings a class of pathological cases in line with normal cases, while not introducing an undue overhead to any of the other cases. Our results also show that the performance of gradual typing in Racket remains prohibitive for many programs, but that collapsible contracts are one essential ingredient in reducing the cost of gradual typing.",
author = "Daniel Feltey and Ben Greenman and Christophe Scholliers and Robert Findler and {St Amour}, Vincent",
note = "Doi>10.1145/3276503",
year = "2018",
language = "English (US)",
volume = "2 (OOPSLA)",
booktitle = "Proceedings of the ACM on Programming Languages 2018",

}

Feltey, D, Greenman, B, Scholliers, C, Findler, R & St Amour, V 2018, Collapsible Contracts: Fixing a Pathology of Gradual Typing. in Proceedings of the ACM on Programming Languages 2018. vol. 2 (OOPSLA), 133.

Collapsible Contracts : Fixing a Pathology of Gradual Typing. / Feltey, Daniel; Greenman, Ben; Scholliers, Christophe; Findler, Robert; St Amour, Vincent.

Proceedings of the ACM on Programming Languages 2018. Vol. 2 (OOPSLA) 2018. 133.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

TY - GEN

T1 - Collapsible Contracts

T2 - Fixing a Pathology of Gradual Typing

AU - Feltey, Daniel

AU - Greenman, Ben

AU - Scholliers, Christophe

AU - Findler, Robert

AU - St Amour, Vincent

N1 - Doi>10.1145/3276503

PY - 2018

Y1 - 2018

N2 - The promise of gradual typing is that programmers should get the best of both worlds: the static guarantees of static types, and the dynamic flexibility of untyped programming. This is an enticing benefit, but one that, in practice, may carry significant costs. Significant enough, in fact, to threaten the very practicality of gradual typing; slowdowns as high as 120x are reported as arising from gradual typing.If one examines these results closely, though, it becomes clear that the costs of gradual typing are not evenly distributed. Indeed, while mixing typed and untyped code almost invariably carries non-trivial costs, many truly deal-breaking slowdowns exhibit pathological performance. Unfortunately, the very presence of these pathological cases---and therefore the possibility of hitting them during development---makes gradual typing a risky proposition in any setting that even remotely cares about performance.This work attacks one source of large overheads in these pathological cases: an accumulation of contract wrappers that perform redundant checks. The work introduces a novel strategy for contract checking---collapsible contracts---which eliminates this redundancy for function and vector contracts and drastically reduces the overhead of contract wrappers.We implemented this checking strategy as part of the Racket contract system, which is used in the Typed Racket gradual typing system. Our experiments show that our strategy successfully brings a class of pathological cases in line with normal cases, while not introducing an undue overhead to any of the other cases. Our results also show that the performance of gradual typing in Racket remains prohibitive for many programs, but that collapsible contracts are one essential ingredient in reducing the cost of gradual typing.

AB - The promise of gradual typing is that programmers should get the best of both worlds: the static guarantees of static types, and the dynamic flexibility of untyped programming. This is an enticing benefit, but one that, in practice, may carry significant costs. Significant enough, in fact, to threaten the very practicality of gradual typing; slowdowns as high as 120x are reported as arising from gradual typing.If one examines these results closely, though, it becomes clear that the costs of gradual typing are not evenly distributed. Indeed, while mixing typed and untyped code almost invariably carries non-trivial costs, many truly deal-breaking slowdowns exhibit pathological performance. Unfortunately, the very presence of these pathological cases---and therefore the possibility of hitting them during development---makes gradual typing a risky proposition in any setting that even remotely cares about performance.This work attacks one source of large overheads in these pathological cases: an accumulation of contract wrappers that perform redundant checks. The work introduces a novel strategy for contract checking---collapsible contracts---which eliminates this redundancy for function and vector contracts and drastically reduces the overhead of contract wrappers.We implemented this checking strategy as part of the Racket contract system, which is used in the Typed Racket gradual typing system. Our experiments show that our strategy successfully brings a class of pathological cases in line with normal cases, while not introducing an undue overhead to any of the other cases. Our results also show that the performance of gradual typing in Racket remains prohibitive for many programs, but that collapsible contracts are one essential ingredient in reducing the cost of gradual typing.

M3 - Conference contribution

VL - 2 (OOPSLA)

BT - Proceedings of the ACM on Programming Languages 2018

ER -

Feltey D, Greenman B, Scholliers C, Findler R, St Amour V. Collapsible Contracts: Fixing a Pathology of Gradual Typing. In Proceedings of the ACM on Programming Languages 2018. Vol. 2 (OOPSLA). 2018. 133