1:07:23 зависимые типы - это вообще большая история. Имеющая, кстати, сильную связь с основаниями математики и типизированным лямбда исчислением (см. полиморфизм Карри-Говарда). Кроме Idris, сюда ещё относятся Agda и Coq. Крутость же зависимых типов в том, что они позволяют выражать в типах контракты произвольной сложности. Классический пример - это тип "сортированный массив длинны n". И соответственно, если функция принимает тип "массив длинны n", а возвращает тип "сортированный массив длинны n", то можно уже не пытаться покрыть все возможные варианты входов и выходов, чтобы убедиться, что в ней нет багов, из-за которых она может вернуть несортированный массив, т.к. теперь это гарантируется системой типов. Кроме того, в них можно описывать доказательства различных фактов так, чтобы система типов гарантировала их корректность - если некоторое утверждение (теорема) является типом для некоторой программы, то эта программа и есть доказательство данного утверждения. В частности, если для примера выше с функцией, которая делает из массива сортированный, если мы ещё докажем, что она всегда возвращает массив из тех же элементов, что и исходный, то можно будет быть уверенными, что она является функцией сортировки. Но есть с ними пока и проблема: ими пока довольно сложно пользоваться, и даже простые факты бывает непросто и довольно громоздко доказывать. Так что есть куда расти науке)
Мне кажется, что пример чисел Фибоначчи на Схеме (21:20) выглядит излишне сложным из-за применённой оптимизации. Может быть стоило показать не оптимальный, но более красивый вариант?: (define (fib n) (if (< n 2) n (+ (fib (- n 1)) (fib (- n 2))))) Его, кстати, не сложно сделать достаточно эффективным, добавив в нужном месте мемоизацию
@@markshevchenko тоже уже потом подумал, что немного поменял задачу. Но тогда можно питонячий вариант переписать, как я выше пнаписал. Будет максимально близко к остальным по коду, производительности и формату вывода
6:35 Не совсем понял, как общая память для данных и программ вынуждает появление процессорных кэшей. Ведь от них была бы ровно такая же польза, даже если бы для данных и программ использовались раздельные хранилища с доступом по отдельным шинам - только кэшей бы тогда тоже понадобилось в два раза больше)
Как я понимаю, это просто усугубляет ситуацию, потому что на шину нагрузка выше. Но какие есть альтернативы такому решению я не знаю, это надо с аппаратчиками пообщаться. :)
@@markshevchenko собственно, будь там два отдельных хранилища - нужно было бы две шины, и если хочется расширить шину, то тоже можно её сделать вдвое шире. Хотя там дальше начнутся проблемы с синхронизацией, которых бы с раздельными хранилищами не было
Спасибо. Слушаем и смотрим 😎
1:07:23 зависимые типы - это вообще большая история. Имеющая, кстати, сильную связь с основаниями математики и типизированным лямбда исчислением (см. полиморфизм Карри-Говарда). Кроме Idris, сюда ещё относятся Agda и Coq. Крутость же зависимых типов в том, что они позволяют выражать в типах контракты произвольной сложности. Классический пример - это тип "сортированный массив длинны n". И соответственно, если функция принимает тип "массив длинны n", а возвращает тип "сортированный массив длинны n", то можно уже не пытаться покрыть все возможные варианты входов и выходов, чтобы убедиться, что в ней нет багов, из-за которых она может вернуть несортированный массив, т.к. теперь это гарантируется системой типов. Кроме того, в них можно описывать доказательства различных фактов так, чтобы система типов гарантировала их корректность - если некоторое утверждение (теорема) является типом для некоторой программы, то эта программа и есть доказательство данного утверждения. В частности, если для примера выше с функцией, которая делает из массива сортированный, если мы ещё докажем, что она всегда возвращает массив из тех же элементов, что и исходный, то можно будет быть уверенными, что она является функцией сортировки.
Но есть с ними пока и проблема: ими пока довольно сложно пользоваться, и даже простые факты бывает непросто и довольно громоздко доказывать. Так что есть куда расти науке)
Каноничный пример на Питоне (32:16) очень похоже записывается в Clojure (только без мутации переменных):
(defn fib [n]
(loop [i 0, a 0, b 1]
(when (
Мне кажется, что пример чисел Фибоначчи на Схеме (21:20) выглядит излишне сложным из-за применённой оптимизации. Может быть стоило показать не оптимальный, но более красивый вариант?:
(define (fib n)
(if (< n 2) n
(+ (fib (- n 1))
(fib (- n 2)))))
Его, кстати, не сложно сделать достаточно эффективным, добавив в нужном месте мемоизацию
Там всё-таки везде другая задача, напечатать первые 20 чисел Фибоначчи. На всех языках реализована она.
@@markshevchenko тоже уже потом подумал, что немного поменял задачу. Но тогда можно питонячий вариант переписать, как я выше пнаписал. Будет максимально близко к остальным по коду, производительности и формату вывода
6:35 Не совсем понял, как общая память для данных и программ вынуждает появление процессорных кэшей. Ведь от них была бы ровно такая же польза, даже если бы для данных и программ использовались раздельные хранилища с доступом по отдельным шинам - только кэшей бы тогда тоже понадобилось в два раза больше)
Как я понимаю, это просто усугубляет ситуацию, потому что на шину нагрузка выше. Но какие есть альтернативы такому решению я не знаю, это надо с аппаратчиками пообщаться. :)
@@markshevchenko собственно, будь там два отдельных хранилища - нужно было бы две шины, и если хочется расширить шину, то тоже можно её сделать вдвое шире. Хотя там дальше начнутся проблемы с синхронизацией, которых бы с раздельными хранилищами не было
Ссылка на слайды ведёт вникуда(
Видимо, привязал слайды к другому посту. Исправляю, правильная ссылка markshevchenko.pro/2021/11/19/history-of-programming/