命名 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

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

\n\n

Idris> :t (.)\n(.) : (b -> c) -> (a -> b) -> a -> c\nIdris> :set showimplicits \nIdris> :t (.)\nPrelude.Basics.(.) : {c : Type} -> {a : Type} -> {b : Type} -> (b -> c) -> (a -> b) -> a -> c\n

\n\n

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

\n\n

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

\n\n

\xce\xbb\xce\xa0> MkData {schema = String} 2 ["hi", "Steven"]\nMkData 2 ["hi", "Steven"] : DataStore String\n

\n\n

第二件事是声明中类型构造函数的类型中的变量的data范围不限于该类型构造函数之外的任何内容。您给出的第二个定义DataStore与原始定义完全相同，因为中的“模式”不在DataStore : (schema : Type) -> Type类型签名的范围内MkData。

\n