依赖类型签名中的多态常量？答案

【问题标题】：Polymorphic constant in a dependent type signature?依赖类型签名中的多态常量？
【发布时间】：2019-03-09 17:00:15
【问题描述】：

假设我想定义一种证明某个向量具有一定总和的类型。我还希望该证明适用于任何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

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

我最后的尝试是定义一个带有大写字母名称的辅助常量，这样 Idris 就不会将它与绑定变量混淆：

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 类型中表达多态常量？

【问题讨论】：

标签： constants idris dependent-type parametric-polymorphism

【解决方案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}) []

也可以。

【讨论】：