Question

I'm looking to describe processes in chemical engineering that that transmute some substances into others. Is there a category that describes morphisms that consume "substances"?

Examples of what I would like to model

To give some examples:

A transformation mix that combines two substances into a mixture.

A transformation boil that boils a substance into some byproducts.

A transformation split that separates a substance to be used in 2 different processes according to a pre-defined proportion.

And so on...

Not a function

As you can see, each chemical process is not merely a function, since its goal is not to "compute" a value but to translate some amounts of certain substances into others.

Maybe a Category?

This led me to consider categories which generalize the notion of functions.

class Category cat where -- | the identity morphism id :: cat a a

-- | morphism composition
(.) :: cat b c -> cat a b -> cat a c

Conceptually this works since chemical processes are composable exactly in this way.

More specific Category

I know there are more specific instances of categories that encode more abstractions (e.g., Cartesian categories). A Cartesian category introduces products:

instance PreCartesian Hask (,) where
    fst = Prelude.fst
    snd = Prelude.snd
    diag a = (a,a)
    (f &&& g) a = (f a, g a)

-- alias
class (Monoidal k p i, PreCartesian k p) => Cartesian k p i | k -> p i 
instance (Monoidal k p i, PreCartesian k p) => Cartesian k p i

However, there is an issue. Conceptually, morphisms in Cartesian categories "compute with" rather than "consume" their objects. From the function diag a = (a, a) you can see that it's able to duplicate the object (this is not be possible in chemical engineering).

It seems like most category typeclasses deal with "computation" rather than "consumption".

Consumable Categories?

Are there any categories which describe morphisms that consume their objects? Any useful implementations in Haskell or research papers that I could look for?

Linear logic

Using Curry-Howard, perhaps it's easier to find an equivalent logic first and then map to the category. I stumbled on linear logic which seems to help:

more about linear logic

CodePudding user response：

This could be a nice application of Linear Haskell! GHC 9.0 and newer supports the LinearHaskell, which enable linear functions.

CodePudding user response：

There’s certainly prior art in the use of linear logic for reaction modelling.

If multiple reactants can combine, maybe what you’re looking for is an operad, rather than a category.

Is there any particular reason why multisets don’t suffice as a basic representation?