Theory of category

Summary

This post is based on “A pragmatic introduction to category theory” talk where were presented definitions of the most used term from theory category defined from the pragmatic perspective. I encourage all of you to watch slides or presentation.

Why should we bother at all?

Category theory gives us a more in-depth understanding of our code. Precisely it gives us information about how things compose together. We reason by composition and abstraction.

Defined terms of `Theory of category` in this talk

  • What is the category?

It is transformation from one object to another A->B

  • The most used category’s rules
    • Identity law
    • Composition Low: ability to combine transformation
    • Associativity: operations can be grouped arbitrarily
  • monoid = category with 1 object

It meets following rules:
Identity : n o id == id o n == n
Composition : forall x, y => x o y
Associativity : x o (y o z) == (x o y) o z

  • functor = category in a box (e.g. Option from F#, Future from Scala, Try, List, Either) where box means that values are lifted to some context.

It meets following rules:

Identity : map(id) == id
Composition : map(g o f) == map(g) o map(f)
Associativity: map(h o g) o map(f) == map(h) o map(g o f)
*applicative = combine more boxes into one

  • monad = fuse two boxes together = it is a monoid in the category of endofunctors

References

Abstract abstracting machines

Its summary of the keynote: “Winning the War on Error: Solving the Halting Problem and Curing Cancer”.

What can you learn?

This talk can inspire you to learn more computer science. You can use programming knowledge to solve changes in curing cancer. The presenter showed how well-known problem like halt problem could inspire to solve some issues in IT world and also solve detection of a wrong genome.

Halt problem

The halting problem is a problem which tries to answer the question: is possible to say when or if executing program has ended? Alan Turing said about it:

Thou shalt not write an algorithm which determines whether a program halts

We can’t solve this problem at all, but we can approximate some solutions and give an answer in some cases. For all unknow cases we can just say “don’t know”. To provide some partial answer, we will abstract abstracting machines.

Software engineer and predictions

The real engineer should use predictions for his design. Do we do such stuff? Matt complained about it.

He showed how he used predictions to approximate programs. He needed to find malware software for the custom Android marketplace which was installed on soldiers devices. He suggested measuring the state of a program (using static analysis) and tried to answer (partially) the halting problem with an approximation. So he suggested to write it down like:

f(program)={halt problem}
f^(program)={halt problem; dunno}

The main idea is to pass program to the Interpreter then to AAM (abstract abstracting machine) and then to Approximator (Static analysers allow programmers to bound and predict the behaviour of software without ever running it.).

What’s needed to create AAM:

  • Injection function = transform program to some state
  • Step function = change state to new state
  • Approximation of execution (guarantee to stop at some point)
  • The abstracted state corresponds to some real state

He described the state of each program using CESK (Control Environment Store Kontinuation).

The CESK machine is a state-machine in which each state has four components: a (C)ontrol component, an (E)nvironment, a (S)tore and a (K)ontinuation. One might imagine these respectively as the instruction pointer, the local variables, the heap and the stack.

Writing these things to more mathematics it will be something like this:

AAM

In bold I wrote things which he needed to approximate to achieve bounded context. After all, this transformation, it is possible to determine and predict: is program well behaving.

Genome analogy to abstracting abstract machines

What is cancer? Cancer is many rare diseases. Finding the same two cancers is hard. The problem which we need to face is curing rare diseases.

Matt found the analogy of software program to biology program:

  • DNA is a collection of characters (char*) which  can accept 4 characters `A` `T“C` `G`
  • DNA is encoding RNA
  • RNA is encoding proteins
  • many proteins are enzymes (Enzymes are functions which catalyse transformation)

From that, we conclude that genome has

  • syntax
  • semantics

So we can use this analogy to build AAM and detect which part of genome fails and mutate in wrong way. Matt Might has invented some algorithm to counteract some mutations.

Real life

He used described a method to find his son disease. He discovered that his son suffers from NGLY1 mutation. What was interesting the medicament which reverts was easy to buy. He tried the medicament on himself and after that, he gave it to his son and he cured him.

In that time, President Obama would like to create the precision medicine program. And he invited Matt to build a genetic telescope and try to build customise drug to diseases. They made assumptions to try cure 5 genetic diseases in 12 months, and they managed to do it. Currently, after changes in US Matt started to create a private clinic and he will develop his project.

References:

CodeMesh 2017

Summary

I was on 8-9 November in London on the conference “Code Mesh”. It was a tough and very interesting conference about non-mainstream technologies. The knowledge which was presented is not something which you can directly implement into your daily work because we don’t have ideas available in our C# language. But each knowledge, in my perspective, should inspire you to do interesting stuff and we shouldn’t close just to one language. I will describe the most interesting talks.

Topics which you can inspire or interest you:

I will describe the other two topics in a short time (mrugnięcie)