The Haskell Unfolder Episode 3: injectivity

An explanation of how parameterized datatypes are injective in Haskell while type families are not, and how to use injective type families.

In this episode, we will discuss in what way parameterised datatypes are injective and type families are not. For this episode, we assume familiarity with Haskell fundamentals, in particular datatypes. Knowledge of type families is certainly helpful, but not required. Resources: - Repository where the code will be made available after the episode: github.com/well-typed/unfolder - Paper: "Injective Type Families", Jan Stolarek, Simon Peyton Jones, Richard Eisenberg, Haskell Symposium 2015, microsoft.com/en-us/research/wp-content/uploads/2016/07/inje… If you are interested in the topics discussed in this episode, Well-Typed offers a course on Haskell's / GHC's type system (as well as other courses). well-typed.com/training_type_system/ 00:00 - Introduction 00:42 - Title sequence 00:58 - Definition of injectivity and examples 03:17 - Injectivity of parameterised Haskell datatypes 05:01 - Proxy 06:13 - Example where ambiguity can arise 10:08 - Example where injectivity is essential 11:55 - Switching to a type family 15:27 - AllowAmbiguousTypes 18:09 - Explicit type applications 20:08 - Using proxy to direct the type checker 21:04 - Why proxies are better than plain explicit type applications 22:43 - Revisiting the Encryption example from Episode 2 26:00 - Injectivity annotations / type family dependencies 28:58 - Questions 31:18 - Defining your own (partial) inverse 33:40 - End