依赖类型的签名中的多态性常数

Question

说我想定义某种证明某些向量具有一定总和的证明。我也希望该证明适用于任何Monoid类型t。我的第一个尝试是：

data HasSum : Monoid t => t -> Vect n t -> Type where
    EndNeutral : Monoid t => HasSum Prelude.Algebra.neutral []
    Component : Monoid t => (x : t) -> HasSum sum xs -> HasSum (x <+> sum) (x :: xs)

不幸的是，编译器认为它是Can't find implementation for Monoid t。因此，我尝试了一个隐式参数，以便可以指定其类型：

    EndNeutral : Monoid t => {Prelude.Algebra.neutral : t} -> HasSum Prelude.Algebra.neutral []

此编译，但这不是：

x : HasSum 0 []
x = EndNeutral

奇怪地声称IT Can't find implementation for Monoid Integer。

我的最后尝试是定义带有大写字母名称的辅助常数，以便IDRI不会将其混淆为界变量：

ZERO : Monoid t => t
ZERO = neutral
data HasSum : Monoid t => t -> Vect n t -> Type where
    EndNeutral : Monoid t => HasSum ZERO []
    Component : Monoid t => {rem : t} -> (x : t) -> HasSum rem xs -> HasSum (x <+> rem) (x :: xs)

，但现在无法猜测EndNeutral（Can't find implementation for Monoid t）定义中ZERO的类型。因此，我再次尝试使用隐式绑定：

    EndNeutral : Monoid t => {ZERO : t} -> HasSum ZERO []

但是现在ZERO成为一个界变量，尽管它编译了，但它无法按预期工作，因为它允许构建具有任意总和的空载体的证明。

此时我用完了想法。有人知道如何在IDRIS类型中表达多态常数吗？

Answer 1

看来我终于找到了答案。它可能不是最好的，但它是我现在唯一知道的。因此，必须在不添加隐式参数的情况下明确指定neutral的类型（这会将neutral变成绑定变量）。当然，功能the可以实现此目的：

data HasSum : Monoid t => t -> Vect n t -> Type where
    EndNeutral : Monoid t => HasSum (the t Prelude.Algebra.neutral) []
    Component : Monoid t => {rem : t} -> (x : t) -> HasSum rem xs -> HasSum (x <+> rem) (x :: xs)

编辑：

查看neutral的类型提出了另一个解决方案：

> :doc neutral
Prelude.Algebra.neutral : Monoid ty => ty

看来neutral的具体类型实际上是一个隐含的参数。因此：

EndNeutral : Monoid t => HasSum (Prelude.Algebra.neutral {ty = t}) []

也有效。