Type Inference & Unification - Isaac Elliot - BFPG 2019-03

preview_player
Показать описание

Type systems increase our confidence that code does useful things. Last month we saw how upgrading untyped lambda calculus to simply-typed lambda calculus (STLC) lead to a better-behaved language by ruling out non-termination and nonsensical operations. In this talk I introduce 'type inference', a process that allows us to type-check programs without any type annotations. We will see how it applies to STLC and beyond, and uncover the critical machinery that makes it work: unification.

(New audio system is better than the aircon noise, but I'll fiddle with the mixer next month to get rid of the clipping and hum)
  1. Brisbane Functional Programming Group
  2. Functional Programming
  3. BFPG
  4. PLT
Рекомендации по теме
Applying unification to 0:04:02

Applying unification to type systems

Hindley-Milner Type Inference 0:07:38

Hindley-Milner Type Inference | OCaml Programming | Chapter 9 Video 37

Intuition for Unification 0:07:16

Intuition for Unification | OCaml Programming | Chapter 9 Video 43

Type Inference & 0:43:06

Type Inference & Unification - Isaac Elliot - BFPG 2019-03

Unification Algorithm | 0:06:03

Unification Algorithm | OCaml Programming | Chapter 9 Video 44

A unification algorithm 0:04:55

A unification algorithm for Hindley-Milner types

Polymorphic Types and 0:16:05

Polymorphic Types and Effects with Boolean Unification

Plait Inference 8 0:04:07

Plait Inference 8 - unification

Podcast 4, part 0:12:17

Podcast 4, part 3 Polymorphic type inference unification

An Existential Crisis 0:13:54

An Existential Crisis Resolved: Type Inference for First-Class Existential Types

Lecture on ML 0:31:40

Lecture on ML Type Inference: No.7 Unification Algorithm and its Correctness Proof

[OOPSLA23] Fast and 0:17:42

[OOPSLA23] Fast and Efficient Boolean Unification for Hindley-Milner-Style Type and Effect...

Guillaume Martres—Scala 3, 0:45:02

Guillaume Martres—Scala 3, Type Inference and You!

Scala - Variable 0:05:19

Scala - Variable Type Inference

Hindley-Milner helpers: substitutions, 1:02:42

Hindley-Milner helpers: substitutions, unification, instantiation, generalisation in TypeScript

The Simple Essence 0:14:39

The Simple Essence of Algebraic Subtyping: Principal Type Inference with Subtyping Ma... (ICFP 2020)

Shplait Inference 8 0:04:03

Shplait Inference 8 - unification

Type Inference from 2:29:13

Type Inference from Scratch: A Workshop with Christoph Hegemann

2 09 Unifiers 0:24:09

2 09 Unifiers as Equivalances: Proof Relevant Unification of Dependently Typed Data

Dynamic Type Inference 0:23:13

Dynamic Type Inference for Gradual Hindley–Milner Typing

Sandy Vanderbleek on 0:09:58

Sandy Vanderbleek on Correcting A Widespread Error in Unification Algorithms

Relational Nullable Types 0:14:22

Relational Nullable Types with Boolean Unification

FreezeML - Complete 0:17:00

FreezeML - Complete and Easy Type Inference for First Class Polymorphism

Bidirectional Type Checking 0:41:31

Bidirectional Type Checking

Комментарии
Автор

I am studying for the last exam of my bachelor's which is "programming paradigms". The exam got canceled due to corona. But I got a last minute chance to take it orally on monday so I don't have to stay for a whole additional semester.
In the lecture slides there is this chapter about type inference and I just couldn't make sense of it. Thankfully I found this great talk that uses almost the same syntax as the lecture slides but with an explanation to it. So finally I undestand what the slides have been trying to tell me for the last 24hours :D
Thank you so much, this is saving my ass! :)

WoDNolz
Автор

Thanks for posting. Was this talk in Queensland?

kreshokresimir