как интерпретировать REL в agda

Question

Я пытаюсь понять некоторые части стандартной библиотеки Agda, и я не могу понять, как определить REL. FWIW вот определение REL:

-- Binary relations 

-- Heterogeneous binary relations 

REL : ∀ {a b} → Set a → Set b → (ℓ : Level) → Set (a ⊔ b ⊔ suc ℓ) 
REL A B ℓ = A → B → Set ℓ 

Я не могу найти никакой документации онлайн, объясняющий это, поэтому я спрашиваю здесь. Как это определяет двоичное отношение?

Answer 1

@ Ответ Родриго Рибейро объясняет бит Level, но как только вы избавитесь от уровней юниверсов, что делает тип Set → Set → Set связан с бинарными отношениями?

Предположим, вы имеете двоичное отношение R ⊆ A × B. Пропозициональным способом моделирования является создание некоторого индексированного типа R : A → B → Set, так что для любого a : A, b : BR a b имеет жителей iff (a, b) ∈ R. Поэтому, если вы хотите поговорить обо всех отношениях за A и B, вам нужно поговорить обо всех A - и B - индексированных типах, то есть вам нужно поговорить о RelationOverAandB = A → B → Set.

Если вы хотите абстрагироваться от левого и правого базового типа отношения, это означает, что выбор A и B больше не фиксируется. Поэтому вы должны поговорить о REL, так что REL A B = A → B → Set.

Что же такое тип REL? Как мы видели из примера REL A B, в качестве двух аргументов он принимает выбор A и B; и его результатом является типA → B → Set.

Итак, подведем итог: учитывая

A : Set 
B : Set 

мы имеем

REL A B = A → B → Set 

который сам по себе имеет тип Set (помните, мы игнорируем уровни вселенной здесь).

И, таким образом,

REL : Set → Set → Set ∎ 

Answer 2

Чтобы определить двоичное отношение, нам нужны два набора, поэтому REL нуждается, по крайней мере, в двух типах. Тип REL:

REL : ∀ {a b} → Set a → Set b → (ℓ : Level) → Set (a ⊔ b ⊔ suc ℓ) 

Этот тип немного загрязнена из-за материала, уровня Вселенной. Если вы позволяете себе немного неформальности, вы можете отключить уровни вселенной (больше информации об этом here) и написать REL как:

REL : Set -> Set -> Set 

который является типом, который ожидает два типа в качестве параметров.

Использование вселенных в теории типов заключается в том, чтобы избежать парадоксов, подобных Russell's Paradox теории множеств.

Я не специалист по теории типа, но интерпретация REL типа можно резюмировать следующим образом:

• Set a и Set b являются параметры типа уровней вселенной a и b соответственно.
• Оператор ⊔ возвращает максимум два уровня параметров.

Надеюсь, что это может вам помочь.

Answer 3

Я предполагаю, что это легче смотреть на пример:

import Level 
open import Relation.Binary 
open import Data.Nat.Base hiding (_≤_) 

data _≤_ : REL ℕ ℕ Level.zero where 
    z≤n : ∀ {n} -> 0 ≤ n 
    s≤s : ∀ {n m} -> n ≤ m -> suc n ≤ suc m 

Сигнатура типа эквивалентно

data _≤_ : ℕ -> ℕ -> Set where 

Так _≤_ есть отношение между два натуральных числа. Он содержит все пары чисел, для которых первое число меньше или равно второму. Таким же образом мы можем написать

open import Data.List.Base 

data _∈_ {α} {A : Set α} : REL A (List A) Level.zero where 
    here : ∀ {x xs} -> x ∈ x ∷ xs 
    there : ∀ {x y xs} -> x ∈ xs -> x ∈ y ∷ xs 

Сигнатура типа эквивалентна

data _∈_ {α} {A : Set α} : A -> List A -> Set where 

_∈_ является соотношением между элементами типа A и списками элементов типа A.

Вселенная мономорфным вариант REL сам по себе является бинарное отношение:

MonoREL : REL Set Set (Level.suc Level.zero) 
MonoREL A B = A → B → Set