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

此外，必须在like之前隐式或显式地声明依赖类型。

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

最后，该函数不能定义为返回类型Bool。但它的类型可以是a。

Answer 2

作为一个额外的语法点，在Agda中，下划线是混合参数的占位符：what_bottom是一个混合名称，在what和bottom之间有一个参数。因此，您最终会得到一个用作what (Onion $ Lamb $ Bottom) bottom的函数，而这可能不是您想要的。如果你觉得有点多余，就叫它whatBottom或what‿bottom吧。