问题描述
我想编写一个函数,它接受任意嵌套的 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 (将#修改为@)