VZ
Ну да, это так.
Size: a a a
2020 July 03
VZ
Хотя в той статье инстансы Functor написаны вручную, поэтому причин полагать, что это сделано для TH, нет.
VZ
Кроме одной фразы
> although it's possible to generate Functor instances with Template Haskell
> although it's possible to generate Functor instances with Template Haskell
АГ
В статье да, там неполная информация
MK
а как ты понимаешь гадты, если не хочешь вдаваться в "type classes, type equality, etc"?
АГ
а как ты понимаешь гадты, если не хочешь вдаваться в "type classes, type equality, etc"?
Интуитивно? Когда есть разница по сигнатурам типа или когда есть какие-нибудь вставки экзистенциальных типов
VZ
Кстати, не первый раз я слышу про “интуитивное” понимание GADT-ов. Для меня GADT-ы и интуитивность в одном предложении не вяжутся.
VZ
Я их понял только через трансляцию в type equality и existential quantification, а existential quantification нормально осознал только когда начал думать о ней как о нерелевантной зависимой сумме
АГ
Мое слово "интуитивное" здесь значит "неформальное". Сами gadt не интуитивные
MK
/me до сих пор не понимает слово "релевантный"
VZ
relevant значит можно матчиться (и соответственно надо в рантайме перекидывать)
VZ
irrelevant значит можно стереть из программы
MK
а в словосочетании "proof-relevant" какое значение?
VZ
Такое же – пруфы нельзя стереть
VZ
От них зависит вычислительная интерпретация кода
VZ
Например, в HoTT равнество может быть изоморфизмом, а изоморфизмы не уникальны
VZ
Поэтому если у меня
data T = A | B, то у T ~ Bool два возможных пруфаVZ
A <-> True; B <-> False
и
A <-> False; B <-> True
и
A <-> False; B <-> True
VZ
А в системе, где все пруфы это просто Refl, их можно выкинуть (proof irrelevance)
MK
пример такой системы?