Dependent Types - salvation or plague | Lambda Days 2021

This video was recorded at a pre-conference meet-up of Lambda Days, which took place on 4th February 2021 - www.lambdadays.org/lambdadays...
More great virtual tech conferences - codesync.global
---
Dependent Types - salvation or plague
run by
John Hughes with Stephanie Weirich, Edwin Brady, Adam Chlipala and Thorsten Altenkirch
introduced by Michał Ślaski
ABSTRACT
Does the future belong to dependent types… or not? Are they a cute toy, or the Next Big Thing? Should you be planning to use them in your next project (or the next but ten), and if so, where and how should you start? What are the swings and roundabouts you should be aware of? Our panelists are leading the adoption of dependent types in a variety of programming languages, and have deep insights into how they scale in practice. Join us to learn if dependent types will be a part of your future!
Need a refresher? We’ll be starting at the beginning, but we will be going fast-if you’d like to prepare a little in advance, I recommend watching Thorsten Altenkirch’s video “The power of Π” (from last year’s Lambda Days): • Thorsten Altenkirch - ...
---
THE HOST - John Hughes
John Hughes has been a functional programming enthusiast for more than thirty years, at the Universities of Oxford, Glasgow, and since 1992 Chalmers University in Gothenburg, Sweden. He served on the Haskell design committee, co-chairing the committee for Haskell 98, and is the author of more than 100 papers, including "Why Functional Programming Matters", one of the classics of the area. With Koen Claessen, he created QuickCheck, the most popular testing tool among Haskell programmers, and in 2006 he founded Quviq to commercialise the technology using Erlang. In 2018 he became an ACM Fellow.
THE PANELISTS
Adam Chlipala - Associate Professor of Computer Science, MIT Computer Science & Artificial Intelligence Lab
Edwin Brady - Creator of the Idris programming language, University of St Andrews
Niki Vazou - Research Assistant Professor, IMDEA
Stephanie Weirich - Professor of Computer Science, University of Pennsylvania
Thorsten Altenkirch - Professor of Computer Science, University of Nottingham
---
Lambda Days
Website: www.lambdadays.org
Twitter: / lambdadays

[@neilbedwell7763]

Torsten's contributions are incredibly insightful

[@LilScottyWeaver]

As both a Scala programmer and huge fan of Computerphile, I was super excited to come across this video!

[@saltrocklamp199]

Thanks for this! I used to write a lot of code for machine learning. Arrays that are dependently typed on size would be super useful for writing complicated expressions with matrix and vector manipulation. Also, less-fancy refinement types (e.g. floats/reals that must be in [0,1] and are not allowed to overflow) could be useful too.

[@Turbanawesomeness]

Why wasn't ATS brought up as an example of a high-performance dependently-typed language?

[@bibliusz777]

why are the likes hidden?

[@steven-t-e-shaw]

I see them. They must be back!

[@GeorgWilde]

Hi