如何解决如何编写接受具有特定元素类型的嵌套 Vect 的函数?
我想编写一个函数,它接受任意嵌套的 Vect
,其最终元素是一组有限的类型,包括。 Double
和 Integer
(“dtype”),并且该函数知道有多少个 Vect
,以及每个的大小(即“形状”)。>
例如,如果我的函数名为 const
,我希望 const 0.0
和 const [[0.0],[1.0]]
编译,并且类型检查器知道第一个没有 Vect
,第二个有两个,长度为 2 和 1。我不想编译 const [["foo"],["bar"]]
。
我的尝试
- 为嵌套向量定义类型别名并为重载使用命名空间
Array : (shape : Vect rank Nat) -> Type -> Type
Array [] ty = ty
Array (d :: ds) ty = Vect d (Array ds ty)
namespace double
const : Array shape Double -> Foo shape Double
namespace integer
const : Array shape Integer -> Foo shape Integer
但是因为这有点倒退(编译器必须从 const
的返回类型而不是参数中推断类型),所以推断类型(即使对于像 const 0.0
这样的简单情况)有困难不明确的上下文。
- 定义一个接口来跟踪形状
interface Array ty where
rank : Nat
shape : Vect rank Nat
dtype : Type
Array Double where -- same for other types
rank = 0
shape = []
dtype = Double
{len : Nat} -> Array ty => Array (Vect len ty) where
rank = 1 + rank {ty}
shape = len :: shape {ty}
dtype = dtype {ty}
const : Array ty => ty -> Foo (shape {ty}) (dtype {ty})
但这不起作用,因为 Idris 不会在 Data.Vect.::
中消除 Prelude.::
和 const [0.0]
之间的歧义,即使我只为 {{1} 实现了 Array
}} 不是 Vect
。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。