произведение?
Ну типа того, любая структура будет типом-произведением. А дженерики тут вообще немного ортогональная семантика
в книге просто плавный подвод к идрису через упоминание логики и лямбда калкулуса, и они описали просто ДВА типа типов, и я завис т.к. не думал что всё можно представить как тип-произведение и тип-сумму
Не всё. Функция это тип-экспонента, например. А ещё есть П-типы.
Обсуждают сегодня