I’m having trouble finishing a post I was trying to write about teaching and how I think, in academia, we sometimes select against traits that are important to being an effective teacher so I think instead I’ll try to brain dump about the various things going on in my head right now in no particular order.
I’ve read the first couple of chapters of Simon Marlow’s book on concurrent and parallel programming in Haskell (well, I suppose more accurately with GHC). It’s cute and well-written. I don’t particularly have a use-case for what I’d use this for, but it’s one of those things I’m reading for my own edification. One observation I do have is that once you’re dealing with things like the Eval monad it starts being quite obvious the nice abstraction ability you get from laziness + an algebraic sequencing abstraction such as monads. The fact that you can separate out a computation from the way it’s evaluated in such a clean manner is just gorgeous.
I’ve been also reading, on and off, the book Let Over Lambda which is about advanced macro use in Common Lisp. I’m only through the first few chapters and, again, I don’t have a particular project that I’m trying to work on using Common Lisp let alone macro hackery but it’s one of those things I just wanted to read about to expand my horizons. Common Lisp was one of the first languages I learned, the first after the imperative hell that was C++ and Fortran 77, although I never really became that proficient in it. Most of my programming experience is in Haskell. Code that generates code has a certain conceptual appeal to me, which is why I’m going back to relearning macro techniques. When I was first learning Haskell, I oft heard the claim that laziness gives you 90% of the power of macros because of the ability to manipulate control flow. I figured why not actually check that claim out myself for once?
On the reading front, I’m also rereading chapters of the HoTT book and formalizing what I can on my own in Agda just to get more familiar with the techniques involved. This past week I also read these papers, which were both pretty easy to read and had cute results. This might be a silly thought, but while HoTT represents a type theory that describes synthetic homotopy theory I’m really interested in what a type theory that describes synthetic geometry would look like. I full admit that it’s my own bias since I cut my teeth first in differential geometry many years ago. On my first read/skim through of the HoTT book I never actually read the chapter on the real numbers, so I’m trying to work back up to that. If you can deal with reals, then maybe you can define the structure of differentiable manifolds in a non-wrenched way within the type theory? Has anyone already done that? I wouldn’t even dream of trying to do diff geo in ordinary intensional type theory because my gut tells me that defining concepts such as smooth functions and diffeomorphisms would just be too painful.
I’m trying to get better about both blogging and organizing my life. I’m still relying heavily on org-mode and beeminder. I’m trying to get more of my week planned in the org-mode agenda view, giving myself permission to move things around when an unpleasant surprise has robbed me of my sanity points. I figure taking the few minutes to adjust my schedule is better than just flailing wildly and dropping all of the tasks I was trying to juggle, right? I’m thinking I’ll also try to crib code from Sacha Chua for making weekly reviews in order to try and analyze how I’m really doing each week in meeting my goals and maybe figuring out what works with, y’know, data rather than just gut feelings and perceptions. I can’t really trust my perceptions since the way my brain works I can have a ridiculously productive couple of days but I’ll think it happened a long time ago and it skews my sense of things. Recording data on how I’m spending my time and what I get done might help significantly with that. I feel pretty confidant about that assertion because I’ve seen the effect happen a bit already just from having beeminder and seeing the numbers go up in my word count or blog goals.
How about research-y things? Oh gracious, I have this backlog of ideas and partially written up results that I still haven’t gotten published and I’m trying to fix that over the next few weeks until I start teaching again. My goal for September is to write 500 words a day on drafts of papers. That’s a reasonable amount per day, but that’s 15k words by the end of the month which is roughly 50-60 pages . On my “good” days I can do about 2-3k words of technical writing, which if I average that out with allowing myself to have some days where I don’t write and days when I’m just a mess, then I think it’s going to both be a realistic goal that I can stick too and let me clear out some of my backlog. I might make a second beeminder goal just for this and delete it when september is done, manually syncing it with my normal wordcount goal. There are two ideas that are in their early stages instead of their omigod-clarissa-just-write-the-latex-already:
- exploring what it means to compose indexed monads and making a more rigorous comparison between indexed monads and effects in Idris, which was sparked by a conversation with Bob Atkey on twitter.
- explore if it’s possible to have a closed universe of descriptions with univalence. I’ve seen a bit of relevant material on the topic here but it doesn’t include a descriptions type like in the levitation paper. So I don’t know how descriptions complicate things and if you can get a result for how “reflective” the universe can be before univalence is simply impossible? In any case, it’d be interesting to know. The last time I asked Conor he didn’t know of anyone answering that question.
Okay, so that kinda covers all the things I’ve been thinking about and working on in the past week. When I write it out it seems like there’s at least a decent amount, even though I’ve been an emotional wreck since writing my last post where I admitted to a prior suicide attempt.