Блог

Наблюдение при определении List в agda с --without-K включенным:

Принимается следующее параметризованное индуктивное определение:

 data List (A : Set) : Set where
    [] : List A
    _::_ : A → List A → List A
 

но не эквивалентное определение индуктивного семейства:

 data List' : Set → Set where 
    []'  : {A : Set} → List' A
    _::'_ : {A : Set} → A → List' A → List' A
 

Сообщение об ошибке Set₁ is not less or equal than Set , поэтому я должен изменить тип с List' : Set → Set List' : Set → Set₁ на, чтобы он проверял тип. Если я отключу --without-K , то agda также правильно проверяет тип.

Я попытался выяснить, почему это так, например, на странице https://agda.readthedocs.io/en/latest/language/without-k.html в нем говорится: «Когда --without-K этот параметр включен, некоторые индексированные типы данных должны быть определены на более высоком уровне юниверса. В частности, типы всех индексов должны соответствовать типу типа данных. » Но в нем не говорится о причине такой разницы между определением индуктивного семейства (индексированных типов данных) и параметризованным индуктивным определением. Я предполагаю, что это как-то связано с интерпретацией гомотопической модели базовой теории типов. Однако я хочу знать, какая «плохая» вещь произойдет, если индуктивное семейство живет в меньшей вселенной (синтаксис и семантика). И как параметризованное индуктивное определение позволяет избежать такой проблемы?