One of the most fundamental notions in type theory is equality. There are various forms of equality, including propositional equality, judgmental equality, typal equality, extensional equality, intensional equality, path equality (a key concept in homotopy type theory), among others. The list goes on, and any deep exploration of the concept of equality could easily expand to book length. Instead of attempting to cover all these notions at once, I believe it’s best to build this blog post incrementally.

Inspired by Satyajit Ray’s Deep Focus—a compulsory reading at FTII Pune and NSD Delhi—I was struck by the depth and nuance with which Ray analyses his favourite films and directors. This led me to finally compile a list of my own 10 (+10) favourite films. However, I soon realised that rather than ranking them purely on cinematic merit, my choices were more personal—a reflection of the life lessons they offer.

Continuing from my Bayes Theorem-based blog post on solving the Monty-Hall problem, I will now show a rather elegant way to model the solution that exploits the humble List monad. To remind the reader, the Monty Hall problem involves a contestant initially choosing one of three doors, hoping to find a car behind it. Monty Hall then opens a different door, revealing a goat, and asks the contestant if they want to switch their initial choice. The goal of the solution is to guide the contestants to make this switching choice such that they have a higher probability of winning. This post was inspired by a less-than 100 lines implementation of a probabilistic programming monad in Haskell

Today, while reading Steven Pinker’s latest book on critical thinking, Rationality, I was scribbling a solution to the Monty Hall problem. The Monty Hall problem is probably one of the most well-studied pop-science problem statement with different intuitive explanations of the solution. In case, dear reader, you have been living under a rock here is the problem statement:

After scouring through the entire web for close to 5 years and giving up out of sheer frustration every time, I was finally able to upload my TeX sources to arXiv (as of 17.01.2024). The solution was buried as a comment to one of the lesser upvoted answers in a less popular StackExchange thread. I hope Google will push this post high up so that it can help Overleaf (and minted) users.

Recently in a private discussion forum, there was a topic under consideration which went something like this:

In pure lambda calculus (untyped or typed) the fix combinator is used to encode recursion. fix represents the least fixed point of a function f i.e the least defined x for which f x = x. An important concept is that a function need not have a least fixed point. But for those functions which do, the least fixed point is the base case for recursion. An intuition about the least fixed point is :

In this post I attempt to summarize my understandings about the transactional nature of Smart contract execution. I conducted this study, while trying to understand the DAO exploit. The basis of the DAO exploit is a recursive(or rather reentrant) message call. One important point to note that an exception(during a message call or otherwise) in the Ethereum Virtual Machine , would imply reverting all changes to state and balance. Solidity has a documentation on cases where exceptions are thrown automatically. However in certain cases like send we need to manually raise an exception using throw. So, the attacker has to be careful not to hit any exceptions while attempting the reentrant call to avoid reverting. I also rectify certain mistaken assumptions, I made in my previous post.

A power set is simply defined as all the subsets of a set.