命名 v 未命名数据类型参数

Question

在Type Driven Development with Idris第6章的代码中，我被这段代码弄糊涂了：

data DataStore : Type -> Type where
    MkData : (size : Nat) ->
             (items : Vect size schema) ->
             DataStore schema

我认为它可能无法编译，因为 schema 似乎未定义或至少需要以某种方式绑定到 DataStore 的第一个参数。但是，它加载正常，可以像这样使用：

*DataStore> the (DataStore String) $ MkData 2 ["Fred", "Wilma"]
MkData 2 ["Fred", "Wilma"] : DataStore String

我认为 DataStore 的第一个参数需要命名为 schema，如下所示：

data DataStore : (schema : Type) -> Type where
    MkData : (size : Nat) ->
             (items : Vect size schema) ->
             DataStore schema

这个定义可以像最初的那样使用。

我想知道这两个定义之间是否存在任何语义差异，是否有人可以帮助我解决我对 schema 未定义的错误直觉。

Answer 1

这里发生了两件事。第一个是隐式参数。用作函数参数的小写名称总是转换为隐式参数。例如，函数组合运算符：

Idris> :t (.)
(.) : (b -> c) -> (a -> b) -> a -> c
Idris> :set showimplicits 
Idris> :t (.)
Prelude.Basics.(.) : {c : Type} -> {a : Type} -> {b : Type} -> (b -> c) -> (a -> b) -> a -> c

compose 的类型涉及变量 a、b 和 c，这些变量未在其类型签名中的任何位置声明。 Idris 将它们变成隐式参数——所有参数都具有 Type 类型——它将尝试通过统一来推断。 {curly brackets} 是用于显式指定隐式参数的语法。您始终可以在解释器中使用 :set showimplicits 来查看它们。在 DataStore 示例中，schema 是一个隐式变量。

您还可以在调用具有隐式的函数时指定隐式：

λΠ> MkData {schema = String} 2 ["hi", "Steven"]
MkData 2 ["hi", "Steven"] : DataStore String

第二件事是 data 声明中类型构造函数类型中的变量除了那个类型构造函数之外没有任何作用域。您给出的 DataStore 的第二个定义与原始定义完全相同，因为 DataStore : (schema : Type) -> Type 中的 "schema" 不在 MkData.[=21= 类型签名的范围内]

命名 v 未命名数据类型参数

Named v unnamed data type arguments

idris