Skip to content
Hallway
0:00 / 0:00

#haskell#gadts#glambda

LambdaConf 2015 - A Practical Introduction to Haskell GADTs Richard Eisenberg

Confreaks

42K subscribers • 85 videos on Hallway • Conference channel

YouTube
  • Recommended by 1 person: 1 in engineering communities.
  • Presented by Richard Eisenberg

Intermediate. Assumes working knowledge.

20K views10 years ago1 recommendation

Programming languagesHaskellLanguage design and type systems

Richard Eisenberg teaches how to use Generalized Algebraic Datatypes in Haskell to encode invariants and enforce them at compile time.

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/

Why it's here

1 person recommends this

What people say. Highly recommended for learning GADTs, particularly alongside the glambda educational codebase for a deep type-system workout.

u/imalsogregin r/haskell • Recommends

On “What are the best Haskell codebases to learn from?”

I've been getting a lot from glambda, a GADT based lambda calculus, written mostly for education, and accompanied by a link to this video. Grokking it is a real workout!
27View on Reddit

u/Faucelmein r/haskell • Mentions

On “Understanding dynamic-typing facilities in haskell”

> Then I realized that in all the use cases I encoutered up until now, I always needed to read expressions dynamically from user input. There is an example STLC interpreter called glambda (https://github.com/goldfirere/glambda) (video) that takes the approach of parsing user input into an intermediate unchecked representation that is later type-checked into the GADT one. Here is the typechecked expression, here is the unchecked one. Here is the type-checking function. I also seem to remember some comments at LtU about this topic, here and here. But they seem to be mainly about the "finally tagless" approach that doesn't use GADTs.
5View on Reddit

u/Faucelmein r/haskell • Mentions

On “Reminder: Stephanie Weirich will speak tomorrow (Monday) in The Chalmers Online Functional Programming Seminar Series”

If I understood correctly, this talk seems related to the glambda and stitch "intrinsic interpreters" for simply-typed lambda calculus, but goes beyond them to also support System F.
3View on Reddit

u/MorrowM_in r/haskell • Mentions

On “Tying Shoes with GADTs”

I'm curious what you mean exactly. If you mean something like this: data IntExpr = AnInt Int data BoolExpr = ABool Bool data Expr = IntExpr IntExpr | BoolExpr BoolExpr | If BoolExpr Expr Expr Then you can't model something like this: ifNot :: Expr Bool -> Expr a -> Expr a -> Expr a ifNot b x y = If (If b (ABool False) (ABool True)) x y `BoolExpr` can't be a nested `Expr`. Really, it's just a `Bool` in disguise. I highly recommend this talk by Richard Eisenberg and the associated repo, which takes advantage of GADTs in this way.
2View on Reddit