根据规范约束向量的类型
在像 Haskell 或 Idris 这样的语言中，是否可以创建一种数据类型来检查函数的输入向量是否是单一的？也就是说，我可以创建一个数据类型 SumsToOne 来检查向量的总和是否等于 1 等吗？
In a language like Haskell or Idris, is it possible to create a data type which checks if an input vector for a function is, for instance, unitary? That is, can I create a data type SumsToOne which checks if a vector adds up to 1, etc?
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（1）
是的。在伊德里斯，就像你说的那样。您可以用证明包装一个列表，其中元素之和为一。
但是，如果通过数据类型您指的是证明，而不是元素，则您可以只
证明是
sums xs = 1 类型。prf只是函数参数名称，auto表示 Idris 会在可以的情况下为您找到证明。我不知道这是否适用于浮点元素。
Yes. In Idris it's kind of just as you say. You could wrap a list with a proof the elements sum to one
Though if by data type you are referring to the proof, rather than the elements as well, you can just
The proof is of type
sums xs = 1.prfis just the function parameter name, andautomeans Idris will find the proof for you if it can.I don't know if this will work for floating point elements.