1. 25

Several people previously indicated interest in a type theory reading group. tel gave me a poke about this and we’ve been talking, but it seems better to have the conversation in public. I’m going to throw out some ideas in comments; please upvote, downvote (I won’t mind!) as appropriate, or leave your own suggestions.

  1.  

  2. 6

    I would like to join this, Pierce’s book has been hanging out on my to-read list for some time.

    1. 6

      If you’re interested in participating please make an entry in this form so we can start estimating the size of this group. If you sign up, expect an email as things start to coalesce.

      Thanks! :)

      1. 5

        I’m definitely interested. Not too concerned about what book we read first; inherently people will be at different states of knowledge, and we’ll iterate as needed, and that’s fine. :)

        IRC is definitely a lot easier for me to engage with than a mailing list; there’s less friction. But I’m okay with any modality I guess.

        1. 4

          Which book should we read?

          1. 7

            Types and Programming Languages. Kind of the standard text, comprehensive, has (sketches of) solutions to exercises in back. No free access.

            1. 7

              Bob Harper’s Practical Foundations of Programming Languages is an alternative to TAPL. There is a draft for free online currently (warning, large PDF).

              1. 3

                I’m a fan of PFPL over TAPL, but TAPL might be more popular.

                1. 3

                  I think that’s about right, I have no strong opinions on this though :)

                2. 1

                  Second edition (only!) has exercises, but no solutions.

              2. 4

                What forum is appropriate to have discussions. lobste.rs is probably fine to promote these things but not great for Q&A/discussions of the readings. Standard choice would be a mailing list but maybe there’s a newer, hipper technology that’d be better?

                1. 3

                  I’m kind of promoting putting together a discourse site or even going on reddit (maybe!). The idea of a maybe weekly “book club” thread plus side threads for exercises/specific topics/questions seems nice.

                  I also like Craig’s notion of landing on a “study guide” as a result. Each “book club” thread could have as a goal adding to that study guide (in Hackpad?).

                  1. 2

                    What’s wrong with using irc, where it’s logged and published on a website? Like bash.org

                    Could also embed a web irc client.

                    1. 5

                      I thing direct communication channels (like IRC) can really get messy when you have more people participating in complicated discussions.

                      I like the idea of a mailing list, google groups is a pretty decent solution for that.

                      1. 4

                        IRC could be nice to go alongside the main work, but I think something more organized than an IRC log would be really desirable.

                        1. 2

                          So mailing lists, IRC, and Google Groups are all going to make LaTeX / MathJax a challenge. I’m thinking that’s a must-have feature?

                          1. 3

                            Eh i say just throw discourse up on a small instance. Can still have irc for live chat on freenode as an example.

                          2. 2

                            IRC is ephemeral, active, and poorly archived. I like it, but more permanent and passive ways of conversing may be preferred for this beyond the rough stages.

                        2. 3

                          What’s the best forum or site for this? I’m thinking LaTeX support is a must-have?

                          1. 3

                            We could use Hackpad to build a kind of collaboratively edited annotation or reading guide, but it’s not a good tool for discussions.

                            1. 3

                              We could set up a Discourse server with a LaTeX plug in. Hosted Discourse is stupidly expensive, but you can host it on Digital Ocean for about $10/month.

                              1. 2

                                One option is to use lobste.rs, but no LaTeX, unless we can sell @jcs on that. :)

                                1. 2

                                  MathJax probably wouldn’t be too hard to splice into lobste.rs, but I personally would prefer MathML or images generated somewhere. However, LaTeX in general in lobste.rs seems useful.

                                  And lobste.rs seems like a good place to discuss things, but only one thing at a time (if you get what I’m failing to convey here), and not as ideal as, for example, Discourse would be.

                              2. 3

                                I’ve got the pierce book. I can give 10 hours a week to this project. Let’s do it.

                                1. 3

                                  We should talk format and expectations as well: weekly reading goals, reviews, co-created study guide, forums, chat rooms, meeting times: what do you think produces the best study group?

                                  1. 6

                                    Opinion: each week on person ought to take responsibility for being “the expert” on the chapter. They should feel comfortable fielding questions, guiding discussions, and so on. This “expert” should probably cycle but at the paper club I’m in this prevents weekly meetings where there’s no discussion because no one knows what is happening.

                                    1. 2

                                      We could also reach out to the selected author (who most likely has better things to do, but still, costs nothing to ask!).

                                      1. 2

                                        Oh, that’s nice!

                                      2. 2

                                        Having a regular meeting is definitely a huge motivator for those of us who have trouble dedicating ten hours a week. :) Timezones are going to play a large role in scheduling that, as they always do…

                                      3. 2

                                        Very interested! I filled out the form.

                                        1. 1

                                          I would be interested in this, sounds great.