Я могу воспроизвести, но это не по профилю чата

Грубо говоря, в этой модели берём последовательности Коши рациональных чисел, на них вводим класс эквивалентности ("разность последовательностей сходится к нулю"), дальше доказываем, что на этих классах эквивалентности верны все аксиомы поля, есть полнота и архимедовость

Построение настолько простое, что можно давать не только на мехматах и в ФМШ

каждый класс эквивалентности - вещественное число

Вообще эта процедура называется пополнение. Тут одна тонкость надо будет ввести сходимость для рациональных чисел, вещественных ещё нет поэтому расстояние между числами придётся мерять рациональными

И классы содержащие константные последовательность отождествляются с рациональными числами

Да, конечно. Я ж предупредил - "грубо говоря" =) Тонкости я намеренно оставил за кадром

не так уж просто для школьников получается

Вообще эта процедура называется пополнение. Тут одна тонкость надо будет ввести сходимость для рациональных чисел, вещественных ещё нет поэтому расстояние между числами придётся мерять рациональными

Сходимость в себе же forall epsilon exist N. forall n>N, m>N |a_n - a_m| < epsilon

Да, но какого типа epsilon? Только рационального

Вообще, ЕМНИП, полноценно модель вещественных чисел школьникам дают в ФМШ и, возможно, в профильных классах (я думаю, что всё-таки нет). Обычно её дают на первом курсе ММФ, ФФ и ЭФ, остальным факульеттам только поверхностно

Просто обычно |a_n - a_m| понимают как действительные числа

+ это последовательность Коши, а она непременно имеет предел только в полных пространствах

+ это последовательность Коши, а она непременно имеет предел только в полных пространствах

Так тебе это и нужно

+ это последовательность Коши, а она непременно имеет предел только в полных пространствах

Собственно, полные пространства через это свойство и определены=)

Ты рассматриваешь классы эквивалентности сходящихся в себе последовательностей коши

И тем самым пополняешь Q

Собственно, полные пространства через это свойство и определены=)

Ну да

про школы, я понимаю в АГ, ФМШ, 239, возможно 40 (про Питер) это дают

В юмш дают

Но это бывшее матнаправление аг

про школы, я понимаю в АГ, ФМШ, 239, возможно 40 (про Питер) это дают

В ФТШ, если память не изменяет, тоже было

Хм, как коррелирует обучение в матшколе и хаскелизм?

положительно наверняка

матшкола должна коррелировать с программированием

в школах не учат типам

из моего класса только один человек пишет на Haskell, насколько я знаю

возможно ещё человека три в курсе, что это такое

тот что с @swamp_agr работает - точно в курсе должен быть

из моего класса только один человек пишет на Haskell, насколько я знаю

это же офигенный результат

Ну меня интересует обратная зависимость

то есть корреляция есть и нехилая

обратная зависимость должна быть

многие могут в олимпиадные программинг уходить

Я могу назвать как минимум двух моих одногодок-хаскелистов из 30'ки

а там Haskell не очень ценят

в школах не учат типам

Я пытался подать информацию по типам.

У меня в классе вроде хаскелистов не было. Один раст-фаг есть

В принципе, программа позволяет давать в школе информацию про типы.

ну в классе у нас были паскалисты и сишники

но в 2004 хаскель был так себе

Я пришёл узнал про хаскель в 11'ом классе от L29Ah и тогда более или менее живые гайды были только про хугс

> L29Ah Знакомые всё лица!

Тов. Евгений, а не были ли в жаббере в концеренциях?

А уже на втором курсе после Standard ML'я мигрировал на ghc

elemir же

Можно было и на ник в ТГ посмотреть

Ох, не, не помню elemir. Видимо, в конфах не пересекались. =)

/me больше всё же в codingteam@cjr сидел

Я сначала обитал в anime-talks (при том, что аниме не смотрел), а потом в gentoo@cjr. Ещё в psiplus-dev жил на первом курсе

Бля, это же не _blah

@qnikst, что вы тут развели? :(

у всех есть 5 минут на то чтобы прочитать и почерпнуть интересное

5 минут примерно равно одной минуте

да удалять-то смысла нет же

если уже написано, то многие и прочитают, а остальные все равно пропустят ну типа флуд нужно предотвращать заранее, а удалять потом уже как-то малополезно, куда полезней уже оставить, чтобы был какой-то конткент интересный (он там есть)

из моего класса только один человек пишет на Haskell, насколько я знаю

класса в какой терминологии?

школьной

кстати, а в хаскеле кто нибудь таким пользуется? http://hackage.haskell.org/package/effect-handlers

freer и extensible-effects люди пользуются

не часто правда

я просто только сегодня узнал про алгебраические эффекты и парень, от которого я это узнал, сказал, что в хаскеле их нет

но судя по всему они есть в виде библиотек, так?

они не встроены прямо в язык, в отличие от PureScript

или может это какие-то "неправильные" алгебраические эффекты?

ну то что есть в Eff изоморфно Monads и ирансформерам

на что есть статья Wadler

в пурс же row-типы встроены, а не эффекты

https://doi.org/10.1145/289423.289429

просто в ленивом языке эффекты это немного печаль

со встроенными эффектами -- это Koka, я правда, честно скажу, не смотрел

и.к. за контролем за стейтом нужна супермонада в которой эффекты будут кодироваться

ну то что есть в Eff изоморфно Monads и ирансформерам

значит ли это что первое не лучше второго, а второе не лучше первого?

и значит все должны дружно переписать свой код

ну первое проще в строгих языках, второе в ленивых

но при желании одно можно выразить через другое

или Eff еще есть

и.е. они одинаковые по мощности, но в практическом применении "лучше" обычно про удобство использования

в той статье Eff как пример языка с эффектами

я осилил вступление пару глав и заключение