История изменений

Через поднятия/опускания типов можно выразить все что угодно, т.к. если есть поднятия/опускания типов - то перед нами динамика.

Там определённые поднятия и опускания, а не вообще. Если типы A и B связаны отношением A <: B то можно безопасно поднять A в B, то есть подтип в супертип. Например, если A агрегирует или наследует B, то можно спокойно использовать этот подтип как супертип (то есть поднять и ожидать выполнения LSP), но обратно уже нужно опускать не из B в A, а из B в Maybe/Optional A, то есть, фактически, делать typecase по набору подтипов супертипа. Это именно статическое подтипирование в духе ООП языков (а также Data.Dynamic хаскеля и некой известной в ML техники - но тут уже сразу (и только) для топ-а). Динамика и топ появляются когда предпорядок становится directed (частичный и полный порядок я не беру, так как не хочу выбрасывать циклические данные из рассмотрения (хотя они же цикличные - это уже звоночек)).

Через поднятия/опускания типов можно выразить все что угодно, т.к. если есть поднятия/опускания типов - то перед нами динамика.

Там определённые поднятия и опускания, а не вообще. Если типы A и B связаны отношением A <: B то можно безопасно поднять A в B, то есть подтип в супертип. Например, если A агрегирует или наследует B, то можно спокойно использовать этот подтип как супертип (то есть поднять и ожидать выполнения LSP), но обратно уже нужно опускать не из B в A, а из B в Maybe/Optional A, то есть, фактически, делать typecase по набору подтипов супертипа. Это именно статическое подтипирование в духе ООП языков (а также Data.Dynamic хаскеля и некой известной в ML техники - там уже сразу топ). Динамика и топ появляются когда предпорядок становится directed (частичный и полный порядок я не беру, так как не хочу выбрасывать циклические данные из рассмотрения (хотя они же цикличные - это уже звоночек)).