Finite sum over a monoid

Function

context $ \langle\!\langle M,* \rangle\!\rangle$ … monoid
let $e$ … unit of $\langle\!\langle M,* \rangle\!\rangle$
definition $\sum^n:\prod_{S:\mathrm{Sequence}(M)}\mathrm{range}(\mathrm{length}(S))\to M$
definition $\sum_{k=1}^n\ S_k:= \begin{cases} e & \mathrm{if}\ n=0\\\\ \left(\sum_{k=1}^{n-1}\ S_k\right)\ *\ S_n & \mathrm{else} \end{cases}$

Discussion

Here $\prod_{S:\mathrm{Sequence}(M)}$ is a dependent function type former.


Context

Monoid, Sequence length

Requirements

Sequence length