寻找类别对象部分可消耗的类型类（化学工程）

Question

问题

我希望描述化学工程中将某些物质转化为其他物质的过程。是否有一个类别描述消耗“物质”的态射？

我想要建模的示例

举一些例子：

将两种物质组合成混合物的转换混合物。

将物质煮沸成一些副产品的转化沸腾。

一种转换拆分，根据预定义的比例将物质分离以用于 2 个不同的过程。

依此类推...

不是函数

正如您所看到的，每个化学过程不仅仅是一个函数，因为它的目标不是“计算”一个值，而是将一定数量的某些物质转化为其他的。

也许是一个类别？

这让我考虑概括函数概念的类别。

类别类别猫在哪里 --|恒等态射 id :: cat aa

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

从概念上讲，这是可行的，因为化学过程可以完全以这种方式组合。

更具体的类别

我知道有更具体的类别实例可以编码更多的抽象（例如，笛卡尔类别）。笛卡尔类别引入产品：

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

但是，存在一个问题。从概念上讲，笛卡尔范畴中的态射“计算”而不是“消耗”它们的对象。从函数 diag a = (a, a) 中您可以看到它能够复制对象（这在化学工程中是不可能的）。

似乎大多数类别类型类处理“计算”而不是“消耗”。

消耗类别？

是否有任何类别描述消耗其对象的态射？我可以寻找 Haskell 中任何有用的实现或研究论文吗？

线性逻辑

使用 Curry-Howard，也许首先找到等效逻辑然后映射到类别会更容易。我偶然发现了线性逻辑，这似乎有帮助：

有关线性逻辑的更多信息

Answer 1

这可能是 Linear Haskell 的一个很好的应用！ GHC 9.0 及更高版本支持支持线性函数的 LinearHaskell。

Answer 2

使用中肯定有现有技术反应建模的线性逻辑。

如果多种反应物可以组合，也许您正在寻找的是一个操作数，而不是一个类别。

是否有任何特殊原因导致 多重集 不足以作为基本表示？

Answer 3

您的 PreCartesian 类太强大了。您真正想要的类应该仅抽象 对称幺半群类别

class Category k where   id :: k a a
                         (.) :: k b c -> k a b -> k a c
class=>Monoidal k where  attachUnit :: k a (a,())
                         detachUnit :: k (a,()) a
                         regroup :: k (a, (b, c)) ((a, b), c)
                         regroup' :: k ((a, b), c) (a, (b, c))
                         (***) :: k a b -> k α β -> k (a,α) (b,β)
class=>Symmetric k where swap :: k (a,b) (b,a)

attachUnit ...regroup' 是样板文件，需要它是因为 Haskell 的 (,)/() 并不是真正的幺半群。

或者，该类可以称为 Braided，其中也有 swap。不同之处在于对称类别需要 swap 。 swap == id，这在你的情况下似乎是合理的。

在constrained-categories中，我调用了封装这些方法的类Morphism。 （这是一个用词不当；遗憾的是，我在误导性的努力中选择了相当糟糕的名称，以保持与 Haskell 的标准类的紧密兼容性，并且仅暗示数学名称。）您的 PreCartesian 对应于我的 PreArrow。