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

Question

Haskell允许:

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

虽然伊德里斯会抱怨a is bound as an implicit,我需要使用不同类型的论点:

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

Answer 1

实际上,伊德里斯并没有把它们混为一谈,因为它a是小写的.但它可以 - 除了Haskell - 因为它支持类型中的值.所以编译器警告你,因为这是错误的常见来源.假设你写:

n : Nat
n = 3

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

你可能期望那种doNothing类型Vect 3 Int -> Vect 3 Int.但是相反,小写参数必然是隐式的,而doNothing实际上是类型{n : Nat} -> Vect n Int -> Vect n Int,尽管先前声明了n.您必须编写Vect Main.n Int或使用N大写字母才能使用它.

所以编译器认为你可能想做一些类似于ain的事情MyList a并警告你.