Бартош Милевски - теория категорий

Самая лучшая вводная лекция по концепциям теории категорий - что такое категория, морфизм и уже из этой лекции можно сделать вывод, что такое функтор, монада, эндофунктор и моноид, и далее с лёгкостью двигаться по серии лекций о теории категорий.

https://youtu.be/p54Hd7AmVFU

Полный курс лекций — Category Theory:
https://www.youtube.com/playlist?list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_

Category Theory II:
https://www.youtube.com/playlist?list=PLbgaMIhjbmElia1eCEZNvsVscFef9m0dm

Links:
https://xn--r1a.website/technologique/1002

Бартош Милевски - правда о типах

Пожалуй лучшая лекция, раскрывающая понятие теории типов, систем типов и что такое тип, основываясь на очень простых концепциях теории категорий.

https://youtu.be/dgrucfgv2Tw

Наикрутейшая лекция о теории категорий применительно к практическому программированию от Филипа Вадлера, соавтора Haskell

https://www.youtube.com/watch?v=V10hzjgoklA

https://www.infoq.com/presentations/category-theory-propositions-principle/

https://www.youtube.com/watch?v=KyEHkUacXxQ

Есть виды типизированного лямбда исчисления (https://gist.github.com/andrcmdr/7121c3d9eb83f06785d8055a5c3604a3, https://xn--r1a.website/technologique/1002).
Если к ним применить теорию категорий - это уже будет конструктор для разработки различных систем типов.

Парадигм пограммирования много конечно, но все они сводятся к нескольким основным структурным парадигмам - структурной (процедуры/функции, модули, объекты/классы) и функциональной (лямбда функции (термы и типы) и категории). Или же по типу программ - к императивной и декларативной парадигме.

Сейчас всё идёт к ФП, потому что теория категорий предлагает более мощный структурный паттерн для создания программ, композиции типов данных и функций для их обработки, композиции систем типов и методов работы с типами, а также формальной верификации программ.

Если всё лямбда исчисление это всё про функции и данные, которые они принимают, про термы и типы, то вся теория категорий, применительно к программированию - это всё про композицию данных, объектов, множеств и функций, морфизмов над объектами, функторов над категориями, для их отображения, трансформации, верификации, отношений между ними, их композиции.

Типизированное лямбда исчисление и теория категорий - это очень мощные концепции в парадигме функционального программирования и именно за ними будущее всего пограммирования и всей IT отрасли.


Список литературы, статей и лекций - "Programming Language Theory":
http://steshaw.org/plt/
https://github.com/steshaw/plt

Дополнительные материалы:
Лекция Филипа Вадлера "Утверждения как типы" - https://www.youtube.com/watch?v=IOiZatlZtGU

Google выпустили Android 8 Oreo

Из основных новшеств: полная поддержка Instant Apps в Google Play, легковесная сборка платформы Android Go, поддержка Java 8 API (finally!) и языка Kotlin.

https://youtu.be/7kD0ZYzJbYo

Следующее поколение процессоров Intel, Coffee Lake, разрабатываемых по 14 nm техпроцессу, будет выпущено в октябре.

На видео есть пасхалка с подсказкой о дате выпуска на кружках с кофе. 😁👍

Не смотря на прежние технологические нормы в 14 нанометров для транзисторов Intel говорят о значительной оптимизации архитектуры, благодаря чему удалось повысить производительность чипов до 40 процентов относительно предыдущего поколения Kaby Lake и при этом значительно снизить их энергопотребление.

https://youtu.be/AAQuQh4dSgA?t=4m50s

Сегодня состоялся официальный релиз Go 1.9

Как всегда в очередной раз улучшены алгоритмы работы сборщика мусора (GOGC) - повышена производительность выделения и освобождения больших объектов в памяти кучи (heap) для приложений использующих очень большой невыгружаемый пул памяти (memory footprint) и очень большие кучи (heap size >50GB), хранящие много крупных объектов в памяти, что весьма хорошо для улучшения производительности in-memory кэширования и приложений in-memory баз данных написанных на Go.

Вызов функции runtime.ReadMemStats и подсчёт указателей в памяти теперь занимают меньше чем 100µs даже на очень больших кучах (heaps).

В run-time улучшен механизм inline подстановок кадров стэка вызова функций, что также повышает производительность работы с памятью.

В компиляторе Go теперь по умолчанию включена паралльельная компиляция, что значительно повышает скорость сборки и компиляции очень крупных проектов на многоядерных машинах.

Также улучшения коснулись самого языка - введены псевдонимы типов для улучшения возможностей рефакторинга.

Множество небольших улучшений сделано в инструментарии Go (Go toolchain) и стандартной библиотеке, с которыми можно более подробно ознакомиться в Release Notes.

https://blog.golang.org/go1.9

https://golang.org/doc/go1.9

https://github.com/golang/go/tree/release-branch.go1.9

http://talks.godoc.org/github.com/davecheney/go-1.9-release-party/presentation.slide#1

Links:
https://xn--r1a.website/technologique/1008
https://xn--r1a.website/technologique/750
https://xn--r1a.website/technologique/721

Видео с недавней конференции GopherCon 2017 с докладом Расса Кокса о будущем Go и грядущем релизе Go 2.0.

https://www.youtube.com/watch?v=0Zbh_vmAKvk

Данный доклад лёг в основу статьи Расса "На пути к Go 2.0" ("Toward Go 2.0"), которую мы публиковали в канале ранее — https://xn--r1a.website/technologique/1008.


#Go
#GoLang

Автор фреймворка Iris провёл достаточно интересный бенчмаркинг и сравнение платформы .Net и приложений на Go и Iris.

https://hackernoon.com/go-vs-net-core-in-terms-of-http-performance-7535a61b67b8

https://hackernoon.com/iris-go-vs-net-core-kestrel-in-terms-of-http-performance-806195dc93d5

Links:
https://xn--r1a.website/technologique/671

Новый рекламный ролик Lenovo к 25-летию серии Thinkpad о самом лучшем топовом бизнес лэптопе всех времён - ThinkPad X1 Carbon.
Показанное в этом году на CES2017 пятое поколение модели стало ещё лучше, мощнее, удобнее в использовании и главное - работа от одного заряда батареи достигла 24-х часов, т.е. целых суток!

Очень кинематографично и художественно снято! Именно такой должна быть реклама!

https://www.youtube.com/watch?v=z_0YhRac2tk

Links:
https://xn--r1a.website/technologique/914

Поддержку yield (для сопрограмм, итераторов и генераторов), сначала экспериментально, а теперь и полностью, внедрили в Rust на уровне языка и в RLS [Rust Language Server - реализация LSP сервера для Rust, для редакторов имеющих поддержку LSP (Language Server Protocol), например GNOME Builder и Visual Studio Code].

Поддержки async/await пока нет даже в планах (https://github.com/rust-lang/rust/pulls?q=async) и RFC, поэтому нет даже таких зарезервированных ключевых слов (https://doc.rust-lang.org/book/second-edition/appendix-01-keywords.html). Видимо пока оставили поддержку асинхронного кода на откуп библиотек.
Но если появилось ключевое слово yield то и реализация async/await не заставит себя долго ждать!

https://github.com/rust-lang/rust/pull/43076
https://github.com/dtolnay/syn/pull/186
https://github.com/rust-lang/rfcs/pull/2033
https://github.com/rust-lang/rust/issues/43122

https://github.com/rust-lang-nursery/rustfmt/pull/1928

https://github.com/rust-lang-nursery/rls/tree/rustfmt-yield


#Rust

Новый тизер "Blade Runner 2049" для ТВ (TV Spot) с интересными подробностями о фильме.

https://www.youtube.com/watch?v=tRcZ6yc1IMI

Плюс небольшое сюжетное отступление от фильма, "2036: Nexus Dawn", снятое Люком Скоттом (братом Ридли Скотта), с предисловием от рефиссёра Дэниса Вильнёва, о ранних событиях 2036 года, раскрывающее характер Ниандера Уоллеса (завладевшего обанкротившейся корпорацией Tyrell) и показывающее моральные возможности нового поколения репликантов Nexus 8, воссозданных им из прежних моделей Nexus 7.
Слабонервным и впечатлительным смотреть крайне не рекомендую.

https://www.youtube.com/watch?v=UgsS3nhRRzQ


#киберпанк
#cyberpunk

Первый трейлер третьего сезона сериала "Мистер Робот".

https://www.youtube.com/watch?v=EMK5e-FSro0

https://www.youtube.com/channel/UCX5R2xqZWND8nJqGTvel3nw

Осень обещает быть весьма интересной и богатой на премьеры!

Links:
https://xn--r1a.website/technologique/1038

Teaser - https://www.youtube.com/watch?v=CmtaZ8sOfbk

Trailer - https://www.youtube.com/watch?v=EMK5e-FSro0

Действительно интересная интерактивная GIS система для мониторинга и прогнозирования атмосферных процессов, разработанная чешской команией InMeteo.

25-26 августа по восточному побережью США прошёл тайфун Харви (Harvey).
10-12 сентября ожидается другой тайфун - Ирма (Irma), который по прогнозам пройдёт по штату Нью-Йорк.

Пример мониторинга и моделирования атмосферных течений над Атлантическим океаном:
https://www.ventusky.com/?p=27.2;-69.6;3&l=wind&t=20170910/06

Пример метрик температуры и атмосферных потоков в Средней Азии:
https://www.ventusky.com/?p=41.2;73.5;5&l=temperature&t=20170907/06


#GIS

Фреймворк Rocket для экосистемы Rust.

Сержио Бенитез, автор фреймворка Rocket на прошедшей 18-19 августа в Портлэнде (штат Орегон, США) конференции RustConf 2017.

https://youtu.be/t_FUZ34ahBE

https://rocket.rs

https://github.com/SergioBenitez/Rocket

Плэйлист видео с конференции:
https://www.youtube.com/watch?list=PL85XCvVPmGQhUSX_QBkxb4g1-o56cCqI9&v=COrl851gMTY

Расписание Rust конференций:
https://blog.rust-lang.org/2017/07/18/conf-lineup.html


Links to the latest posts about Rust:
https://xn--r1a.website/technologique/1063
https://xn--r1a.website/technologique/1061


#Rust

Дорогие друзья и подписчики канала @Technologique!

Наступила осень и нас уже почти три сотни человек! Это довольно много! Для нас и меня лично это серьёзный рубеж и определённая ответственность перед читателями!
Создавая канал в январе 2016 года согласно своим интересам в программировании и желанию реализации своих мыслей и взглядов в этой области, для обмена информацией с близкими мне друзьями, я никогда не думал, что это превратится во что-то более серьёзное и канал будет существовать так долго. Но время доказало обратное и я этому рад.

Мы любим читать, смотреть и любим качественный контент.
Мы любим новые технологии, любим экспериментировать, изучать и постигать их.
Мы любим и уважаем своих читателей, и стараемся держать планку качества канала, материалов и публикаций на должном уровне, и будем её только повышать.

Надеюсь вам нравится наш канал, его тематика и публикации!
Спасибо что вы с нами, для нас это большая мотивация продолжать писать и возможность двигаться дальше вместе!

С уважением, редакционная команда канала @Technologique.

В Telegram очень много интересных каналов, которые мы любим читать, освещающих интресующие нас и любимые нами темы - программирование, интернет и связь, технологии и наука, математика, физика, космические технологии, философия, психоанализ, искусство, кино (особенно киберпанк), литература (особенно sci-fi).
Всех тем не перечесть!
Но в данном канале мы освещаем только технологии программирования и разработки софта, концепции языков программирования, современные тренды и формирующиеся экосистемы разработки, т.к. мы спецализируемся в этом деле и делаем это хорошо.

Но охват лишь одной темы ограничивает кругозор, поэтому я хотел бы возобновить рекомендации интересных каналов, которые мы читаем.
Такие публикации будут под хэш-тегом #channels.

Интервью Райана Дала, автора Node.js.

В интервью Райан Дал был предельно откровенен и признался, что понял и глубоко осознал, что серверное однопоточное программирование на Node.js это не лучший выбор, поэтому он покинул этот проект.

https://www.mappingthejourney.com/single-post/2017/08/31/Episode-8-Interview-with-Ryan-Dahl-Creator-of-Nodejs

Аудиозапись интервью:
https://soundcloud.com/pramod-shashidhara/episode-8-interview-with-ryan-dahl-creator-of-nodejs

Я думаю, что сейчас уже многим понятно, что Node.js не является технически или инженерно совершенным решением в текущих современных условиях серверных приложений, реализация движка V8, JIT компилятора JavaScript для платформы Node.js, является однопоточной, но prefork мультипроцессной, т.е. с process pool'ом, но не thread pool'ом с поддержкой M:N mapping'а потоков на системные треды, что только повышает накладные расходы из-за использования системных вызовов ядра, поэтому использование Node.js для создания многопоточных сетевых приложений и серверов является не лучшим решением в большинстве случаев.
При этом это проблема только языковой исполнительной среды, как и в Python и в Ruby, но не проблема самого языка — стандарт ECMAScript 8 значительно упразднил многие проблемы в языке и сделал его более приятным.

Idris - язык чистого тотального функционального программирования.

Изучая функциональное программирование, виды типизированного лямбда исчисления, теорию категорий, мне стало интересно, есть ли уже или появится ли в ближайшие годы какой-нибудь язык ФП, который реализует более полно теорию категорий и исчисление конструкций (зависимые типы) для более широких масс в более практически применимой форме, не такой язык, какие есть сейчас, более практическая альтернатива текущим популярным ФП языкам, которые на данный момент представляют лишь исследовательский и академический интерес, всё же Haskell остаётся весьма маргинальным языком.

После определённых поисков и изучения области знаний выяснилось, что на самом деле такие языки уже есть, при том появились они совсем недавно, в конце нулевых, начале десятых годов, имея богатую генеалогию предшественников (ALF, Cayenne, Epigram, Lean, Clean).

Это языки Agda и её последователь Idris.

Idris как более практический язык для реального применения в разработке представляет больший интерес.
Как и OCaml, Idris может использоваться для создания статических анализаторов, верификации и валидации программ, escape анализа программ, исследования и создания новых систем типов и компиляторов для новых языков, использующих математическое доказательство завершённости программ для создания более безопасного программного обеспечения, а также для метапрограммирования DSL языков.

https://vimeo.com/62037963

Канал с видеолекциями автора языка, Эдвина Брэди:
https://vimeo.com/user16996198

Курс программирования на Idris:
https://www.idris-lang.org/dependently-typed-functional-programming-with-idris-course-videos-and-slides/

Отличная книга по языку:
https://www.manning.com/books/type-driven-development-with-idris

Idris has a priority on easy management of side-effects.

Контроль побочных эффектов в Idris подобен механизмам языка OCaml - можно всё писать в чисто функциональном стиле без сайдэффектов, но когда они действительно нужны (например для сетевых приложений, работы с сокетами) можно их использовать, без особых заморочек с монадами и функторами (как в Haskell). В общем все side-effects контролируемые (side-effect control, effect system).

https://github.com/idris-lang/Idris-dev/tree/master/libs/effects

http://docs.idris-lang.org/en/latest/effects/index.html

https://www.idris-lang.org/documentation/effects/

Мне нравится, что Idris это один из современных языков (наряду с его предшественником - Agda), который поддержвает strong functional programming (иначе total functional programming - это как раз то, что я искал!), использует eager/strict evaluation наряду с поддержкой lazy evaluation (ленивые вычисления тоже контролируемые, что хорошо - можно их использовать, но язык по умолчанию использует strict evaluation) и использует систему зависимых типов (dependent types, с исчислением конструкций - типизированным лямбда исчислением высших порядков), которое базируется на теории типов Мартина-Лёфа (Martin-Löf type theory, см. документацию - https://github.com/idris-lang/Idris-dev/wiki) и унифицированную теорию зависимых типов (unified theory of dependent types).

Более того язык обладает системой уникальных типов (uniqueness types), подобной субструктурной системе линейных типов (sub-structural linear type system) для обеспечения безопасности любого ввода вывода - работы с памятью, указателями, многопоточностью, сетевым стэком и т.д.

http://docs.idris-lang.org/en/latest/reference/uniqueness-types.html

They are inspired by linear types, Uniqueness Types in the Clean programming language, and ownership types and borrowed pointers in the Rust programming language.

Очень советую изучить Idris.
Idris понравился мне даже больше чем OCaml и конечно больше чем Haskell по своим концепциям.

https://www.idris-lang.org

https://github.com/idris-lang/Idris-dev

Есть бэкэнд компиляторы (кодогенераторы) под различные платформы:
https://github.com/idris-hackers