В
Я отвечу в трёх частях
для тех кто в танке, что за три части?
Size: a a a
2020 March 02
Oℕ
foo : forall A. A -> A
Oℕ
foo[A] = \a -> if(A is Int) a + 1 else a
Oℕ
foo - замкнутый терм типа forall A. A -> A
Oℕ
(foo, foo) не является отношением, соответствующим типу forall A. A -> A
λ
foo[A] = \a -> if(A is Int) a + 1 else a
а, что если типы не стёрлись в рантайме, то пользователю обязательно доступен их тайпреп?
Oℕ
это и называется "стирание типов" - уничтожение любой информации о типе
Oℕ
если какая-то информация осталась
Oℕ
ей можно воспользоваться для того, чтобы создать терм. не соответствующий отношению
Oℕ
то, что тип можно складывать
Oℕ
что у него есть выделенный элемент и т.п.
w
что у него есть выделенный элемент и т.п.
Oℕ
в языках с parametricity существует ровно один терм типа
forall A. A -> A - это айдентити
forall A. A -> A - это айдентити
λ
это и называется "стирание типов" - уничтожение любой информации о типе
но информация о типе может остаться в результате мономорфизации или для джита, а все остальные варианты получить информацию о типе могут быть заблокированы
Oℕ
но информация о типе может остаться в результате мономорфизации или для джита, а все остальные варианты получить информацию о типе могут быть заблокированы
мономорфизация не ломает параметрисити, и тип остаётся стёртым
Oℕ
она вообще не относится к обсуждаемой теме
Oℕ
типы без стирания - это когда можно написать терм, который использует информацию о типе как-то
Oℕ
которую ему не предоставили явно в виде параметра\инстанса
λ
понято, Олег