[TYPES] A Paper: "Type System as Homomorphism between Monoids"

[xieyuheng]

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.