Ответ 1
Аксиома K также называется принципом единственности доказательств тождества и является аксиомой о природе тождественного типа в теории типа типа Мартина-Лёфа. Этот тип не существует (и на самом деле не может быть определен) в более простых типах, таких как система F, поэтому, вероятно, это причина, по которой вы не сталкивались с этим в упомянутых вами книгах.
Тип идентификации записывается как Id(A,x,y) или также x = y и кодирует свойство, что x и y равны (в соответствии с соответствием Карри-Говарда). Существует один базовый способ дать доказательство типа идентичности, а это refl : Id(A,x,x), т.е. Доказательство того, что x равно самому себе.
При исследовании типа идентичности в тезисе Томас Штрейхер представил новый выпрямитель для типа идентичности, который он назвал K (в качестве следующей буквы в алфавите после J, стандартный выпрямитель для типа идентичности). В нем утверждается, что любое доказательство равенства p равенства x = x само по себе равно тривиальному доказательству refl. Отсюда следует, что любые два доказательства p и q любого уравнения x = y равны, поэтому альтернативное имя "уникальность доказательств тождества". Примечательно то, что он доказал, что это не вытекает из стандартных правил теории типов. Я рекомендую прочитать статью Dan Licata на блоге теории гомотопического типа, если вы хотите понять, почему нет, он объясняет это намного лучше, чем я мог.
Чтобы ответить на вторую часть вашего вопроса: сопоставление шаблонов ML-стиля не связано с K, поскольку ML не имеет типа идентификации и, следовательно, не может даже сформулировать аксиому K. С другой стороны, K требуется для зависимого сопоставления шаблонов, введенного Тьерри Коквандом в "Согласование шаблонов с зависимыми типами (1992)". Причиной этого является то, что очень легко доказать K путем сопоставления шаблонов на конструкторе refl тождественного типа:
K : (p : x = x) -> p = refl
K refl = refl
Фактически, Конор Макбрайд показал в своем тезисе ( "В зависимости от типизированных функциональных программ и их доказательств (2000)" ), что K - единственное, что зависимое сопоставление шаблонов действительно добавляет к теории зависимых типов.
Мой интерес к этому вопросу заключается в том, чтобы точно понять, почему зависимое сопоставление шаблонов требует K и как его можно ограничить, чтобы его больше не было. Результатом стала статья и новая реализация опции --without-K в Agda. Основная идея заключается в том, что алгоритм унификации, используемый для анализа случаев во время зависимого сопоставления шаблонов, не должен удалять уравнения формы x = x, потому что для этого требуется К. Я рекомендую вам прочитать (введение) статьи, если вы хотите знать больше.