DF
В общем это Дроздов
Size: a a a
2020 June 09
G
Какими типами-то. Вот у нас есть число. Мы хотим на него поделить другое число. Чтобы на уровне типов не давать делить на 0, нужны зависимые типы. Всё, приехали, языков с зависимыми типами существует 1 штука, идрис
Ещё можно воспользоваться weakest precondition calculus, как делают в FramaC
G
Так, народ
G
Вам когда-то пригождались кортежи вместо просто переменных в теле функции (не когда она возвращает кортеж)?
DF
Да, это полезно
DF
Меньше имен
G
Ну допустим можно в коллекцию их запихать
G
Что ещё?
SP
интересна ситуация в котлине. они сначала запилили кортежи, поняли что это мусор и оставили только тупл и трипл типы, для больше элементов рекомендуют создавать тип.
SP
лол у полунина РО
DF
Танку еще
DF
Хотя вроде спокойно щас , нет набросов
С
Вам когда-то пригождались кортежи вместо просто переменных в теле функции (не когда она возвращает кортеж)?
Для Task<result, exception>, чтобы Task.WhenAll дожидался всех, а не умирал на первой же таске с ошибкой
DF
+
AZ
let f = |key: &[&_]| match key {G
Tuples at home:
AZ
все же я радикально не понимал вчера вашу позицию. Для того что я хотел как бы никакие завтипы не нужны, мы просто кодим option на типах в компайлтайме, этот option представляем не отдельной структурой а самим флоатом, у нас таким образом получается байтовое представление одно а представление в компайлтайме другое. получается та же мейби монада только мы это рантайм(читаем процессорное) поведение сопровождаем статически
т.е. короче все операции которые нам дают нан должны отдавать наш optional, и в обычном случае мы просто делаем мап по optional который должен заэлиминейтиться в тот код который вы и хотите получить(т.е. без проверок)
да это все выглядит ужасно без ду нотации и это не для каждого языка и не для каждой хотелки но чисто как PoC в голове я это представляю вполне.
а то что говорил голдштейн "оно же в процессоре" - это вообще как бы какое то совсем непонимание статики. статика это и есть эмулирование рантайм поведения в компайлтайме. смысл статики как раз в том что мы вкладываем в обьект в компайлтайме тонну лишнего смысла который нам нужен хотя в рантайме это просто сраный инт
т.е. короче все операции которые нам дают нан должны отдавать наш optional, и в обычном случае мы просто делаем мап по optional который должен заэлиминейтиться в тот код который вы и хотите получить(т.е. без проверок)
да это все выглядит ужасно без ду нотации и это не для каждого языка и не для каждой хотелки но чисто как PoC в голове я это представляю вполне.
а то что говорил голдштейн "оно же в процессоре" - это вообще как бы какое то совсем непонимание статики. статика это и есть эмулирование рантайм поведения в компайлтайме. смысл статики как раз в том что мы вкладываем в обьект в компайлтайме тонну лишнего смысла который нам нужен хотя в рантайме это просто сраный инт
что делать языкам без типов?
AZ
питухонам? сишке где f64 в языке ?расту?
G
Хорошо, а когда неименованные кортежи нужны, если есть именованные?
G
struct {
int x;
int y;
} point;VS
TUPLE(int, int) point;