idris - 为什么 Idris 将值名称与随后定义的类型参数名称混为一谈？

Question

Haskell 允许:

a:: Int 
a = 3
data MyList a = Nil | Cons a (MyList a) 

而 idris 会提示 a is bound as an implicit ,
我需要使用不同类型的参数:

a: Int 
a = 3
data MyList b = Nil | Cons b (MyList b)

Answer 1

实际上，Idris 并没有在这里将它们混为一谈，因为 a是小写。但它可以——除了 Haskell——因为它支持类型中的值。因此编译器会警告您，因为这是错误的常见来源。假设你写:

n : Nat
n = 3

doNothing : Vect n Int -> Vect n Int
doNothing xs = xs

您可能期望 doNothing的类型是 Vect 3 Int -> Vect 3 Int .而是 lower case arguments are bound to be implicit和 doNothing的类型实际上是 {n : Nat} -> Vect n Int -> Vect n Int ，尽管之前声明 n .你必须写 Vect Main.n Int或制作 N大写来使用它。

所以编译器认为也许你想做一些与 a 类似的事情。在 MyList a并警告你。