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

【问题标题】：Why does Idris conflate a value name with a type argument name that is subsequently defined?为什么 Idris 将值名称与随后定义的类型参数名称混为一谈？
【发布时间】：2023-03-12 12:04:01
【问题描述】：

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)

【问题讨论】：

标签： idris

【解决方案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 大写才能使用它。

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

【讨论】：