Podcasts about gradual typing

It's the Season 10 finale of the Elixir Wizards podcast! José Valim, Guillaume Duboc, and Giuseppe Castagna join Wizards Owen Bickford and Dan Ivovich to dive into the prospect of types in the Elixir programming language! They break down their research on set-theoretical typing and highlight their goal of creating a type system that supports as many Elixir idioms as possible while balancing simplicity and pragmatism. José, Guillaume, and Giuseppe talk about what initially sparked this project, the challenges in bringing types to Elixir, and the benefits that the Elixir community can expect from this exciting work. Guillaume's formalization and Giuseppe's "cutting-edge research" balance José's pragmatism and "Guardian of Orthodoxy" role. Decades of theory meet the needs of a living language, with open challenges like multi-process typing ahead. They come together with a shared joy of problem-solving that will accelerate Elixir's continued growth. Key Topics Discussed in this Episode: Adding type safety to Elixir through set theoretical typing How the team chose a type system that supports as many Elixir idioms as possible Balancing simplicity and pragmatism in type system design Addressing challenges like typing maps, pattern matching, and guards The tradeoffs between Dialyzer and making types part of the core language Advantages of typing for catching bugs, documentation, and tooling The differences between typing in the Gleam programming language vs. Elixir The possibility of type inference in a set-theoretic type system The history and development of set-theoretic types over 20 years Gradual typing techniques for integrating typed and untyped code How José and Giuseppe initially connected through research papers Using types as a form of "mechanized documentation" The risks and tradeoffs of choosing syntax Cheers to another decade of Elixir! A big thanks to this season's guests and all the listeners! Links and Resources Mentioned in this Episode: Bringing Types to Elixir | Guillaume Duboc & Giuseppe Castagna | ElixirConf EU 2023 (https://youtu.be/gJJH7a2J9O8) Keynote: Celebrating the 10 Years of Elixir | José Valim | ElixirConf EU 2022 (https://youtu.be/Jf5Hsa1KOc8) OCaml industrial-strength functional programming https://ocaml.org/ ℂDuce: a language for transformation of XML documents http://www.cduce.org/ Ballerina coding language https://ballerina.io/ Luau coding language https://luau-lang.org/ Gleam type language https://gleam.run/ "The Design Principles of the Elixir Type System" (https://www.irif.fr/_media/users/gduboc/elixir-types.pdf) by G. Castagna, G. Duboc, and J. Valim "A Gradual Type System for Elixir" (https://dlnext.acm.org/doi/abs/10.1145/3427081.3427084) by M. Cassola, A. Talagorria, A. Pardo, and M. Viera "Programming with union, intersection, and negation types" (https://www.irif.fr/~gc/papers/set-theoretic-types-2022.pdf), by Giuseppe Castagna "Covariance and Contravariance: a fresh look at an old issue (a primer in advanced type systems for learning functional programmers)" (https://www.irif.fr/~gc/papers/covcon-again.pdf) by Giuseppe Castagna "A reckless introduction to Hindley-Milner type inference" (https://www.lesswrong.com/posts/vTS8K4NBSi9iyCrPo/a-reckless-introduction-to-hindley-milner-type-inference) Special Guests: Giuseppe Castagna, Guillaume Duboc, and José Valim.

Python is a technology and community built upon the goodwill and volunteer time of 1,000s of contributors from the core devs inside CPython to the authors of 100,000s of external packages on PyPI. Until recently, the only full time folks have been at the PSF doing very important work but that work has been largely outside of CPython the technology. In July, 2021, the PSF created the Python Developer in Residence position. The first person in that role is Łukasz Langa and he's here to tell us how it's going and how it will benefit Python at large. Links from the show Łukasz Langa on twitter: @llanga Black: github.com/psf/black CPython PRs: github.com Weekly reports: lukasz.langa.pl Visionary Sponsors: python.org/psf/sponsorship/sponsors What do you get when you sponsor the PSF?: www.python.org/sponsors/application Brett Canon's PyCascades talk: youtube.com Django fellowship program: djangoproject.com Lukasz's prior episodes: Gradual Typing of Production Applications: talkpython.fm/151 Dive into CPython 3.8 and beyond: talkpython.fm/214 Python Language Summit 2018: talkpython.fm/179 Episode transcripts: talkpython.fm Sponsors Talk Python Training AssemblyAI

See the full show notes for this episode on the website at talkpython.fm/151.

Victor Lanvin (ENS Cachan, France) gives the third talk in the fourth panel, Integrating Static and Dynamic Typing, on the 3rd day of the ICFP conference. Co-written by Giuseppe Castagna (CNRS, University of Paris Diderot). We propose a type system for functional languages with gradual types and set-theoretic type connectives and prove its soundness. In particular, we show how to lift the definition of the domain and result type of an application from non-gradual types to gradual ones and likewise for the subtyping relation. We also show that deciding subtyping for gradual types can be reduced in linear time to deciding subtyping on non-gradual types and that the same holds true for all subtyping-related decision problems that must be solved for type inference. More generally, this work not only enriches gradual type systems with unions and intersections and with the type precision that arise from their use, but also proposes and advocates a new style of gradual types programming where union and intersection types are used by programmers to instruct the system to perform fewer dynamic checks.

Yuu Igarashi (Kyoto University, Japan) gives the second talk in the fourth panel, Integrating Static and Dynamic Typing, on the 3rd day of the ICFP conference. Co-written by Taro Sekiyama (IBM Research, Japan), Atsushi Igarashi (Kyoto University, Japan). We study an extension of gradual typing--a method to integrate dynamic typing and static typing smoothly in a single language--to parametric polymorphism and its theoretical properties, including conservativity of typing and semantics over both statically and dynamically typed languages, type safety, blame-subtyping theorem, and the gradual guarantee--the so-called refined criteria, advocated by Siek et al. We develop System F-G, which is a gradually typed extension of System F with the dynamic type and a new type consistency relation, and translation to a new polymorphic blame calculus System F-C, which is based on previous polymorphic blame calculi by Ahmed et al. The design of System F-G and System F-C, geared to the criteria, is influenced by the distinction between static and gradual type variables, first observed by Garcia and Cimini. This distinction is also useful to execute statically typed code without incurring additional overhead to manage type names as in the prior calculi. We prove that System F-G satisfies most of the criteria: all but the hardest property of the gradual guarantee on semantics. We show that a key conjecture to prove the gradual guarantee leads to the Jack-of-All-Trades property, conjectured as an important property of the polymorphic blame calculus by Ahmed et al.

03:32 - Jeff Morrison Introduction Twitter GitHub Facebook 03:46 - Avik Chaudhuri Introduction Twitter GitHub LinkedIn Facebook 04:27 - Flow @flowtype [GitHub] flow 05:36 - Static Type Checking Dynamic vs Static Type Languages 09:52 - Flow and Unit Testing Jest 12:39 - Gradual Typing 15:07 - Type Inference 17:50 - Keeping Up with New Features in JavaScript Babel 20:49 - Generators 24:46 - Working on Flow 28:27 - Flow vs TypeScript Inference Support Tony Hoare: Null References: The Billion Dollar Mistake 35:41 - Putting the “Java” Back in JavaScript Server/Client Overview Prototyping 45:26 - Flow and the JavaScript Community 46:43 - React Support 48:39 - Documentation gh-pages (link to the docs) IRC Channel for Flow: #flowtype on webchat.freenode.net Picks Nolan Lawson: We have a problem with promises (Aimee) Jim 'N Nick's BBQ Restaurant (Aimee) Frank McSherry: Scalability! But at what COST? (Jamison) Frank McSherry: Bigger data; same laptop (Jamison) Greg Wilson: What We Actually Know About Software Development, and Why We Believe It's True (Jamison) Marron: Time-Travel Debugging for JavaScript/HTML Applications (Jeff) Real World OCaml (Jeff) Muse (Jeff) Shtetl-Optimized (Avik) Chef's Table (Avik)

03:32 - Jeff Morrison Introduction Twitter GitHub Facebook 03:46 - Avik Chaudhuri Introduction Twitter GitHub LinkedIn Facebook 04:27 - Flow @flowtype [GitHub] flow 05:36 - Static Type Checking Dynamic vs Static Type Languages 09:52 - Flow and Unit Testing Jest 12:39 - Gradual Typing 15:07 - Type Inference 17:50 - Keeping Up with New Features in JavaScript Babel 20:49 - Generators 24:46 - Working on Flow 28:27 - Flow vs TypeScript Inference Support Tony Hoare: Null References: The Billion Dollar Mistake 35:41 - Putting the “Java” Back in JavaScript Server/Client Overview Prototyping 45:26 - Flow and the JavaScript Community 46:43 - React Support 48:39 - Documentation gh-pages (link to the docs) IRC Channel for Flow: #flowtype on webchat.freenode.net Picks Nolan Lawson: We have a problem with promises (Aimee) Jim 'N Nick's BBQ Restaurant (Aimee) Frank McSherry: Scalability! But at what COST? (Jamison) Frank McSherry: Bigger data; same laptop (Jamison) Greg Wilson: What We Actually Know About Software Development, and Why We Believe It's True (Jamison) Marron: Time-Travel Debugging for JavaScript/HTML Applications (Jeff) Real World OCaml (Jeff) Muse (Jeff) Shtetl-Optimized (Avik) Chef's Table (Avik)

03:32 - Jeff Morrison Introduction Twitter GitHub Facebook 03:46 - Avik Chaudhuri Introduction Twitter GitHub LinkedIn Facebook 04:27 - Flow @flowtype [GitHub] flow 05:36 - Static Type Checking Dynamic vs Static Type Languages 09:52 - Flow and Unit Testing Jest 12:39 - Gradual Typing 15:07 - Type Inference 17:50 - Keeping Up with New Features in JavaScript Babel 20:49 - Generators 24:46 - Working on Flow 28:27 - Flow vs TypeScript Inference Support Tony Hoare: Null References: The Billion Dollar Mistake 35:41 - Putting the “Java” Back in JavaScript Server/Client Overview Prototyping 45:26 - Flow and the JavaScript Community 46:43 - React Support 48:39 - Documentation gh-pages (link to the docs) IRC Channel for Flow: #flowtype on webchat.freenode.net Picks Nolan Lawson: We have a problem with promises (Aimee) Jim 'N Nick's BBQ Restaurant (Aimee) Frank McSherry: Scalability! But at what COST? (Jamison) Frank McSherry: Bigger data; same laptop (Jamison) Greg Wilson: What We Actually Know About Software Development, and Why We Believe It's True (Jamison) Marron: Time-Travel Debugging for JavaScript/HTML Applications (Jeff) Real World OCaml (Jeff) Muse (Jeff) Shtetl-Optimized (Avik) Chef's Table (Avik)

Larry Wall joins me to talk about Perl 6. Show Notes FOSDEM 2015 - Get ready to party! Perl 6 Parrot VM Pugs - pugscode sorear/niecza Not Quite Perl MoarVM - A VM for NQP and Rakudo Perl 6 rakudo.org | Rakudo Perl 6 Curtis Poe: Perl 6 For Mere Mortals Perl 6 RFC Index Gradual Typing Inline::Perl5 FOSDEM 2015 - Over 9000: The Future of JRuby The Wall Nuthouse #perl6 IRC channel Larry Wall (@TimToady) | Twitter Tim O'Reilly Rosetta Code

Welcome to Illegal Argument Episode 98 - Typed Clojure with Ambrose Bonnaire Sergeant. Links: An Intro to Typed Clojure - Jim Duey The Typed Racket Guide Alms programming language (affine types) Levels of Gradual Typing - part 1, part 1 Chez Scheme flow analysis paper: Flow-Sensitive Type Recovery in Linear-Log Time Sketch of AST types core.typed mailing list People: Ambrose Bonnaire Sergeant - @ambrosebs Brandon Bloom - @BrandonBloom Laurent Petit - @petitlaurent