idris - 命名 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 中的“模式”不在 MkData 的类型签名范围内.