Logical equivalences in Haskell

The blogpost Classical Logic in Haskell established a way to prove equivalences between logical propositions and law of excluded middle by writing intances of Iso for the same propositions wrapped in a newtype. Vladimir’s post contain proofs of some important propositions. I had fun proving them myself. I wanted to continue with some more.

Recently, I did the Logic and Proof course to learn both proof techniques and Lean theorem prover. It was fun. So I picked few propositions from the exercises of the Propositional Logic in Lean chapter to try write equivalence proofs for them.

Below are the propositions as newtypes (their logical notations mentioned as comment) and subsequently the Iso instances to prove their equivalences with Lem. As mentioned in the original blogpost, one nice way to progress here is by taking clues from the type system itself in the form of typed holes.

Let’s set some language pragmas

Required Iso class from the original blogpost put inside a module so that it can be imported for rest of the sections

And now the propositions…

This is an IHaskell Notebook which is pretty cool for above kind of experiments. Much more feature rich than GHCi. I got the inspiration from Vaibhav Sagar who writes all his posts as IHaskell Notebooks.

Retrospecting 2018

This year was mostly uneventful unlike 2017. However, I did do a lot more technical reading - mostly papers and a few books - than previous years. Professionally things changed quite drastically. I am now meant to do mostly research-y things than what used to be half & half with engineering before. Not that I complain, my feelings are on the contrary actually. But this whole new setting at work, both from an operations & vision standpoint, is still clumsy and need more time to shape up well.

I am beginning to focus on the areas of Knowledge Engineering. I want to tie it with fascinating things from Type Systems. I believe their shared foundations in Mathematical Logic will provide interesting things to work on. And my choice of technology to realise any such research will be Haskell, mostly.

So apart from spending most of the time reading papers on the history of knowledge bases, their representation, and reasoning I also tried to get used to logic and proofs. During one such excavation, I landed on a course aptly named Logic and Proof which uses this beautiful language called Lean to write the proofs. Lean, like Haskell, has its roots in Microsoft Research. It, like Agda, is dependently typed language which also provides means to do inductive/automated theorem proving. It was my first foray into the world of computational theorem proving and some serious work with dependent types (I did dabble with Idris but it is better not to talk about that). Working with Lean and learning more about its origins and background type systems research gave me ideas that I believe are relevant to knowledge systems.

With Lean, I digressed heavily into learning dependent types, this time with a larger vision to make them useful for knowledge systems. And hence I got this amazing book called The Little Typer. It provides the necessary foundations for me to relate dependent types, higher-order logic, relational programming, and eventually their role in knowledge systems. I am nowhere close to anything concrete to go after but I am having fun peeling the layers of these seemingly disjoint fields converging together elegantly.

Haskell with its dependent typing tools is nowhere close to things that Lean and Agda could do today. But it’s still amazing how far the current type system could take you. Sandy Maguire’s new book is how I am trying to get my head around all those esoteric corners of Haskell. It’s pretty good.

I also want to mention one other thing that is happening coincidentally and maybe right now I am not able to leverage it to its full extent only coz of my lack of understanding but I am pretty sure it will be something that I will be leaning a lot in future. And that is Edward Kmett’s Twitch videos on his creation of Guanxi. Ed’s videos are highly motivational (for some apparent indescribable reason).

Finally, I also want to highlight that I continued persevering with Nix irrespective of it still not friendly as a package manager in macOS. I realised that there’s no other way, right now, to reading nixpkgs source code to make stuff work properly with Nix especially in macOS. Hopefully, it will improve and I will also do my best towards that goal. But Nix is the future of so-called devops that I believe in and I want it to succeed at all costs.

As my daughter grows up to her 3rd year of existence in 2019, I am hoping her to be a bit more independent and me getting a bit more time off work to try to contribute to some open source Haskell projects. Having a 2-year-old kid around when you are trying to do some focussed programming session is not a happy setting (no offence to any 2-year-olds).

I learnt a lot of new things in 2018 that now I think I have some roadmap for next year to channel my energies on. But none of them is related to Deep Learning, Blockchain, or Microservices unfortunately !!

WC 2018: Final Day: Game of the champions

The Final

Croatia 2 - France 4

It could not have been more engaging and dramatic than what unfolded as one of the best World Cup finals of recent times. The game started with Croatians putting their heart and soul into the game. They created the first scare for France and were relentless in their pursuit to score early. It was first 15-20 minutes of a gripping game of Croatian attack & pressure tactics. Unfortunately French got it past Croatian net for no credit of theirs. Croatian reply by the amazing Perisic was spellbinding. VAR came to the rescue of France as it’s been from their first game. I believe the resulting penalty was the turning point of the game.

The second half belonged to France. They showed their class with superb ball control and creative ball passing. Both Pogba’s and Mbappe’s goals were astounding. They are the signs of a team worthy of being a champion. Croatia, in the end, succumbed due to a bit of bad luck and a better opponent.

As the curtains dropped, I consider this edition of the World Cup to be one of the best of the modern era. It was full of honest surprises and impressive comebacks. But more than ever this World Cup was for those who dared to dream and deliberated on it by having fun rather than for those who either got complacent or were bored with the game.

WC 2018: Day 24: The consolation game

3rd & 4th place game

England 0 - Belgium 2

Belgians came back with their inventive & creative gameplay. It was a treat to watch. England did not change much on playing boring football. It was fantastic watching Hazard & De Bruyne sweating & overcoming clueless English midfield & defence. Hazard, in particular, created more chances than out-of-form Lukaku could handle. Belgium in a way deserved more than the 3rd place. And England needs to find fun in their game to start with.

WC 2018: Day 23: Croatian dream run

Semifinal #2

England 1 - Croatia 2

Ivan Sršen describing the mood as Croatian goalkeeper saved the decisive penalty against Russia in quarterfinal

For a brief moment at least, to me and perhaps to all of us in the bar, it felt as though the war was finally over.

Ivan also talks about the legacy of Croatian football and background of some current Croatian players like Modrić and Lovren. It highlights the significance of Croatian progress in this World Cup.

Football, the so-called beautiful game, only needs a pair of legs and pile of passion. That way it binds people from every stratum of society.

Last night the Croatian players showcased matured & infallible football. It was a gripping game. Barring that superb 4th-minute free-kick, England had nothing to showcase in the whole 120 minutes. The Croatian players, like their coach, had a unique sense of calmness and deep focus. Which led them to dominate England in the whole match. England, as I have earlier mentioned as well, lacked both individual skills & collective playmaking. Their early lead was never meant to stand against the pressing Croatian attack.

Croatia will face a much tougher & skilful opposition in France in the final. They should work on improving their pass accuracy and man-tagging in the back, especially for the speedster Mbappe. But this nail-biting win over England should lift their spirits. They will attempt to cause the unthinkable for their country as they have done with their lives.

WC 2018: Day 22: Les bleus le progrès

Semifinal #1

Belgium 0 - France 1

Kylian Mbappé is a revolution. 4 mins in the match the way he ran from midfield to almost inside the Belgium goal post with the ball set the tone of the rest of the match. It would have been more misery for Belgium if his out of form teammate Giroud would have converted some wonderful passes. Belgium suffered from a lack of interest shown by their centre-forward Lukaku. He hardly kicked the ball in the overall match. Hazard was persistent & De Bruyne tried his best to create chances from the flanks. Second half substitution of Mertens brought some much-needed energy to the team. But they suffered from a similar conundrum that Brazil had against them in the quarterfinal. France after scoring the crucial goal went to a full defensive mode. Which was kind of expected. It was a nice game & I feel bad for the Belgs. This was the best team they could ever have. France on the, on the other hand, is clear if Mbappé maintains his pace & check his cheekiness.

WC 2018: Day 21: The English March

England has the best chance to go for the cup and hosts, unfortunately, had to stop at Quarters.

Sweden 0 - England 2

This English team is playing like a well-oiled machine. Lacking individual skills they rely more on each other & set pieces to deliver. And they are doing that pretty well. They now have clear shot to the finals. And depending on who will stand on the other side if this team play sensibly they might do the unthinkable.

Russia 2 (3) - Croatia 2 (4)

It might be the loudest game of the tournament. Much of that roar was for host nation Russia. Russians did not disappoint at all. It was a game of blistering pace & passion. Croatia, as I had previously pointed out, is playing with all their heart. They have not shown any sign of big tournament chill like many other underdogs. Which make their case against England in semis pretty interesting.

WC 2018: Day 20: South American exodus

It will be again a European crown like last time.

Uruguay 0 - France 2

It was a game of tussle between Uruguayan desperation & French persuasion. Without Cavani, the Uruguayan attack was like an already amputated man losing his last leg. Suarez tried his best to muster a number of chances. But none of his teammates had the vision or talent to work with them. France realised that & made sure they don’t do anything silly on the back. French game had the same fluidity like last time. Mbappe showed some interesting skills both with his legs & drama. However, I felt Uruguayans were not that bewildered by French defence. Which might be enough for Martinez’s jubilant men to easily triumph in the semis.

Brazil 1 - Belgium 2

This was the best match of the tournament so far for me (many consider Belgium’s last match with Japan to be the best). It was a great night of football where teams played to their best with a worthy winner in the end. Brazil’s painstaking efforts to penetrate Belgium defence was a treat to watch. Also quite heartbreaking. Belgium’s superb tactic to make De Bruyne play from the centre with Lukaku in the flanks split wide open Brazilian defence. Lukaku was unstoppable & Hazard was critical. But I would say the real hero of the match was Courtois. His gravity-defying saves took the match away from Brazil.

Tite’s plan to not start with Firmino again might be a bad move. He along with Costa made quite an impression in the second half. However, I felt Brazil lacks a physically strong attacking player who could withstand the pushing & shoving to rush inside a stubborn defence. Current talents like Neymar & Coutinho are too feeble to make their way in & hence spend most of the time strolling around the penalty circle. Brazil also missed some straightforward chances which are a criminal offence in the World Cup. Brazil did not disappoint like last time. I wish they progress further next time in Qatar.

In the meantime, I am betting on Belgium as champions.

WC 2018: Day 19: Boring drama

Knockouts Day 3

Sweeden & Switzerland should be banned for playing the most boring game of the World Cup. And England narrowly missed their exit.

Columbia 1 (3) - England 1 (4)

Watching English players on the field is like watching a Twitch stream of someone playing the latest version of EA Sports’ FIFA. Their gameplay and style were so mechanical that it bored me to death. Columbians, on the other hand, showed exquisite legwork whenever they found time after doing those unnecessary pushing, shoving, and play-acting drama. The game was more of reality tv than a real sport. I pity the referee who should avoid travelling to South America anytime soon. England’s path till finals henceforth is easy (assuming Croatia don’t panic against Russia and then get beaten by the English luck). Also, their next game should be called off by sending Sweeden home for wasting the time of thousands of spectators with the most dreadful game of the tournament against Switzerland.

WC 2018: Day 18: A new found calmness

Knockouts Day 3

Brazilians behaved like monks and Belgians got exposed.

Mexico 0 - Brazil 2

This Brazil is a completely different team. They are composed, methodical, and introverted. But the most striking feature is the unusual calmness in their game. They controlled the flow of the entire game. The whole game appeared to follow a rhythm of sleepy progress, a sudden burst of energy, and quick settling back to the earlier state of nirvana. But the Selecaos never lost track of their main agenda ever. Neymar continued leveraging his rediscovered form from the last game. But the real star of this game was Wilson. He suddenly got woke in the second half and decided to do the work for everyone else. And he did deliver pretty well. In the end, it seemed the game got over a bit early. I was hoping for them to continue the wonderful legwork for some more time.

Brazil’s next challenge against the mighty Belgians would be their toughest. Last minute luck favoured Belgium against Japan but the game raised pressing questions on their invincibility. Hope Tete and his team are studying them well.