Ct
Затем чтобы апи его фреймворка меньше стреляло по ногам, например.
Для этого инженеры для инженеров придумали best practices. Теория типов тут немного сбоку, ее все еще необязательно знать, чтобы этими best practices пользоваться.
Size: a a a
2020 August 10
DF
А потом визитор на 400 строк
BD
Лол, если он считает, что в теории типов тип - это множество, то это точно значит, что он ничего в ней не понимает.
В том числе ради чего она вообще появилась изначально
В том числе ради чего она вообще появилась изначально
он как обычно открыл первую главу Бартоша и такой “ок, множества, стрелки, я понял, говно, обосраться, дошколята"
DF
Кек
DF
Ну на самом деле это всё довольно несложные области
DF
Просто они развиты и требуют длительного изучения
DF
Но каких то фантастических вещей там нет
p
BD
Dollar Føølish
Но каких то фантастических вещей там нет
до 4 или пятой главы нет, а дальше конечно опять начинается “как всем досконально известно, ..."
DF
Очевидно, что
SP
так еще раз:
У математиков чтото не складывалось с теорией множеств, и пацаны придумали некуд "теорию типов". это работало строго как разрешение противоречий в терках математиков относительно теории множеств в вопросах "считать ли пустое множество членом пустого множества"
потом почему то ктото приплел туда лямбда исчисление и теорию категорий(теория категорий кстати слеплена из абстрактной алгебры которую я понял лучше все кукаретики в интернете говорят "ну оно похоже но просто теоркат звучит солиднее и хомячки ведутся лучше")
далее просто интуитивной понятной вещи типа map придается какой то сокральный смысл и на основе похожести того что он делает на "морфизм" все эти раковые теории приплетаются как обязательные, на чем строится все программирование.
но программирование строится не на этом.
обьектом любой науки о кодочмырении будет то как человеку удобно писать код: том что считать типом а что значением, как можно использовать конструкторы в качестве фильтров для типов, и прочего прочего
У математиков чтото не складывалось с теорией множеств, и пацаны придумали некуд "теорию типов". это работало строго как разрешение противоречий в терках математиков относительно теории множеств в вопросах "считать ли пустое множество членом пустого множества"
потом почему то ктото приплел туда лямбда исчисление и теорию категорий(теория категорий кстати слеплена из абстрактной алгебры которую я понял лучше все кукаретики в интернете говорят "ну оно похоже но просто теоркат звучит солиднее и хомячки ведутся лучше")
далее просто интуитивной понятной вещи типа map придается какой то сокральный смысл и на основе похожести того что он делает на "морфизм" все эти раковые теории приплетаются как обязательные, на чем строится все программирование.
но программирование строится не на этом.
Объект науки - те явления, которые она изучает. Предмет - то, что интересует данную науку в конкретном объекте.
обьектом любой науки о кодочмырении будет то как человеку удобно писать код: том что считать типом а что значением, как можно использовать конструкторы в качестве фильтров для типов, и прочего прочего
BD
так еще раз:
У математиков чтото не складывалось с теорией множеств, и пацаны придумали некуд "теорию типов". это работало строго как разрешение противоречий в терках математиков относительно теории множеств в вопросах "считать ли пустое множество членом пустого множества"
потом почему то ктото приплел туда лямбда исчисление и теорию категорий(теория категорий кстати слеплена из абстрактной алгебры которую я понял лучше все кукаретики в интернете говорят "ну оно похоже но просто теоркат звучит солиднее и хомячки ведутся лучше")
далее просто интуитивной понятной вещи типа map придается какой то сокральный смысл и на основе похожести того что он делает на "морфизм" все эти раковые теории приплетаются как обязательные, на чем строится все программирование.
но программирование строится не на этом.
обьектом любой науки о кодочмырении будет то как человеку удобно писать код: том что считать типом а что значением, как можно использовать конструкторы в качестве фильтров для типов, и прочего прочего
У математиков чтото не складывалось с теорией множеств, и пацаны придумали некуд "теорию типов". это работало строго как разрешение противоречий в терках математиков относительно теории множеств в вопросах "считать ли пустое множество членом пустого множества"
потом почему то ктото приплел туда лямбда исчисление и теорию категорий(теория категорий кстати слеплена из абстрактной алгебры которую я понял лучше все кукаретики в интернете говорят "ну оно похоже но просто теоркат звучит солиднее и хомячки ведутся лучше")
далее просто интуитивной понятной вещи типа map придается какой то сокральный смысл и на основе похожести того что он делает на "морфизм" все эти раковые теории приплетаются как обязательные, на чем строится все программирование.
но программирование строится не на этом.
Объект науки - те явления, которые она изучает. Предмет - то, что интересует данную науку в конкретном объекте.
обьектом любой науки о кодочмырении будет то как человеку удобно писать код: том что считать типом а что значением, как можно использовать конструкторы в качестве фильтров для типов, и прочего прочего
с двача чтоль?
SP
с двача чтоль?
сам только что написал, есть че сказать по теме?
p
нет, я это я
у тебя же wip https://github.com/teloxide/teloxide/pull/256 висит
DS
@DogeShibu а можно определение типа согласно теории типов? мне интересно насколько оно вообще оторвано от реального мира. я просто не могу найти
Тебе согласно какой теории типов?
Так это очень уж общее определние выходит.
Обычно под этим подразумевается какая-то конструкция, которую ты можешь указать для каждого терма своего языка согласно данным правилам типизации.
А лучше вот сюда: https://ncatlab.org/nlab/show/type+theory
Так это очень уж общее определние выходит.
Обычно под этим подразумевается какая-то конструкция, которую ты можешь указать для каждого терма своего языка согласно данным правилам типизации.
А лучше вот сюда: https://ncatlab.org/nlab/show/type+theory
DS
так еще раз:
У математиков чтото не складывалось с теорией множеств, и пацаны придумали некуд "теорию типов". это работало строго как разрешение противоречий в терках математиков относительно теории множеств в вопросах "считать ли пустое множество членом пустого множества"
потом почему то ктото приплел туда лямбда исчисление и теорию категорий(теория категорий кстати слеплена из абстрактной алгебры которую я понял лучше все кукаретики в интернете говорят "ну оно похоже но просто теоркат звучит солиднее и хомячки ведутся лучше")
далее просто интуитивной понятной вещи типа map придается какой то сокральный смысл и на основе похожести того что он делает на "морфизм" все эти раковые теории приплетаются как обязательные, на чем строится все программирование.
но программирование строится не на этом.
обьектом любой науки о кодочмырении будет то как человеку удобно писать код: том что считать типом а что значением, как можно использовать конструкторы в качестве фильтров для типов, и прочего прочего
У математиков чтото не складывалось с теорией множеств, и пацаны придумали некуд "теорию типов". это работало строго как разрешение противоречий в терках математиков относительно теории множеств в вопросах "считать ли пустое множество членом пустого множества"
потом почему то ктото приплел туда лямбда исчисление и теорию категорий(теория категорий кстати слеплена из абстрактной алгебры которую я понял лучше все кукаретики в интернете говорят "ну оно похоже но просто теоркат звучит солиднее и хомячки ведутся лучше")
далее просто интуитивной понятной вещи типа map придается какой то сокральный смысл и на основе похожести того что он делает на "морфизм" все эти раковые теории приплетаются как обязательные, на чем строится все программирование.
но программирование строится не на этом.
Объект науки - те явления, которые она изучает. Предмет - то, что интересует данную науку в конкретном объекте.
обьектом любой науки о кодочмырении будет то как человеку удобно писать код: том что считать типом а что значением, как можно использовать конструкторы в качестве фильтров для типов, и прочего прочего
А, ну полное непонимание глубоких связей математики со всем.
DS
Что и ожидалось
N
у тебя же wip https://github.com/teloxide/teloxide/pull/256 висит
Я его починила