Tag : maths

This is the third part of my serie about Haskell and category theory. In the previous post, I described a bit the Hask category and some categorical constructs. The goal of this text is to understand the meaning of a recursive type like List. For that, we will have to understand what is a free algebra and have a quick look at the relationship with monads (for applications look at the blog of sigfpe). But first, I would like to highlight a problem with the category Hask.

In my previous post, I explained that with category theory you can define some concepts in such a way that they can be used in several different contexts. As a side effect, the definitions are rather abstract since they are forbidden from talking about the implementation of the objects and must rely only on the provided interfaces. So, a first thing to do when studying category theory is learning some of these definitions. Some of them are just generalizations of ideas commonly used in set theory.

Before continuing my exploration of the specification and extraction of softwares in Coq, I think I should make a pause and focus a little on Coq basics like the differences between Set and Prop and the meaning of a type like 4>0 ...

If you like maths you'll love this free software : Group explorer. Group Explorer helps you visualize groups, homomorphisms, subgroup lattices, and more. The most common group visualization technique is the multiplication table; nearly every student has seen it and therefore it needs little introduction. Cayley diagrams are a very potent but underused visualization technique, probably because creating them is difficult by hand. Group Explorer makes them easy to view and edit.

This weekend, I wanted to do some experimentations with random number generations and arrays in Haskell. So, I decided to build a small Iterated Function System (IFS) library because it is a quite standard stuff, easy and which can generate some cool pictures. And, it needs random number generation, array and speed.

One month ago I did not know a lot about logic : just truth tables for some connectives. But, for some time I have been having fun with Haskell and it finally convinced me to use some of my spare time to learn about logic. Of course, you can code in Haskell without knowing a lot about logic, the Curry-Howard isomorphism and all that but it is much more fun to code in Haskell if you know a bit about it. So, thanks to my Christmas vacations, and the fact that being French I have long vacations :-), I read a few papers about logic : classical, intuitionistic, modal, linear etc... This post is an attempt to summarize what I think I have understood and I hope it may be useful to other newbies too.