Blog

Bad ideas in type theory


Types as sets and subtypes as subsets.  This may be due to confusing usage in mathematical practice where, for example, we often see references to integers as a subset of reals. But in mathematical usage, people generally understand that while real numbers without fractional parts are a subset of the…

Current reading August 2017


Two-way string matching  And an implementation in Musl. The C standard post C11 The Rube-Goldberg approach to fault tolerance in NTPd  which is not worse than PTP fault tolerance but a lot worse than what is done in TimeKeeper. Interesting but naive article about bank accounting and credit/money creation. Meanwhile:

Sorting and groups


I can't find much reference to this in the literature (see Maus for some hints and an interesting paper) , but surely people have looked at sorting as a problem in group theory? Given a sequence $latex s=[x_1\dots x_n] $ say a permutation $latex \pi$ sorts $latex  s$ if and…

Current reading: July 8 2017


Principal type-schemes for functional programs∗ Luis Damas† and Robin Milner First published in POPL ’82: Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, ACM, pp. 207–212 THE PRINCIPAL TYPE-SCHEME OF AN OBJECT IN COMBINATORY LOGIC BY R. HINDLEY Quicksort.  Tiny C - sheer genius! Plan B …

The C standard committee effort to kill C continues


Consider the following code: void f(void) { unsigned char x[1]; /* intentionally uninitialized */ x[0] ^= x[0]; printf("%d\n", x[0]); printf("%d\n", x[0]); return; } In this example, the unsigned char array x is intentionally uninitialized but cannot contain a trap representation because it has a character type. Consequently, the value is both indeterminate and an…

Types considered harmful


Russell introduced what is often viewed as his most original contribution to mathematical logic: his theory of types—which in essence tries to distinguish between sets, sets of sets, etc. by considering them to be of different “types”, and then restricts how they can be combined. I must say that I…