[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Link to the paper: https://urldefense.com/v3/__https://readonly.link/articles/xieyuheng/xieyuheng/-/papers/publish/type-system-as-homomorphism-between-monoids.md__;!!IBzWLUs!QDKONs89nYQk1pdWyJwpctfD9aMo_yPCUbkQ-U-7OiW42F8IB6h8ki4UXNfwRoD7DT2XmvxPBKuSGjxmf2FykWdZHg$ **Abstract** We demonstrate how to view a type system as a homomorphism between two monoids, where the space of types is monoid, the space of terms is also a monoid, and the homomorphism is the `infer` function of the type system. We use a concrete example to demonstrate this idea, in our example the space of types is _linear logic propositions_, and the space of terms is a _concatenative programming language_ (like Forth and Joy). Some key points of our demonstration: - Negation of linear logic should NOT be interpreted as "implying false", but be interpreted as a type of _linear assignment_ (thus constructive). - Linear logic additive connectives can be interpreted without concurrency. - Type errors will be captured by a special `Error` element.