The tropical semiring is given by (R U {*}, +, 0, min , *) with the underlying set the reals with infinity (written here as *). If we take max instead of min, and take negative infinity as its identity we get a max plus algebra. In this case I'm going to restrict us to the regular old natural numbers, as all sizes of things are whole, and take 0 instead of negative infinity (so it is not much like a tropical semiring at all, but this was the source of my thought process). The morphism of algebraic types into this algebraic structure is straightforward- for every primitive type we have some natural number of bytes, or words, or bits, or whatever we want to measure (holes?), and for types M and N, size(NxM) = size(N)+size(M), size(N+M) = max(size(N), size(M)) as they are represented in C. Assuming a Void type, size(Void) = 0, which works okay, and for a Unit type size(Unit) = 1.
Pointers in C are all represented by the same size thing, so there doesn't seem to be a need to have a star operator in this structure. Instead, I suppose we can just embed all pointer types as primitives, or just specify that the star operator in the type system acts specially with respect to the size morphism.
This is pretty trivial (and probably wrong), but I wanted to record it as I like to think about the shapes of things and the properties of shapes.
No comments:
Post a Comment