Agda：函数解析错误

Question

我是agda的新手，并且按照小书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 → ...

最后，无法使用返回类型Bool定义该函数。它可以有a类型。

Answer 2

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