After an interruption today, my web page is back online.

# Recording of My Talk at Lambda Days 2019

In February I was at the Lambda Days 2019 conference to give a talk “Function Totality: Abstraction Tool in Programming” and a workshop “Introduction to Dependent Types”. The talk had examples in Haskell and Idris while the workshop was in Agda. Both the talk and the workshop went quite well and I received nice comments for both. I was fortunate to have David Turner and John Hughes at my talk and to have a discussion with them around the topic.

The talk was recorded and if you’re interested in watching it, you can find it available online. Talk slides are available too.

# Insisting on a Three-valued Boolean Type

If your program can have only two legal states, what sense does it make to extend a Boolean type with a third data constructor to account for the possibility of an “illegal program state”? Use a coproduct type with a Boolean type on the right instead. Make illegal program states irrepresentable in your types. I’m baffled by folks that insist on having their three-valued Boolean type.

## Comparison of Type Theory and Set Theory

### Status

If you ever wondered how are types different from sets or more generally what is the difference between type theory and set theory, I recommend watching a talk by Thorsten Altenkirch at Foundations of Mathematics: Univalent Foundations and Set Theory 2016.

## Competing Against Wadler

### Status

I applied to give a theorem proving seminar at a university. They chose Philip Wadler as a lecturer over me. That must have been close! Still, so disappointed…

# Isomorphism and Embedding

To me as a programmer, to write mathematical proofs that are mechanically checked by a computer feels empowering. To have these proofs as executable programs feels even more empowering. Therefore, our proofs have a computational aspect and vice-versa: our programs have a logical aspect. To be able to get an instant feedback while proving a theorem is amazing. With Agda, a dependently typed functional programming language, one can interactively write a proof by getting guidance from Agda as to what is left to prove. Furthermore, Agda checks the correctness of proofs by following a set of rules. Unlike with pen and paper proofs, proofs in Agda are much more rigorous because there is no room for hand-waving nor unwarranted claims for something to be trivial. An uninformed mathematician will likely find this comparison to Agda hard to believe.

## Google and its own Software

### Status

Isn’t it ironic – Google’s own proprietary Meet service isn’t supported in Chromium, a web browser by Google, but it is supported in Firefox, a web browser by Google’s competitor.

# Gave a Talk: Terminating and Productive Functions

At the Lambda Zagreb Meetup this Monday I gave a talk on terminating and productive functions. It was an interesting discussion with questions that tied the topic and examples I had with natural numbers, linear types and communicating systems.

## Giving Talk on Productive and Terminating Functions

### Status

Today I’ll be giving a talk on terminating and productive functions as part of the Lambda Zagreb Meetup group. This talk will be very familiar to my upcoming Lambda Days 2019 talk.

## Structurelessness

### Status

Jo Freeman has an interesting essay on the tyranny of structurelessness. The lack of structure implies the lack of power to act.