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…

the terrible effect of Krohn-Rhodes


One of the most interesting theorems in computer science is the Krohn-Rhodes theorem that shows a strong link between basic computer science and group theory. Crudely, the KR theorem extends Jordan-Holder $latex (H_1 \triangleleft H_2 ... \triangleleft H_n=G)$ ┬áto state machines, but it does it in a way that doesn't…