b
ну это анализ одной пропозиции из трактата
Size: a a a
2020 June 24
b
плюс исторический контекст
DS
Russels theory of types - словно ей кто-то вообще пользуется
b
я только эту теорию типов знаю..
DF
Кстати в современной ТТ тоже есть понятие формы
DF
Shape
DF
Но это имеет смысл только в заатиповом сеттинге наверн
DS
я только эту теорию типов знаю..
Из современного - вон HoTT и погнали или с более старого Мартин-Лёфа начать
DS
Хотя хотт - это положение теорий Мартин-Лёфа, насколько я понимаю
λ
было бы круто если бы в идрисе была фича из тайпскрипта:
let foo: any = ...;
if (foo instanceof Struct) {
// здесь foo имеет тип Struct
}
да и вообще во всех языках
let foo: any = ...;
if (foo instanceof Struct) {
// здесь foo имеет тип Struct
}
да и вообще во всех языках
есть такая фича:
((a : Type) ** a)G
Отвратительно
+
G
для завтипов было бы полезно
для зав типов патмат обычный
b
сегодня я узнал что я наполовину chad
p
для зав типов патмат обычный
&
p
не понял
G
хз мне лень
λ
двачую про аппеляцию к авторитету
AZ
было бы круто если бы в идрисе была фича из тайпскрипта:
let foo: any = ...;
if (foo instanceof Struct) {
// здесь foo имеет тип Struct
}
да и вообще во всех языках
let foo: any = ...;
if (foo instanceof Struct) {
// здесь foo имеет тип Struct
}
да и вообще во всех языках
так ты же там по типам матчиться можешь