Почему размер обрабатывается по-разному, когда определяется как параметр по сравнению с индексом? - PullRequest
Новая
       9

Почему размер обрабатывается по-разному, когда определяется как параметр по сравнению с индексом?

1 голос
/ 15 января 2020

У меня вопрос по поводу некоторого кода, который использует взаимные индуктивные / коиндуктивные типы данных и типы размеров. 

module Ts where

open import Codata.Thunk using (Thunk; force)
open import Size using (Size; ↑_; ∞; Size<_)
open import Level using (Level)

private
  variable
    a : Level
    A : Set a

record L∞ (A : Set a) (i : Size) : Set a

data L (A : Set a) (i : Size) : Set a where
  []  : L A i
  _∷_ : A → L∞ A i → L A i

record L∞ A i where
  coinductive
  field force : {j : Size< i} → L A j
open L∞

♯_ : ∀ {i} → L A i → L∞ A i
♯ l = λ where .force {j} → {!l!}

-- Goal: L {A.a} A j
-- Have: L {A.a} A i
-- ————————————————————————————————————————————————————————————
-- j   : Size< i
-- l   : L {A.a} A i
-- i   : Size  (not in scope)
-- A   : Set A.a  (not in scope)
-- A.a : Level  (not in scope)

record L▴∞ (A : Set a) (i : Size) : Set a

data L▴ (A : Set a) : Size → Set a where
  []  : ∀ {i} → L▴ A i
  _∷_ : ∀ {i} → A → L▴∞ A i → L▴ A i

record L▴∞ A i where
  coinductive
  field force : {j : Size< i} → L▴ A j
open L▴∞

♯▴_ : ∀ {i} → L▴ A i → Thunk (L▴ A) i
♯▴ l = λ where .force {j} → {!l!}

-- Goal: L▴ {A.a} A j
-- Have: L▴ {A.a} A i
-- ————————————————————————————————————————————————————————————
-- j   : Size< i
-- l   : L▴ {A.a} A i
-- i   : Size  (not in scope)
-- A   : Set A.a  (not in scope)
-- A.a : Level  (not in scope)

Суть: https://gist.github.com/raduom/4c15349c1ccd5864ae08b2ed2d4157b8

Разница между двумя определениями я добавляю тип Size в индуктивное определение. Сначала я добавляю его как параметр типа, а во второе определение как индекс.

Вопрос в том, почему Agda принимает термин в первой лунке, а не во второй? 1012 *

...