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!
amara.org/v/HblS/

[@AlexBerg1]

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.

[@YestinHarrison]

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

[@edvardm4348]

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

[@robertpeszek6892]

Very nice tutorial, Thank you!

[@haskelltype4627]

Superb tutor!

[@micknamens8659]

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

[@pewpewpew8613]

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.

[@philnguyen0112]

It's an idea that's natural to people who are used to theorem proving, but not obvious to most programmers. The idea is that here you can't just pass in an arbitrary number, because you don't know what type the element at that index is, or if it even exists. So here you pass a "witness" (of type Elem ts t) that you know there's an element of type (t) in the list of type (HList ts). The structure of the type (Elem ts t) is similar to unary Natural number (e.g. N ::= Z | S N), but richer, encoding the inductive definition of what it means to know that an element is in the list.

[@EchoNolan]

Please mic the audience next time :)

[@polypus74]

+Echo Nolan with headphones they are audible, just

[@realYuanW]

the repo github.com/goldfirere/glambda