示例：函数解析错误

Question

我是 agda 的新手，正在学习 little MLer 一书中的一个简单示例。谁能帮我弄清楚为什么编译器会给我一个解析错误？

谢谢

data Shish (a : Set) : Set where
  Bottom : a → Shish a
  Onion : Shish a → Shish a
  Lamb : Shish a → Shish a
  Tomato : Shish a → Shish a

data Rod : Set where
  Dagger : Rod
  Fork : Rod
  Sword : Rod

data Plate : Set where
  Gold-plate : Plate
  Silver-plate : Plate
  Brass-plate : Plate

what_bottom : Shish (a : Set) → Bool
what_bottom (Bottom x) → x
what_bottom (Onion x) → what_bottom x
what_bottom (Lamb x) → what_bottom x
what_bottom (Tomato x) → what_bottom x



/Volumes/Little/mko_io/cat/tmp/mler.agda:54,24-24
        /Volumes/Little/mko_io/cat/tmp/mler.agda:54,24: Parse error
        :<ERROR>
         Set) → Bool
        what_bottom (Bott...

Answer 1

数据类型定义已正确定义，但这不是 Agda 中定义函数的方式。一个好的入门教程是 Dependent types at work

函数用等号定义。

id : {A : Set} → A → A
id a = a

此外，依赖类型必须像这样隐式或显式声明。

what_bottom : {A : Set} → Shish A → ...

最后，该函数不能用 return 类型定义 Bool。不过它可以有类型 a。

Answer 2

作为一个额外的语法点，在 Agda 中，下划线是 mixfix 参数的占位符：what_bottom 是一个 mixfix 名称，其中一个参数介于 what 和 bottom 之间。所以你最终会得到一个你将用作 what (Onion $ Lamb $ Bottom) bottom 的函数，这可能不是你想要的。如果你觉得额外的，就叫它 whatBottom 或 what‿bottom。

示例：函数解析错误

Agda: Function Parsing error

parsing

agda