Menu

Typelevel Summit Lausanne

June 14, 2019 at École Polytechnique Fédérale de Lausanne

About the Summit

The eight Typelevel Summit will once again be co-located with Scala Days. Read more about all events in the blog post from the Scala Center.

The Summits are open to all, not just current contributors to and users of the Typelevel projects, and we are especially keen to encourage participation from people who are new to them. Whilst many of the Typelevel projects use somewhat “advanced” Scala, they are a lot more approachable than many people think, and a major part of Typelevel’s mission is to make the ideas they embody much more widely accessible. If you’re interested in types and pure functional programming we’d love to see you here!

Buy tickets

Speakers and Schedule

Stay tuned while we announce the full programme!

Time Talk
TBD
Lord of the rings: the Spire numerical towers
  • Denis Rosset

Spire defines around 80 typeclasses, including 30 coming from algebra and cats-kernel. We’ll see how much of that structure is dictated by mathematical laws, and which parts are the result of design decisions that balance different tradeoffs. In p...

More
TBD
Taking Resources to the Type Level
  • Vilem-Benjamin Liepelt

With the Granule project, we are working towards making statically typed functional languages more resource-aware, hence providing a way to enforce stateful protocols regarding memory, file handles, network interaction, etc. Static enforcement of ...

More
TBD
TwoFace values: a bridge between terms and types
  • Oron Port

Scala 2.13 introduces literal types, and with great types comes great thirst for power to control them. In this talk we get acquainted with the singleton-ops library, a typelevel programming library that enables constraining and performing operati...

More
TBD
Formal verification of Scala programs with Stainless
  • Romain Ruetschi

Everyone knows that writing bug-free code is fundamentally difficult, and that bugs will sometimes sneak in even in the presence of unit- or property-based tests. One solution to this problem is formal software verification. Formal verification al...

More
TBD
Actors Design Patterns and Arrowised FRP
  • Diego E. Alonso

Object-oriented design patterns combine basic language features to solve coding problems in an extensible way. In functional Scala, we solve those coding problems with functions, combinators, and type-classes, so design patterns are less relevant....

More
TBD
Exploring Scala Tooling ecosystem
  • Jeferson David Ossa

We are going to explore and compare some build tools with special focus on LSP/BSP implementations, IDEs and text editor support. To help the audience’s judgement about the tools that are suitable for their particular needs this talk aims to get a...

More
TBD
Want to Diversify the Scala Community? Here is How You Can Help!
  • Yifan Xing

The Scala community has grown significantly over the past 15 years. As a community, we wrote millions of lines of code and developed hundreds of projects. While the language is thriving, there is still room to contribute to the community. Differen...

More

Lord of the rings: the Spire numerical towers

at TBD

Spire defines around 80 typeclasses, including 30 coming from algebra and cats-kernel. We’ll see how much of that structure is dictated by mathematical laws, and which parts are the result of design decisions that balance different tradeoffs. In particular, we’ll discuss the different roles played by typeclasses in the Scala ecosystem:

  • as encoding operations obeying well-defined laws,
  • as enabling the use of a particular syntax for those operations, if possible close to the mathematical notation of a domain (and subfields often disagree on the notation!),
  • defining a context in which a combination of typeclasses implicitly imposes additional laws (for example, the ordering of numbers and addition),
  • enabling the user to change the variant of a relation being used (Order),
  • singling out one variant of a structure as canonical (cats: the additive Group for integers),
  • as selecting a particular algorithm for an operation (integer factorization: deterministic or Monte-Carlo).

It quickly becomes apparent that these roles conflict. With this in mind, we’ll have a look at some design choices made in Spire. We’ll discuss success stories, such as the clarification of the laws of the % operator, the commutative ring tower that formalizes integer factorization and Euclidean division. We’ll also discuss parts where trade offs have been made, such as the triplication of group structures (Group, AdditiveGroup, MultiplicativeGroup), the problem of coherent instances, especially when various typeclasses are combined. Time permitting, we’ll also discuss issues with law-based property checks (precision, range, time and memory complexity).

About Speaker

  • Denis Rosset

I’m a researcher in quantum physics with a strong interest in convex optimization and numerical/symbolical computing. I’ve been using Scala&Play since I wanted to build a database of research results, and Play seemed to be a reasonable solution. I fell in love with the Scala language since then, and am contributing to its open source ecosystem (Spire + personal libraries for mathematical computations).

Taking Resources to the Type Level

at TBD

With the Granule project, we are working towards making statically typed functional languages more resource-aware, hence providing a way to enforce stateful protocols regarding memory, file handles, network interaction, etc. Static enforcement of security policies and first-class support for multi-stage programming are further examples of what is possible in a type system based on Linear Logic and Graded Modalities. We present Granule, a functional programming language which combines parametric polymorphism and indexed types with such a type system. Granule programs will probably look very familiar to you, especially if you know some Haskell/ML, but in Granule’s type system we can reason about much more. Hillel Wayne’s Great Theorem Prover Showdown has made a point of the fact that there are many things we can’t easily reason about with functional (programming | proving)—up until now! We will implement leftPad in Granule and prove it correct with little more effort that writing the type signatures. We will then breeze through how Granule’s type system very naturally supports session-typed channels and safe mutable arrays.

About Speaker

  • Vilem-Benjamin Liepelt

I believe in static types & thoughtfully crafted APIs, good communication & documentation, and open-mindedness & fearless prototyping

TwoFace values: a bridge between terms and types

at TBD

Scala 2.13 introduces literal types, and with great types comes great thirst for power to control them. In this talk we get acquainted with the singleton-ops library, a typelevel programming library that enables constraining and performing operations on literal types. We learn about the library’s TwoFace value feature, and how it can be used to bridge the gap between types and terms by converting a type expression to term expression and vice-versa.

About Speaker

  • Oron Port

I am a third year Electrical Engineering Ph.D. student at Technion – Israel Institute of Technology. My research topic is “DFiant: A Dataflow Hardware Description Language”, a Scala-based DSL. I’m involved in and contribute to the Scala ecosystem and especially to the singleton-ops library.

Formal verification of Scala programs with Stainless

at TBD

Everyone knows that writing bug-free code is fundamentally difficult, and that bugs will sometimes sneak in even in the presence of unit- or property-based tests. One solution to this problem is formal software verification. Formal verification allows users to statically verify that software systems will never crash nor diverge, and will in addition satisfy given functional correctness properties. In this talk, I will present Stainless, a verification system for an expressive subset of Scala. I will start by explaining what formal verification is, what are some of the challenges people encounter when putting it into practice, and how it can be made more practical. Then I will give a high-level overview of Stainless, and finally present a few verified programs, such as a small actor system, a parallel map-reduce implementation, as well as a little surprise! I’ll also demonstrate the tooling we have developed around Stainless which lets users easily integrate Stainless in their SBT-based Scala projects.

About Speaker

  • Romain Ruetschi

I earned a MSc degree in Computer Science from EPFL in February 2018, and I have since been working at the Laboratory for Automated Reasoning and Analysis (LARA) at EPFL, under the supervision of Prof. Viktor Kunčak. I discovered Scala directly from Prof. Martin Ordersky during my Bachelor at EPFL a few years ago, and have never stopped learning more of it, alongside other languages such as Haskell, Rust or Idris. I am mainly interested in pure functional programming, type systems and formal methods.

Actors Design Patterns and Arrowised FRP

at TBD

Object-oriented design patterns combine basic language features to solve coding problems in an extensible way. In functional Scala, we solve those coding problems with functions, combinators, and type-classes, so design patterns are less relevant. Actor design patterns combine basic features of the actors to solve coding problems in an extensible way. Arrowised functional reactive programming (based on languages like Scala and Haskell also offers a way to solve those coding problem using functions, combinators, and type-classes. This talk describes a prototype implementation of AFRP and its primitive types and functions, discusses its similarities to actors, and then describes how some actor design patterns in the existing literature corresponds to constructions of AFRP.

About Speaker

  • Diego E. Alonso

Exploring Scala Tooling ecosystem

at TBD

We are going to explore and compare some build tools with special focus on LSP/BSP implementations, IDEs and text editor support. To help the audience’s judgement about the tools that are suitable for their particular needs this talk aims to get attendees familiar with terms like SemanticDB, Metals, Bloop, SBT, Pants, Bazel, Ensime, IntelliJ IDE, Scala IDE, Dotty IDE and other honorific mentions.

About Speaker

  • Jeferson David Ossa

I am a software engineer living in Medellin, Colombia. Scala and distributed systems enthusiast interested in FP, software architecture and infrastructure. Scuba diver wannabe.

Want to Diversify the Scala Community? Here is How You Can Help!

at TBD

The Scala community has grown significantly over the past 15 years. As a community, we wrote millions of lines of code and developed hundreds of projects. While the language is thriving, there is still room to contribute to the community. Different from other tech talks, this talk focuses on contributing to the diversity aspect of the community. It explains the significance and benefits of diversity, and it proposes solutions to diversify and improve the community. One of the best ways to grow the community and to bring diversity into the community is to organize ScalaBridge workshops, which are intended to provide resources for people from underrepresented populations to learn Scala. (Diversity comes in many forms: race, gender, age, religion, culture, sexual orientation, socioeconomic background, etc.) While the workshops have positive and lasting impacts, it cannot be done by one individual or by a single organization. In order for the Scala community to become more diverse, we need your help to scale up! Attend this talk to learn about how to contribute to our community!

About Speaker

  • Yifan Xing

Yifan is a software engineer, ScalaBridge organizer, and open-source contributor. Her work involves many distributed systems related topics, including network protocols, consensus, network security, etc. Yifan contributed to the message queue systems and asynchronous APIs for a Scala open source project Shared Health Research Information Network (SHRINE) at Harvard Medical School. The system uses concepts of parallel processing/multi-threading, non-blocking asynchronous, distributed systems, etc.

Sponsors

If you would like to talk to us about sponsorship options, please get in touch:

Become a sponsor