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.
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.
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…
Great idea for creating educational videos like this!
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.
