Material for Learning GADT

I like the example in the GHC manual. It's simple, and it illustrates some key points:

GADTs let you use Haskell's type system to model the type system of a language you're implementing (the "object language")
This allows Haskell's static checking to assert that your "compiler passes" or what-not are type preserving. Functions taking object-language terms can assume those terms are well-typed. Functions returning object-language terms are required to produce well-typed terms.
Pattern matching a GADT constructor causes type refinement. eval has type Term a -> a overall, but the right-hand side for eval (Lit i) has type Int, because the left-hand constructor had type Term Int.
The Haskell system doesn't care what types you give your GADT constructors. We could just as easily make every constructor in data Term a give a result of type Term a, or Term Bool, and the data definition would still go through. But we wouldn't be able to write eval :: Term a -> a. You choose the GADT "tag types" to model your problem, so that the useful functions you want to write are well-typed.

I was about to recommend it, too. ;-)

Heinrich Apfelmus 2010-10-26 08:16:20

I highly recommend that video for someone starting out with GADTs.

Yitz 2010-10-26 08:16:34

Does anybody have a transcript? I suppose I am not the only kind of person who is more comfortable and faster reading rather than listening/watching.

jetxee 2010-10-26 13:07:30

@jetxee You are the test subject I was looking for! ;-) I have uploaded both a video and a transcript (sorta). I'd love to get feedback on which one you prefer and why; and also what you think of the subsequent [video/slideshow hybrid](http://apfelmus.nfshost.com/blog/2010/07/02-fixed-points-video.html).

Heinrich Apfelmus 2010-10-26 19:54:35

I just watched the video. I much preferred the video version. I read very fast, but having things written out more slowly with the audio, forces me to slow down and digest the concepts appropriately. Thank you, M.S., for the question, and Apfelmus, for the video tutorial. I finally understand GADTs and Phantom Types...

mayahustle 2010-10-26 20:41:51

@Apfelmus I switched off the audio after the second slide, when I wanted a pause (and also because I am not alone in the room, and don't want to put on the headphones). Even with hand-written scribbles and strange jumpy scrolling I find it more convenient to read. Going back as in video is worse than PageUp or scroll with text (positioning is less precise and predictable, requires more complex movement). Also, for me, as a foreign speaker, it's easier to read than to comprehend a random accent (yours is OK, but people speak differently).

jetxee 2010-10-26 22:28:02

@Apfelmus I also quickly looked at GADT text. Mostly reading only code blocks, going back to explanations before them when necessary, and skipping to the header of the next section when I thought I understood the idea. Paid some more attention to the Summary. With video I cannot jump to the next subsection, I cannot see where the next section begins, and cannot tell in the first 2 seconds what this section is about. My patience lasted 35 seconds (more than enough to read 5 words on the screen).

jetxee 2010-10-26 22:38:42

@jetxee. Thanks a lot for your detailed comments! I agree that video is really bad when it comes to navigation and random access. Therefore, I'm trying to find a format that gives the best of both worlds. I would be delighted if you could take a look at my subsequent [video/slideshow hybrid experiment about the fixed point combinator](http://apfelmus.nfshost.com/blog/2010/07/02-fixed-points-video.html) and tell me your thoughts.

Heinrich Apfelmus 2010-10-27 12:06:35

@Apfelmus My first comment was about the fixed point hybrid. The second one was about the GADT tutorial. I didn't notice at first that I can go forward and back with arrow keys (nice!), and used the mouse (to drag the slider, didn't like scrolling this way). The are some issues, but, anyway, it is better than just a video. As you see from the comments, some people are happier with audio and video explanations than with the written text or graphics. For me sitting 10-20 minutes and watching the video is just against my learning habits (and I don't own a TV).

jetxee 2010-10-27 13:02:57

@Apfelmus The issues with the hybrid I noticed, are: 1) when I start browsing through the slides, at some point in the middle the slider jumps back to the first slide sometimes (did something finish loading? Chromium 6.0.472.62); 2) I am more used to see the new page every time, rather than a half-page jump; it takes some time to understand that I've seen half of the slide already, because the scrolling is not continuous; 3) reading hand-written scribbles is difficult. Overall a good format, but I preferred it without audio.

jetxee 2010-10-27 13:12:16

@jetxee. Ah, ok, that was for both videos. Again, thanks a lot for your feedback! The half-page jump 2) is indeed annoying; I'm currently writing a software tool for making video-slideshows that will help me avoid this problem. By the way, my reason for including audio/video instead of just text is that there are many valuable things that text can't convey, for instance seeing the lecturer thinking live or making mistakes; and some explanations, especially about mathematics, are extremely difficult to do well in text, while being very easy to do on the blackboard.

Heinrich Apfelmus 2010-10-27 19:42:17

ansaurus

tags:

views:

answers:

Material for Learning GADT

related questions