Agda: ошибка разбора функции

Question

Я новичок в агде, и следую простому примеру в книге маленький 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 подчеркивания являются заполнителями для аргументов mixfix: what_bottom - это имя mixfix с одним параметром от what до bottom. Таким образом, вы получите функцию, которую вы будете использовать как what (Onion $ Lamb $ Bottom) bottom, что, вероятно, не то, что вы хотели. Просто назовите это whatBottom или what‿bottom, если вы чувствуете себя лишним.

Answer 2

Определения типов данных определены правильно, но это не тот способ, которым определяются функции в Agda. Хороший стартовый урок: Зависимые типы на работе

Функции определены со знаком равенства.

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

Более того, зависимый тип должен быть объявлен раньше, например, неявно или явно.

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

Наконец, эту функцию нельзя определить с типом возврата Bool. Он может иметь тип a.