Wadler's Blog

Thank you for posting these. I appreciate the extra treat. I enjoyed your two StrangeLoop 2015 talks a great deal. They were fun, I learned a lot, and some things I knew are now better organized in my head.

I also enjoyed the discussion you had with Matthias Felleisen at RacketCon. Maybe you are both right. I recently did a project with ensembles of tropical cyclone tracks that was successful but made me think of both of you. I'll rewrite the Racket code in Typed Racket and Haskell to clean things up and gain more insight. Typed Racket before Haskell because Prabhakar Ragde asked me a question as I was starting that I still need to answer. Your discussion about how we get started, how we frame things from the beginning is important. I think we strive to end up where you are, everything beautiful and fun, simple but not simpler, but the paths we take to get there are many and interesting, including our mistakes.
 

Forgive me if it seems obvious, but I noticed that quotation seems similar to monads in Haskell. There's lifting vs. return, run vs. do, normalisation vs. >>= or join (fmap...) which is like flattening... I suppose the connection is that monads are 'models of computation', and quoting is like having a mini model of computation embedded in the host language.
 

Quotation does bear a resemblance to monads, but it is not precise. Via propositions-as-types, both quotation and monads correspond to modal logics, but they are two different modal logics. See Davies and Pfenning for correspondence of quotation to a modal logic, and Benton, Bierman, and de Paiva for correspondence of monads to another modal logic.