以下面的例子为例
postulate DNE : {A : Set} ? ¬ (¬ A) ? A
data ? (A B : Set) : Set where
inl : A ? A ? B
inr : B ? A ? B
-- Use double negation to prove exclude middle
classical-2 : {A : Set} ? A ? ¬ A
classical-2 = ? {A} ? DNE (? z ? z (inr (? x ? z (inl x)))
我知道这是正确的,纯粹是因为agda是如何工作的,但我是这种语言的新手并且不能理解它的语法是如何工作的,如果有人能告诉我正在发生的事情,我将不胜感激,谢谢:)
我有haskell的经验,虽然那是一年前的事.
让我们从假设开始.语法很简单:
postulate name : type
这断言存在一些type被称为类型的值name.将其视为逻辑中的公理 - 被定义为真实且不受质疑的事物(在这种情况下由Agda提出).
接下来是数据定义.mixfix声明略有疏忽,所以我会解决它并解释它的作用.第一行:
data _?_ (A B : Set) : Set where
引入一个名为的新类型(构造函数)_?_._?_接受两个类型的参数,Set然后返回一个Set.
我将它与Haskell进行比较.的A和B是或多或少等效a和b在下面的例子:
data Or a b = Inl a | Inr b
这意味着数据定义定义了多态类型(模板或通用,如果您愿意).Set是Agda相当于Haskell的*.
下划线有什么用？Agda允许您定义任意运算符(前缀,后缀,中缀...通常仅由单个名称调用 - mixfix).下划线告诉Agda参数在哪里.使用前缀/后缀运算符最好看:
-_ : Integer ? Integer -- unary minus
- n = 0 - n
_++ : Integer ? Integer -- postfix increment
x ++ = x + 1
您甚至可以创建疯狂的运算符,例如:
if_then_else_ : ...
下一部分是数据构造函数本身的定义.如果您已经看过Haskell的GADT,这或多或少是相同的.如果你还没有:
当您在Haskell中定义构造函数时,Inr如上所述,您只需指定参数的类型,Haskell就会计算整个事物的类型,即Inr :: b -> Or a b.当您在Agda中编写GADT或定义数据类型时,您需要指定整个类型(并且有充分的理由,但我现在不会介绍它).
因此,数据定义指定了两个inl类型A ? A ? B和inr类型的构造函数B ? A ? B.
现在是有趣的部分:第一行classical-2是一个简单的类型声明.这Set件事怎么了？当您在Haskell中编写多态函数时,您只需使用小写字母来表示类型变量,例如:
id :: a -> a
你真正的意思是:
id :: forall a. a -> a
你真正的意思是:
id :: forall (a :: *). a -> a
即它不仅仅是任何一种a,但这a是一种类型.Agda让你做这个额外的步骤并明确地声明这个量化(那是因为你可以量化更多的东西而不仅仅是类型).
还有花括号？让我再次使用上面的Haskell示例.例如,当您在id某处使用该功能时id 5,您无需指定该功能a = Integer.
如果您使用普通的paretheses,则A每次调用时都必须提供实际类型classical-2.但是,大多数情况下,类型可以从上下文中推断出来(很像id 5上面的示例),因此对于这些情况,您可以"隐藏"参数.然后Agda尝试自动填充 - 如果不能,它会抱怨.
而对于最后一行:? x ? y是阿格达的说法\x -> y.这应该可以解释大部分内容,唯一剩下的就是花括号了.我相当肯定你可以在这里省略它们,但无论如何:隐藏的论据做他们所说的 - 他们隐藏.所以当你定义一个函数{A}时B,你只需要提供一些类型的东西B(因为它{A}是隐藏的).在某些情况下,你需要知道隐藏参数的值,这就是这种特殊的lambda所做的:? {A} ?允许你访问隐藏的A!