尝试将隐式参数引入 Idris 中定义左侧的范围会导致 "is f applied to too many arguments" 错误

Question

函数 applyRule 应该提取隐式参数 n，该参数在它获取的另一个参数中使用，类型为 VVect。

data IVect : Vect n ix -> (ix -> Type) -> Type where -- n is here
  Nil  : IVect Nil b
  (::) : b i -> IVect is b -> IVect (i :: is) b

VVect : Vect n Nat -> Type -> Type -- also here
VVect is a = IVect is (flip Vect a)

-- just for completeness
data Expression = Sigma Nat Expression

applyRule : (signals : VVect is Double) ->
            (params : List Double) ->
            (sigmas : List Double) ->
            (rule : Expression) ->
            Double

applyRule {n} signals params sigmas (Sigma k expr1) = cast n

不引用 {n}，代码类型检查（如果 cast n 更改为某个有效的双精度）。但是，添加它会导致以下错误：

When checking left hand side of applyRule:
Type mismatch between
        Double (Type of applyRule signals params sigmas rule)
and
        _ -> _ (Is applyRule signals
                             params
                             sigmas
                             rule applied to too many arguments?)

这对我来说似乎没有意义，因为我没有对任何可能依赖于 n 的参数进行模式匹配，所以我认为简单地将它放在花括号中会将其纳入范围。

Answer 1

如果 n 在某处定义（例如作为参数中的变量），您只能将其带入范围。否则很难弄清楚 n 是从哪里来的——至少对于人类来说是这样。

applyRule : {is : Vect n Nat} ->
            (signals : VVect is Double) ->
            (params : List Double) ->
            (sigmas : List Double) ->
            (rule : Expression) ->
            Double
applyRule {n} signals params sigmas (Sigma k expr1) = cast n

尝试将隐式参数引入 Idris 中定义左侧的范围会导致 "is f applied to too many arguments" 错误

Trying to bring implicit argument into scope on the left side of a definition in Idris results in "is f applied to too many arguments" error

idris