SCALA '17: "Effekt: Extensible Algebraic ..."
Effekt: Extensible Algebraic Effects in Scala (Short Paper)
Jonathan Immanuel Brachthäuser and Philipp Schuster
(University of Tübingen, Germany)
Algebraic effects are an interesting way to structure effectful programs and offer new modularity properties. We present the Scala library Effekt, which is implemented in terms of a monad for multi-prompt delimited continuations and centered around capability passing. This makes the newly proposed feature of implicit function types a perfect fit for the syntax of our library. Basing the library design on capability passing and a polymorphic embedding of effect handlers furthermore opens up interesting dimensions of extensibility. Preliminary benchmarks comparing Effekt with an established library suggest significant speedups.
@InProceedings{SCALA17p67,
author = {Jonathan Immanuel Brachthäuser and Philipp Schuster},
title = {Effekt: Extensible Algebraic Effects in Scala (Short Paper)},
booktitle = {Proc.\ SCALA},
publisher = {ACM},
pages = {67--72},
doi = {},
year = {2017},
}
SCALA '17: "Kompics Scala: Narrowing the ..."
Kompics Scala: Narrowing the Gap between Algorithmic Specification and Executable Code (Short Paper)
Lars Kroll, Paris Carbone, and Seif Haridi
(KTH, Sweden)
Message-based programming frameworks facilitate the development and execution of core distributed computing algorithms today. Their twofold aim is to expose a programming model that minimises logical errors incurred during translation from an algorithmic specification to executable program, and also to provide an efficient runtime for event pattern-matching and scheduling of distributed components. Kompics Scala is a framework that allows for a direct, streamlined translation from a formal algorithm specification to practical code by reducing the cognitive gap between the two representations. Furthermore, its runtime decouples event pattern-matching and component execution logic yielding clean, thoroughly expected behaviours. Our evaluation shows low and constant performance overhead of Kompics Scala compared to similar frameworks that otherwise fail to offer the same level of model clarity.
@InProceedings{SCALA17p73,
author = {Lars Kroll and Paris Carbone and Seif Haridi},
title = {Kompics Scala: Narrowing the Gap between Algorithmic Specification and Executable Code (Short Paper)},
booktitle = {Proc.\ SCALA},
publisher = {ACM},
pages = {73--77},
doi = {},
year = {2017},
}
SCALA '17: "ScalaSMT: Satisfiability Modulo ..."
ScalaSMT: Satisfiability Modulo Theory in Scala (Tool Paper)
Franck Cassez and Anthony M. Sloane
(Macquarie University, Australia)
Satisfiability modulo theory (SMT) consists of determining the satisfiability of logical formulas. It can reason in various formal theories, e.g., in linear integer or real arithmetic, first-order logic, or logics of arrays. An SMT solver is a program that implements the corresponding algorithms to automatically determine whether a logical formula is satisfiable.
The SMTLIB initiative provides a common input and output format based on S-expressions for interacting with SMT solvers. We present ScalaSMT, a Scala library that provides an abstraction over the SMTLIB format. The library brings consistency and type safety to the textual and dynamically typed world of SMTLIB solver interaction.
ScalaSMT relies on the SMTLIB input/output capabilities of the solvers and consequently provides access to numerous popular SMTLIB-compliant solvers such as Z3, CVC4, Yices, MathSat5 or SMTinterpol.
ScalaSMT is easily extendable (SMTLIB commands and theories can be added) and configurable (SMTLIB-compliant solvers can be added). ScalaSMT fills a gap in the Scala library landscape by providing support for powerful logical reasoning algorithms.
@InProceedings{SCALA17p51,
author = {Franck Cassez and Anthony M. Sloane},
title = {ScalaSMT: Satisfiability Modulo Theory in Scala (Tool Paper)},
booktitle = {Proc.\ SCALA},
publisher = {ACM},
pages = {51--55},
doi = {},
year = {2017},
}
Info
SCALA '17: "The Limitations of Type Classes ..."
The Limitations of Type Classes as Subtyped Implicits (Short Paper)
Adelbert Chang
Type classes enable a powerful form of ad-hoc polymorphism which provide solutions to many programming design problems. Inspired by this, Scala programmers have striven to emulate them in the design of libraries like Scalaz and Cats.
The natural encoding of type classes combines subtyping and implicits, both central features of Scala. However, this encoding has limitations. If the type class hierarchy branches, seemingly valid programs can hit implicit resolution failures. These failures must then be solved by explicitly passing the implicit arguments which is cumbersome and negates the advantages of type classes.
In this paper we describe instances of this problem and show that they are not merely theoretical but often arise in practice. We also discuss and compare the space of solutions to this problem in Scala today and in the future.
@InProceedings{SCALA17p8,
author = {Adelbert Chang},
title = {The Limitations of Type Classes as Subtyped Implicits (Short Paper)},
booktitle = {Proc.\ SCALA},
publisher = {ACM},
pages = {8--12},
doi = {},
year = {2017},
}
SCALA '17: "Typesafe Abstractions for ..."
Typesafe Abstractions for Tensor Operations (Short Paper)
Tongfei Chen
(Johns Hopkins University, USA)
We propose a typesafe abstraction to tensors (i.e. multidimensional arrays) exploiting the type-level programming capabilities of Scala through heterogeneous lists (HList), and showcase typesafe abstractions of common tensor operations and various neural layers such as convolution or recurrent neural networks. This abstraction could lay the foundation of future typesafe deep learning frameworks that runs on Scala/JVM.
@InProceedings{SCALA17p45,
author = {Tongfei Chen},
title = {Typesafe Abstractions for Tensor Operations (Short Paper)},
booktitle = {Proc.\ SCALA},
publisher = {ACM},
pages = {45--50},
doi = {},
year = {2017},
}
SCALA '17: "Making Collection Operations ..."
Making Collection Operations Optimal with Aggressive JIT Compilation
Aleksandar Prokopec, David Leopoldseder, Gilles Duboscq, and Thomas Würthinger
(Oracle Labs, Switzerland; JKU Linz, Austria)
Functional collection combinators are a neat and widely accepted data processing abstraction. However, their generic nature results in high abstraction overheads -- Scala collections are known to be notoriously slow for typical tasks. We show that proper optimizations in a JIT compiler can widely eliminate overheads imposed by these abstractions. Using the open-source Graal JIT compiler, we achieve speedups of up to 20x on collection workloads compared to the standard HotSpot C2 compiler. Consequently, a sufficiently aggressive JIT compiler allows the language compiler, such as Scalac, to focus on other concerns.
In this paper, we show how optimizations, such as inlining, polymorphic inlining, and partial escape analysis, are combined in Graal to produce collections code that is optimal with respect to manually written code, or close to optimal. We argue why some of these optimizations are more effectively done by a JIT compiler. We then identify specific use-cases that most current JIT compilers do not optimize well, warranting special treatment from the language compiler.
@InProceedings{SCALA17p29,
author = {Aleksandar Prokopec and David Leopoldseder and Gilles Duboscq and Thomas Würthinger},
title = {Making Collection Operations Optimal with Aggressive JIT Compilation},
booktitle = {Proc.\ SCALA},
publisher = {ACM},
pages = {29--40},
doi = {},
year = {2017},
}
SCALA '17: "Kompics Scala: Narrowing the ..."
Kompics Scala: Narrowing the Gap between Algorithmic Specification and Executable Code (Short Paper)
Lars Kroll, Paris Carbone, and Seif Haridi
(KTH, Sweden)
Message-based programming frameworks facilitate the development and execution of core distributed computing algorithms today. Their twofold aim is to expose a programming model that minimises logical errors incurred during translation from an algorithmic specification to executable program, and also to provide an efficient runtime for event pattern-matching and scheduling of distributed components. Kompics Scala is a framework that allows for a direct, streamlined translation from a formal algorithm specification to practical code by reducing the cognitive gap between the two representations. Furthermore, its runtime decouples event pattern-matching and component execution logic yielding clean, thoroughly expected behaviours. Our evaluation shows low and constant performance overhead of Kompics Scala compared to similar frameworks that otherwise fail to offer the same level of model clarity.
@InProceedings{SCALA17p73,
author = {Lars Kroll and Paris Carbone and Seif Haridi},
title = {Kompics Scala: Narrowing the Gap between Algorithmic Specification and Executable Code (Short Paper)},
booktitle = {Proc.\ SCALA},
publisher = {ACM},
pages = {73--77},
doi = {},
year = {2017},
}
SCALA '17: "Squid: Type-Safe, Hygienic, ..."
Squid: Type-Safe, Hygienic, and Reusable Quasiquotes
Lionel Parreaux, Amir Shaikhha, and Christoph E. Koch
(EPFL, Switzerland)
Quasiquotes have been shown to greatly simplify the task of metaprogramming. This is in part because they hide the data structures of the intermediate representation (IR), instead allowing metaprogrammers to use the concrete syntax of the language they manipulate. Scala has had “syntactic” quasiquotes for a long time, but still misses a statically-typed version like in MetaOCaml, Haskell and F#. This safer flavor of quasiquotes has been particularly useful for staging and domain-specific languages. In this paper we present Squid, a metaprogramming system for Scala that fills this gap. Squid quasiquotes are novel in three ways: they are the first statically-typed quasiquotes we know that allow code inspection (via pattern matching); they are implemented purely as a macro library, without modifications to the compiler; and they are reusable in the sense that they can manipulate different IRs. Adapting (or binding) a new IR to Squid is done simply by implementing a well-defined interface in the style of object algebras (i.e., tagless-final). We detail how Squid is implemented, leveraging the metaprogramming tools already offered by Scala, and show three application examples: the definition of a binding for a DSL in the style of LMS; a safe ANF conversion; and the introduction of type-safe, hygienic macros as an alternative to the current macro system.
@InProceedings{SCALA17p56,
author = {Lionel Parreaux and Amir Shaikhha and Christoph E. Koch},
title = {Squid: Type-Safe, Hygienic, and Reusable Quasiquotes},
booktitle = {Proc.\ SCALA},
publisher = {ACM},
pages = {56--66},
doi = {},
year = {2017},
}
SCALA '17: "Kompics Scala: Narrowing the ..."
Kompics Scala: Narrowing the Gap between Algorithmic Specification and Executable Code (Short Paper)
Lars Kroll, Paris Carbone, and Seif Haridi
(KTH, Sweden)
Message-based programming frameworks facilitate the development and execution of core distributed computing algorithms today. Their twofold aim is to expose a programming model that minimises logical errors incurred during translation from an algorithmic specification to executable program, and also to provide an efficient runtime for event pattern-matching and scheduling of distributed components. Kompics Scala is a framework that allows for a direct, streamlined translation from a formal algorithm specification to practical code by reducing the cognitive gap between the two representations. Furthermore, its runtime decouples event pattern-matching and component execution logic yielding clean, thoroughly expected behaviours. Our evaluation shows low and constant performance overhead of Kompics Scala compared to similar frameworks that otherwise fail to offer the same level of model clarity.
@InProceedings{SCALA17p73,
author = {Lars Kroll and Paris Carbone and Seif Haridi},
title = {Kompics Scala: Narrowing the Gap between Algorithmic Specification and Executable Code (Short Paper)},
booktitle = {Proc.\ SCALA},
publisher = {ACM},
pages = {73--77},
doi = {},
year = {2017},
}
SCALA '17: "Making Collection Operations ..."
Making Collection Operations Optimal with Aggressive JIT Compilation
Aleksandar Prokopec, David Leopoldseder, Gilles Duboscq, and Thomas Würthinger
(Oracle Labs, Switzerland; JKU Linz, Austria)
Functional collection combinators are a neat and widely accepted data processing abstraction. However, their generic nature results in high abstraction overheads -- Scala collections are known to be notoriously slow for typical tasks. We show that proper optimizations in a JIT compiler can widely eliminate overheads imposed by these abstractions. Using the open-source Graal JIT compiler, we achieve speedups of up to 20x on collection workloads compared to the standard HotSpot C2 compiler. Consequently, a sufficiently aggressive JIT compiler allows the language compiler, such as Scalac, to focus on other concerns.
In this paper, we show how optimizations, such as inlining, polymorphic inlining, and partial escape analysis, are combined in Graal to produce collections code that is optimal with respect to manually written code, or close to optimal. We argue why some of these optimizations are more effectively done by a JIT compiler. We then identify specific use-cases that most current JIT compilers do not optimize well, warranting special treatment from the language compiler.
@InProceedings{SCALA17p29,
author = {Aleksandar Prokopec and David Leopoldseder and Gilles Duboscq and Thomas Würthinger},
title = {Making Collection Operations Optimal with Aggressive JIT Compilation},
booktitle = {Proc.\ SCALA},
publisher = {ACM},
pages = {29--40},
doi = {},
year = {2017},
}
SCALA '17: "Interactive Development using ..."
Interactive Development using the Dotty Compiler (Tool Paper)
Guillaume Martres
(EPFL, Switzerland)
A programming language is only as good at its tooling. Traditionally, tooling has always been an after-thought of language design since developing good tools take significant development efforts. Dotty is an experimental compiler for what will one day be called Scala 3, and Scala already has established and functional tooling. For Dotty to be seen as a viable alternative to Scala 2, it needs to deliver a developer experience at least as good. In particular, good support for Integrated Development Environments (IDEs) is crucial. In this paper we report our progress on providing IDE support for Dotty.
@InProceedings{SCALA17p41,
author = {Guillaume Martres},
title = {Interactive Development using the Dotty Compiler (Tool Paper)},
booktitle = {Proc.\ SCALA},
publisher = {ACM},
pages = {41--44},
doi = {},
year = {2017},
}
SCALA '17: "Towards Algorithmic Typing ..."
Towards Algorithmic Typing for DOT (Short Paper)
Abel Nieto
(University of Waterloo, Canada)
The Dependent Object Types (DOT) calculus formalizes key features of Scala. The D<: calculus is the core of DOT. To date, presentations of D<: have used declarative, as opposed to algorithmic, typing and subtyping rules. Unfortunately, algorithmic typing for full D<: is known to be an undecidable problem.
We explore the design space for a restricted version of D<: that has decidable typechecking. Even in this simplified D<:, algorithmic typing and subtyping are tricky, due to the “bad bounds” problem. The Scala compiler bypasses bad bounds at the cost of a loss in expressiveness in its type system. Based on the approach taken in the Scala compiler, we present the Step Typing and Step Subtyping relations for D<:. These relations are sound and decidable. They are not complete with respect to the original D<: typing rules.
@InProceedings{SCALA17p2,
author = {Abel Nieto},
title = {Towards Algorithmic Typing for DOT (Short Paper)},
booktitle = {Proc.\ SCALA},
publisher = {ACM},
pages = {2--7},
doi = {},
year = {2017},
}
SCALA '17: "A Scala Framework for Supercompilation ..."
A Scala Framework for Supercompilation
Nathaniel Nystrom
(University of Lugano, Switzerland)
Supercompilation is a program transformation technique that attempts to evaluate programs as much as possible at compile time. Supercompilation has been used for theorem proving, function inversion, and most notably optimization, especially of functional programs. However, the technique has numerous practical problems that prevent it from being applied in mainstream compilers. In this paper, we describe a framework that can be used for experimenting with supercompilation techniques. Our framework allows supercompilers to be constructed directly from an interpreter. The user specifies the interpreter using rewrite rules and the framework handles termination checking, generalization, and residualization. We demonstrate the approach by implementing a supercompiler for JavaScript.
@InProceedings{SCALA17p18,
author = {Nathaniel Nystrom},
title = {A Scala Framework for Supercompilation},
booktitle = {Proc.\ SCALA},
publisher = {ACM},
pages = {18--28},
doi = {},
year = {2017},
}
SCALA '17: "Rust-Like Borrowing with 2nd-Class ..."
Rust-Like Borrowing with 2nd-Class Values (Short Paper)
Leo Osvald and Tiark Rompf
(Purdue University, USA)
The Rust programming language demonstrates that memory safety can be achieved in a practical systems language, based on a sophisticated type system that controls object lifetimes and aliasing through notions of ownership and borrowing. While Scala has traditionally targeted only managed language runtimes, the ScalaNative effort makes Scala a viable low-level language as well. Thus, memory safety becomes an important concern, and the question bears asking what, if anything, Scala can learn from Rust. In addition, Rust's type system can encode forms of protocols, state machines, and session types, which would also be useful for Scala in general. A key challenge is that Rust's typing rules are inherently flow-sensitive, but Scala's type system is not. In this paper, we sketch one possible method of achieving static guarantees similar to Rust with only mild extensions to Scala's type system. Our solution is based on two components: First, the observation that continuation passing style (CPS) or monadic style can transform a flow-sensitive checking problem into a type-checking problem based on scopes. Second, on a previously presented type system extension with second-class values, which we use to model scope-based lifetimes.
@InProceedings{SCALA17p13,
author = {Leo Osvald and Tiark Rompf},
title = {Rust-Like Borrowing with 2nd-Class Values (Short Paper)},
booktitle = {Proc.\ SCALA},
publisher = {ACM},
pages = {13--17},
doi = {},
year = {2017},
}
SCALA '17: "Squid: Type-Safe, Hygienic, ..."
Squid: Type-Safe, Hygienic, and Reusable Quasiquotes
Lionel Parreaux, Amir Shaikhha, and Christoph E. Koch
(EPFL, Switzerland)
Quasiquotes have been shown to greatly simplify the task of metaprogramming. This is in part because they hide the data structures of the intermediate representation (IR), instead allowing metaprogrammers to use the concrete syntax of the language they manipulate. Scala has had “syntactic” quasiquotes for a long time, but still misses a statically-typed version like in MetaOCaml, Haskell and F#. This safer flavor of quasiquotes has been particularly useful for staging and domain-specific languages. In this paper we present Squid, a metaprogramming system for Scala that fills this gap. Squid quasiquotes are novel in three ways: they are the first statically-typed quasiquotes we know that allow code inspection (via pattern matching); they are implemented purely as a macro library, without modifications to the compiler; and they are reusable in the sense that they can manipulate different IRs. Adapting (or binding) a new IR to Squid is done simply by implementing a well-defined interface in the style of object algebras (i.e., tagless-final). We detail how Squid is implemented, leveraging the metaprogramming tools already offered by Scala, and show three application examples: the definition of a binding for a DSL in the style of LMS; a safe ANF conversion; and the introduction of type-safe, hygienic macros as an alternative to the current macro system.
@InProceedings{SCALA17p56,
author = {Lionel Parreaux and Amir Shaikhha and Christoph E. Koch},
title = {Squid: Type-Safe, Hygienic, and Reusable Quasiquotes},
booktitle = {Proc.\ SCALA},
publisher = {ACM},
pages = {56--66},
doi = {},
year = {2017},
}
SCALA '17: "Making Collection Operations ..."
Making Collection Operations Optimal with Aggressive JIT Compilation
Aleksandar Prokopec, David Leopoldseder, Gilles Duboscq, and Thomas Würthinger
(Oracle Labs, Switzerland; JKU Linz, Austria)
Functional collection combinators are a neat and widely accepted data processing abstraction. However, their generic nature results in high abstraction overheads -- Scala collections are known to be notoriously slow for typical tasks. We show that proper optimizations in a JIT compiler can widely eliminate overheads imposed by these abstractions. Using the open-source Graal JIT compiler, we achieve speedups of up to 20x on collection workloads compared to the standard HotSpot C2 compiler. Consequently, a sufficiently aggressive JIT compiler allows the language compiler, such as Scalac, to focus on other concerns.
In this paper, we show how optimizations, such as inlining, polymorphic inlining, and partial escape analysis, are combined in Graal to produce collections code that is optimal with respect to manually written code, or close to optimal. We argue why some of these optimizations are more effectively done by a JIT compiler. We then identify specific use-cases that most current JIT compilers do not optimize well, warranting special treatment from the language compiler.
@InProceedings{SCALA17p29,
author = {Aleksandar Prokopec and David Leopoldseder and Gilles Duboscq and Thomas Würthinger},
title = {Making Collection Operations Optimal with Aggressive JIT Compilation},
booktitle = {Proc.\ SCALA},
publisher = {ACM},
pages = {29--40},
doi = {},
year = {2017},
}
SCALA '17: "Rust-Like Borrowing with 2nd-Class ..."
Rust-Like Borrowing with 2nd-Class Values (Short Paper)
Leo Osvald and Tiark Rompf
(Purdue University, USA)
The Rust programming language demonstrates that memory safety can be achieved in a practical systems language, based on a sophisticated type system that controls object lifetimes and aliasing through notions of ownership and borrowing. While Scala has traditionally targeted only managed language runtimes, the ScalaNative effort makes Scala a viable low-level language as well. Thus, memory safety becomes an important concern, and the question bears asking what, if anything, Scala can learn from Rust. In addition, Rust's type system can encode forms of protocols, state machines, and session types, which would also be useful for Scala in general. A key challenge is that Rust's typing rules are inherently flow-sensitive, but Scala's type system is not. In this paper, we sketch one possible method of achieving static guarantees similar to Rust with only mild extensions to Scala's type system. Our solution is based on two components: First, the observation that continuation passing style (CPS) or monadic style can transform a flow-sensitive checking problem into a type-checking problem based on scopes. Second, on a previously presented type system extension with second-class values, which we use to model scope-based lifetimes.
@InProceedings{SCALA17p13,
author = {Leo Osvald and Tiark Rompf},
title = {Rust-Like Borrowing with 2nd-Class Values (Short Paper)},
booktitle = {Proc.\ SCALA},
publisher = {ACM},
pages = {13--17},
doi = {},
year = {2017},
}
SCALA '17: "Effekt: Extensible Algebraic ..."
Effekt: Extensible Algebraic Effects in Scala (Short Paper)
Jonathan Immanuel Brachthäuser and Philipp Schuster
(University of Tübingen, Germany)
Algebraic effects are an interesting way to structure effectful programs and offer new modularity properties. We present the Scala library Effekt, which is implemented in terms of a monad for multi-prompt delimited continuations and centered around capability passing. This makes the newly proposed feature of implicit function types a perfect fit for the syntax of our library. Basing the library design on capability passing and a polymorphic embedding of effect handlers furthermore opens up interesting dimensions of extensibility. Preliminary benchmarks comparing Effekt with an established library suggest significant speedups.
@InProceedings{SCALA17p67,
author = {Jonathan Immanuel Brachthäuser and Philipp Schuster},
title = {Effekt: Extensible Algebraic Effects in Scala (Short Paper)},
booktitle = {Proc.\ SCALA},
publisher = {ACM},
pages = {67--72},
doi = {},
year = {2017},
}
SCALA '17: "Squid: Type-Safe, Hygienic, ..."
Squid: Type-Safe, Hygienic, and Reusable Quasiquotes
Lionel Parreaux, Amir Shaikhha, and Christoph E. Koch
(EPFL, Switzerland)
Quasiquotes have been shown to greatly simplify the task of metaprogramming. This is in part because they hide the data structures of the intermediate representation (IR), instead allowing metaprogrammers to use the concrete syntax of the language they manipulate. Scala has had “syntactic” quasiquotes for a long time, but still misses a statically-typed version like in MetaOCaml, Haskell and F#. This safer flavor of quasiquotes has been particularly useful for staging and domain-specific languages. In this paper we present Squid, a metaprogramming system for Scala that fills this gap. Squid quasiquotes are novel in three ways: they are the first statically-typed quasiquotes we know that allow code inspection (via pattern matching); they are implemented purely as a macro library, without modifications to the compiler; and they are reusable in the sense that they can manipulate different IRs. Adapting (or binding) a new IR to Squid is done simply by implementing a well-defined interface in the style of object algebras (i.e., tagless-final). We detail how Squid is implemented, leveraging the metaprogramming tools already offered by Scala, and show three application examples: the definition of a binding for a DSL in the style of LMS; a safe ANF conversion; and the introduction of type-safe, hygienic macros as an alternative to the current macro system.
@InProceedings{SCALA17p56,
author = {Lionel Parreaux and Amir Shaikhha and Christoph E. Koch},
title = {Squid: Type-Safe, Hygienic, and Reusable Quasiquotes},
booktitle = {Proc.\ SCALA},
publisher = {ACM},
pages = {56--66},
doi = {},
year = {2017},
}
SCALA '17: "ScalaSMT: Satisfiability Modulo ..."
ScalaSMT: Satisfiability Modulo Theory in Scala (Tool Paper)
Franck Cassez and Anthony M. Sloane
(Macquarie University, Australia)
Satisfiability modulo theory (SMT) consists of determining the satisfiability of logical formulas. It can reason in various formal theories, e.g., in linear integer or real arithmetic, first-order logic, or logics of arrays. An SMT solver is a program that implements the corresponding algorithms to automatically determine whether a logical formula is satisfiable.
The SMTLIB initiative provides a common input and output format based on S-expressions for interacting with SMT solvers. We present ScalaSMT, a Scala library that provides an abstraction over the SMTLIB format. The library brings consistency and type safety to the textual and dynamically typed world of SMTLIB solver interaction.
ScalaSMT relies on the SMTLIB input/output capabilities of the solvers and consequently provides access to numerous popular SMTLIB-compliant solvers such as Z3, CVC4, Yices, MathSat5 or SMTinterpol.
ScalaSMT is easily extendable (SMTLIB commands and theories can be added) and configurable (SMTLIB-compliant solvers can be added). ScalaSMT fills a gap in the Scala library landscape by providing support for powerful logical reasoning algorithms.
@InProceedings{SCALA17p51,
author = {Franck Cassez and Anthony M. Sloane},
title = {ScalaSMT: Satisfiability Modulo Theory in Scala (Tool Paper)},
booktitle = {Proc.\ SCALA},
publisher = {ACM},
pages = {51--55},
doi = {},
year = {2017},
}
Info
SCALA '17: "Making Collection Operations ..."
Making Collection Operations Optimal with Aggressive JIT Compilation
Aleksandar Prokopec, David Leopoldseder, Gilles Duboscq, and Thomas Würthinger
(Oracle Labs, Switzerland; JKU Linz, Austria)
Functional collection combinators are a neat and widely accepted data processing abstraction. However, their generic nature results in high abstraction overheads -- Scala collections are known to be notoriously slow for typical tasks. We show that proper optimizations in a JIT compiler can widely eliminate overheads imposed by these abstractions. Using the open-source Graal JIT compiler, we achieve speedups of up to 20x on collection workloads compared to the standard HotSpot C2 compiler. Consequently, a sufficiently aggressive JIT compiler allows the language compiler, such as Scalac, to focus on other concerns.
In this paper, we show how optimizations, such as inlining, polymorphic inlining, and partial escape analysis, are combined in Graal to produce collections code that is optimal with respect to manually written code, or close to optimal. We argue why some of these optimizations are more effectively done by a JIT compiler. We then identify specific use-cases that most current JIT compilers do not optimize well, warranting special treatment from the language compiler.
@InProceedings{SCALA17p29,
author = {Aleksandar Prokopec and David Leopoldseder and Gilles Duboscq and Thomas Würthinger},
title = {Making Collection Operations Optimal with Aggressive JIT Compilation},
booktitle = {Proc.\ SCALA},
publisher = {ACM},
pages = {29--40},
doi = {},
year = {2017},
}
SCALA '17: "Spark and Scala (Keynote) ..."
Spark and Scala (Keynote)
Reynold Xin
(Databricks, USA)
Written mostly in Scala and with over 1000 contributors, Apache Spark has become the de facto standard for big data processing. In this talk, I will review the evolution of Spark for the last seven years and our experience using Scala as the main programming language in a high profile open source project with a distributed team. I will outline language features that we can't live without, and features we wish were designed differently. Last but not least, I will discuss how we at Databricks are leveraging native code to further improve performance.
@InProceedings{SCALA17p1,
author = {Reynold Xin},
title = {Spark and Scala (Keynote)},
booktitle = {Proc.\ SCALA},
publisher = {ACM},
pages = {1--1},
doi = {10.1145/3136000.3148042},
year = {2017},
}
Publisher's Version