кажется, это пиратский стрим

зависит от системы. Если система содержит equality reflection, то нельзя:

Under a false hypothesis, all equations hold and every program is well-typed. As you cannot tell whether your current context contains a false hypothesis (what with the undecidability of propositions and all), it’s basically unsafe to execute open terms.

Если система содержит general recursion, то тоже нельзя, потому что доказательство равенства может быть фейковым и просто зацикливаться, так что надо досчитать до Refl и только потом коерсить

Плюс есть разные варианты иррелевантности. В агде есть по сути compile-time irrelevance и runtime-irrelevance. В первом случае если у тебя есть два значения x1, x2, которые имеют тип .A (точка отвечает за иррелевантность), то оба значения равны для тайпчекера и не существуют в рантайме. Во втором случае они не считаются равными для тайпчекера, но все еще отсуствуют в рантайме. Можно тут про второй случай почитать: https://agda.readthedocs.io/en/v2.6.1/language/runtime-irrelevance.html

Насколько я понимаю, надо читать про Quantitative Type Theory, чтобы понять общую картину, но я не читал

О, значит runtime-irrelevance это как раз то, что я вроде нормально понимаю (в отличие от остальных вариантов)

Круто, это в последней версии добавили

Вроде раньше это называлось spine irrelevance и существует уже несколько лет, но хз

А если мы фпамаем над списком значений оборачивая в ньютайп это тоже вырезано будет?

Тем язык хуже чем заставляет помнить реализацию всего

тут есть нюанс, что мы считаем поведение newtype каким-то нетривиальным только потому что сравниваем синтаксически с data, и видим другие поведение

А как правильно трансформеры расставлять ? Если мне допустим нужна программа работающая с изменяемым состоянием, и в то же время должно быть глобальное состояние неименяемое. Мне нужно делать ReaderT (StateT) или StateT (ReaderT) ?

было бы скажем

opaque type URL = String

и все функции в этом модуле могли бы спокойно конвертить из URL в String и наоборот - не было бы мысли что newtype ведут себя иначе по сравнению с data, но тогда бы пришлось писать больше сигнатур и не было бы возможности экспортировать маркер

то что newtype шарит синтаксис с data уже заставляем нас смотреть на это с другой стороны, с того что у newtype необычное поведение, хоть совсем наоборот, это у другой вещи такой же синтаксис как у data

ну язык ленивый, а fmap Wrapper это по сути fmap id, так что ничего не произойдет просто

Но можно и явно скоерсить

Тогда точно ничего не произойдёт

В случае с ReaderT/StateT не важно

Вот ExceptT/StateT будут по-разному себя вести в зависимости от порядка

А может быть разница в производительности ?

Может, но это сильно зависит от того, что именно делает код.

r -> s -> m (a, s)
s -> r -> m (a, s)