什么时候应该使用数据类型和计算类型

Question

我什么时候应该更喜欢创建数据类型而不是计算类型？

具体示例 - 给出：

data Zero : Set where

record One : Set where

data Nat : Set where
  zero : Nat
  suc : Nat -> Nat

想要定义 \lt，它们各自的优点和缺点是什么：

-- a new datatype
data _<_ : Nat -> Nat -> Set where
  ozero : {n : Nat} -> zero < suc n
  osuc : {n m : Nat} -> n < m -> suc n < suc m

与

-- calculating
_<_ : Nat -> Nat -> Set
zero < zero = Zero
zero < suc m = One
suc n < zero = Zero
suc n < suc m = n < m

到目前为止我已经得到了这些：

• 我记得/已经看到的是，第二个使 agda 有时更难推断隐式参数（？）
• 第一个应该使用更多内存（？）
• 当您希望 agda 能够将您的小于证明作为隐式参数推断时，例如当您的参数是常量/可推断时，第二种数据类型更有用