Когда я должен использовать типы данных против типов расчета - PullRequest
Новая
       10

Когда я должен использовать типы данных против типов расчета

3 голосов
/ 10 марта 2020

Когда я предпочитаю создавать типы данных, а не вычислять типы?

Конкретный пример - дано: 

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

Пока у меня есть эти:

  • Я помню / видел, что второй делает это Агде труднее иногда выводить неявные аргументы (?)
  • первый должен использовать больше памяти (?)
  • второй тип данных более полезен, когда вы хотите, чтобы агда могла выводить ваши менее чем доказательство в качестве неявного аргумента, например, когда ваши аргументы являются константами / выводимыми
...