LambdaConf 2015 - A Practical Introduction to Haskell GADTs Richard Eisenberg

A burgeoning Haskeller soon discovers that proper use of descriptive types helps to capture real-world ideas, catches errors, aids in refactoring, speeds development, and indeed makes programming more fun. But, once that Haskeller has drunk the well-typed Kool-Aid, where to go from there? The answer: even more types! A Generalized Algebraic Datatype (GADT), at its core, allows a compiler to make different assumptions about types within different branches of a pattern match. Leveraging this power allows a programmer to encode detailed invariants in a datatype or algorithm and have these invariants checked at compile time. Clever use of GADTs also lets you remove certain uses of unsafeCoerce, as long as these can be proved safe. This workshop will be a hands-on, interactive tutorial on using Haskell GADTs in a practical setting.

Help us caption & translate this video!

[AlexBerg]

So thankful that LambdaConf organizers decided to get confreaks to come to record the sessions. This talk was only helpful to me years after I attended this talk.
Also thankful to this speaker for coming to share his knowledge. So nice.

[edvardm]

Eisenberg is such an amazing Haskell teacher. Really enjoyed his series in @Tweag, hope I could get more of these

[YestinHarrison]

can confirm that in 2024, GHC handles things nicely without complaining about bogus incomplete patterns :)

[micknamens]

It's always frustrating that the questions from the audience are (almost) not audible. Please provide them as subtitles (embedded in the video itself, not (only) in the cc) or as voice-over. Thanks

[pewpewpew]

I absolutely did not understood the second task and this Elem type. I spend couple of hours to understand this type and how it correlates with function get and I failed. But nevertheless, when I opened editor and started writing code I somehow implemented working function get.
Indeed, there is only one way to do this, but even having written a function, I do not fully understand how it works and how in general it was possible to come up with such a thing. To be honest, when I finished this function, I didn't even immediately understand how to use it.
That feeling when you managed to do something, but you don't feel any satisfaction from it.