haskell - 基于范数约束向量的类型

Question

在像 Haskell 或 Idris 这样的语言中，是否可以创建一种数据类型来检查函数的输入向量是否是单一的？也就是说，我可以创建一个数据类型 SumsToOne 来检查向量加起来是否等于 1 等吗？

Answer 1

是的。在 Idris 中，就像您所说的那样。你可以用元素总和为 1 的证据包装一个列表

data SumsToOne : Type where
  STO : (xs : List Int) -> {auto prf : sum xs = 1} -> SumsToOne

虽然如果按数据类型你指的是证明，而不是元素，你可以只是

go : (xs : List Int) -> {auto prf : sum xs = 1} -> <whatever you're returning>

证明的类型是sums xs = 1。 prf 只是函数参数名，auto 表示如果可以，Idris 会为您找到证明。

我不知道这是否适用于浮点元素。