Educational videos about Haskell and GHC

#1

Is there any demand for educational videos about GHC development, advanced type-level programming, modeling dependent types in Haskell using singleton types, and so on? There are plenty of written resources that cover those topics (blog posts, papers, documentation), but sometimes an explanation just doesn’t click until you see it in action.

Perhaps there is a specific language extension that you would like to see clarified? Or maybe a design pattern, such as encoding existential quantification via universal quantification and continuations? If you have a particular topic in mind that could be covered in 15 minutes or so, it would really help me decide what to make a video about.

11 Likes
#2

I think the answer to your main question is yes, I do believe there is a demand for these kinds of videos. I know that a lot of people prefer blog posts but I’ve always preferred videos and I doubt I’m alone in that. In terms of big picture topics, I would love some kind of introductions to GHC development so that I could work up the confidence to try and make contributions. For more specific suggestions and for type level programming in particular, I think a video version of your type families blog post would be pretty popular.

1 Like
#3

I think Generics is one that can use a video explanation.

Someone should also definitely cover Generics with an imaginary version of Dependent Haskell at some point.

Currently, Generics is a hellscape of instance declarations with no coverage checks. With Dependent Haskell, Generics could very likely have a much simpler interface.

It’s a very powerful way to sell the value of dependent types…

2 Likes
#4

Really missing @rae’s videos, which were doing something like that. The niche is empty and awaits brave souls!

3 Likes
#5

…very brave ones!

#6

Great idea for creating educational videos like this! :+1:

I think it would be really nice to have a short video about solving a real-life problem with ordinary ADTs in an awkward way where there’s no nice way to solve a problem using simple Haskell constructions.

Like, you really want to express that some combinations are not possible but the GHC exhaustiveness checker forces you to handle all of them anyway. And this becomes fragile when you want to refactor code later (e.g. you handled cases with _ and now you added a constructor and GHC doesn’t warn you about handling this case but specifying all the constructors is too much work for some big types or something different).

And then it can be shown how GADTs or singletons can be used to eliminate this problem.

1 Like
#7

yes could use videos about basic usage of mysql, requesting web apis, saving to files, simple monads, simple io, simple tasks

#9

saving to files, […] simple I/O, simple tasks…

A quick search using the term: haskell "I/O" video

…one point to be aware of: these days, most Haskell users avoid using String, with many preferring Text instead.

#10

In depth GADTs as in how coercions are related to GADTs; local equalities

Perhaps an analogy would be how Dictionaries are passed as simple runtime values when they are not specialized. That’s a key idea of type classes.

What would be a key idea in GADTs? What’s the magic behind local equality contraints?

I feel like the type classes + dictionaries are much more widely understood than the GADTs + local equalities

Thanks :slight_smile:

2 Likes