In the functional programming world, we rely on languages with type systems that help us write, extend and maintain our software. These type systems, such as the one in Haskell, are based on solid type theory. While we usually and easily see the benefits of having a static type system on simple types such as integers, we might fail to see the benefits of applying the same principles to user-defined data types. Continue reading

# Author Archives: Marko Dimjašević

# Boeing and Deaths due to Software Bugs

The IT field has been aware for decades that software can kill people and so we are witness of this fact again with Boeing and its two airplanes 737 Max crashing and killing everyone on board due to erroneous software in the accompanying MCAS system. Continue reading

## Notice of AMS: Vladimir Voevodsky

### Status

The American Mathematical Society wrote a memorial notice on Vladimir Voevodsky where, among others, his contributions to type theory are considered.

## Gentle Introduction to Homotopy Type Theory

### Status

If you’re a programmer and you want to understand what is homotopy type theory about, Dan Licata has a talk on the topic.

## Interactive Theorem Proving

### Status

Interactive theorem proving such as one provided by Agda is so empowering. The help provided by the compiler while interactively developing a proof is invaluable. Types guide you to a solution at every single step.

# Giving a Talk on Propositions as Types

On Tuesday, March 26, I’ll be giving a talk on propositions as types to the Lambda Zagreb Meetup group. The talk will be in Croatian and it is titled *¬ sve za ∀ (no ∃ uvod u propozicije kao tipove)*, which can be translated as *¬ everything is for ∀ (but there ∃ an introduction to propositions as types)*. Obviously, I incorporated logic operators into the title with the goal to make it catchy and to attract more audience with an unusual title. Given that only about 10 people RSVPed so far and that there are only three days left until the talk, it looks like I’ve achieved quite the opposite!

## Web Page is Back

### Status

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.