Agda中定义多参数数据类型是否需在参数间添加分隔符号？

问题代码 #

data Mode : Set where
  ⇛ : Mode
  ⇚ : Mode

infix  4  _⊢_

data _⊢_ : Context → Term → Mode → Type → Set where
  ⊢-int : ∀ {Γ n}
    → Γ ⊢ (lit n) ⇛ Int

错误信息 #

Mode → Type → Set should be a sort, but it isn't
when checking that the inferred type of an application
Mode → Type → Set
matches the expected type
_30

问题原因 #

Agda要求data声明的类型部分必须是合法的种类（sort），比如Set、Set₁或返回这些sort的函数类型。当前写法中，_⊢_的类型被解析为Context → Term → (Mode → Type → Set)，而Mode → Type → Set属于Set层级的类型，并非合法的sort，因此不符合data声明的语法要求。

解决方案 #

无需使用无意义的点符号，有两种简洁合规的写法：

方案1：使用带中缀参数的运算符

保留_⊢_的中缀特性，通过中缀参数嵌入Mode和Type，兼顾语法合规性与可读性：

data Mode : Set where
  ⇛ : Mode
  ⇚ : Mode

infix 4 _⊢_[_]_

data _⊢_[_]_ : Context → Term → Mode → Type → Set where
  ⊢-int : ∀ {Γ n}
    → Γ ⊢ (lit n) [ ⇛ ] Int

方案2：改用前缀数据类型

如果不需要严格的二元中缀形式，直接将所有参数放在数据类型名后，写法更直接：

data Mode : Set where
  ⇛ : Mode
  ⇚ : Mode

data ⊢ : Context → Term → Mode → Type → Set where
  ⊢-int : ∀ {Γ n}
    → ⊢ Γ (lit n) ⇛ Int

内容的提问来源于stack exchange，提问作者DoubleX