Programming Languages Journal

Foreword

I have come to a point in my Haskell journey where I should start learning about other programming languages (PL) fields. Towards the end of my FP journal, I started diving into Category Theory and formal verifications, endeavours that shouldn’t be documented in a “FP Journal”. As such, I’ve decided to start a PL journal, documenting all of my PL ventures. Unlike the previous journal, I do not plan to elaborate on the concepts I made sense of, as these elaborations often turn into word rambles in the moment.

June

28th

Understanding the relationships between LTL (Linear Temporal Logic), Haskell, model-checkers, and proof assistants. Conclusion: TLA+ (model checker) can be used to model LTL statements and verify them. There exists LTL libraries in Haskell but they appear to be more data modelling purposes.

29th

• Chris (from work) sent me two papers:
  • Runtime Verification for LTL and TLTL
  • Alternating Automata and Program Verification These papers supposedly describe how LTL statements can really be translated (down?) to a FSM (Finite State Machine). From there, any language can be used to implement this FSM (since a simple FSM is just a while loop + switch statements). I will zoom in on these tomorrow.
• Watched a video on linear logic. Everyday I’m hearing 5 new jargons, at the end of this week I ought to layout a taxonomy of the topics.

July

1st to 14th

• Read the first 10 pages of the Lamport’s TLA paper that covers TLA motivation and semantics.
• Watched the first lecture of RWTH Aachen University’s Model Checking course.
• Talked to ChatGPT a lot to derive a taxonomy of formal verifications technique. Lectures do better jobs covering these types of information though — ChatGPT don’t really come up with memorable sayings.
• Came across Linear Types, didn’t understand much.
• Submitted my first paper ever (it’s on program analysis) to SCAM’23! I can reveal more if it gets accepted.
• Read the intro of Pierce’s Software Foundations.
• Read the first two chapter of Pierce’s TAPL — currently, I don’t find type theory as interesting as formal verifications. Though, I do believe that enjoyment is a linear combinations of the interestingness of the topic’s pure abstractions, the topic’s applicability, and one’s current understanding of the field. When it comes to type theory, I don’t have any of these.

15th to 19th

• Read the docs of the servant library thoroughly: It’s the first library I encountered that uses DataKinds.
• Read up on the expression problem (encountered through servant’s paper). Supposedly, Object Algebras of OOP or advanced Haskell type features can address it.
• Going back to reading Milewski’s Category Theory for Programmers because I should be knowing what Kelsili Arrow and natural transformations are at this point.
  • Finished Chapter 3. Interesting idea: Think of functions in their uncurried form more. If I think of mappend as m -> (m -> m), I can see it as a mapping between an element of a monoid set to a function acting on that set!

Week 4

• Listened to two episodes of the Haskell Interlude podcast: One with Gabriella Gonzalez, and one with Graham Hutton. Professor Hutton’s honesty and passion was, simply put, inspiring. The also-inspiring Gabriella mentioned two interesting things I’ll look into: Monad Reader and Dhall.
• Listened to Conal Elliot talking about the lost elegance of computation. Unique and poignant philosophy, inspired by Conal’s passion, I ought to read John Backus’s famou 1977 Turing award lecture and read into FRP.
• Read Monad Reader issue 19; learned about the Coroutine monad; I was able to use Iteratee and Generator to successfully implement a basic sketch of a program for work.

August

Week 1

• Spent a weekend in FRP via Heinrich’s guide. Big idea: Behaviors are continous and Events are discrete, but, they can be easily composed and transformed to one another.
• React-banana uses MonadMoment, which is also a MonadFix. I tried reading MonadFix is Time Travel. I only partially understood what’s going on even with after reading another article because I lack a complete understanding of laziness, thunks, and seq, so, I started reading Haskell wikibook’s laziness article.

Week 2

• Finished my internship at TwoSix technologies, looking forward in returning as a formal methods researcher next summer!
• Coming across the following for the first time: Refinement types, cubic type theory, the K framework.
• I want to dedicate my time fully to reading 2 materials: Software Foundations (SF) and the Milewski’s Category Theory handbook, until school begins.
• Finished the Basics chapter of SF’s Logical Foundations (LF) book. Good old functional programming!
• Read Chapter 5-8 of the category theory book. I need to spend some time to gather more examples…