16

在 Idris/Haskell 中，可以通过注释类型和使用 GADT 构造函数来证明数据的属性，例如使用 Vect，但是，这需要将属性硬编码到类型中（例如，Vect 必须是与 List 不同的类型）。是否可以拥有具有一组开放属性的类型（例如同时带有长度和运行平均值的列表），例如通过重载构造函数或使用 Effect 中的某些东西？

4

1 回答 1

17
于 2014-12-01T01:28:34.643 回答