基于范数约束向量的类型

Question

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

Answer 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 会在可能的情况下为您找到证明。

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