Pull to refresh
38
0
Роман Кашицын @roman_kashitsyn

Пользователь

Send message
Не, поймите, я сам иногда мечтаю об анонимных неявных тайпклассах в хаскеле.

Наверное, вы хотите просто записи с Row Polymorphism.

Программисты нужны не для того, чтобы хорошо знать «TypeScript», а чтобы уметь эффективно решать проблемы. Этот навык приходит исключительно с опытом и изучением фундаментальных наук (математика, логика, алгоритмы).


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


Я изучил C# и .NET с разными областями применения (asp.net, wpf, xamarin), js/ts (react/redux, node) и убедил себя, что теперь-то могу действительно всё.

Это что ли много?


Learn at least a half dozen programming languages. Include one language that emphasizes class abstractions (like Java or C++), one that emphasizes functional abstraction (like Lisp or ML or Haskell), one that supports syntactic abstraction (like Lisp), one that supports declarative specifications (like Prolog or C++ templates), and one that emphasizes parallelism (like Clojure or Go).
http://norvig.com/21-days.html

Я бы добавил к этому списку языки, которые обладают выразительной модульной системой (OCaml, Standard ML) и языки, которые помогают осознать соответствие Карри—Ховарда: Coq, Agda, Idris или F*.


Однажды я зафигачил дизайн на абстрактных классах в typeScript, и меня высмеяли. Потому что в тайпскрипте» так не делают.

А кого волнует, что там кто делает или не делает в «TypeScript»? Надо уметь обосновать выбор дизайна. Идиоматичность дизайна является одним из факторов (к примеру, в математике никто не будет обозначать целое число буквой большой буквой S), но если преимущества (простота в поддержке, эффективное использование ресурсов, лёгкость в отладке) «неидеоматичного» решения перевешивает недостатки, аргумент «так никто не делает» выглядит довольно нелепо.

Вы забыли про правила вывода.

Под "законами логики" я имел ввиду исчисление предикатов и логика высших порядков, о каких именно "правилах вывода" вы говорите? Мат. индукция? Это частный случай исчисления предикатов.

А доказательства этих теорем — конечные последовательности правил

Нет, правила — это логика + набор аксиом. Доказательства — это последовательные применения законов логики к аксиомам для получения требуемого результата.


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


Когда-нибудь всё везде будет строго доказываться на аналоге Coq, вот тогда ваш тезис будет совсем верным.

В математике чтение учебника — это и есть выполнение упражнений

Нет.


Я прочитал много книжек по математике и программированию, и совершенно уверен, что просто чтение не работает, в голове не остаётся совершенно ничего.


Кмк, лучше всего начинать сразу с задач, и читать учебник, чтобы понять в чём заключается проблема и как её решить.
Недавно пробовал такой подход с топологией. Берёшь задачи-теоремы, которые нужно доказать, и читаешь ровно столько учебника, сколько нужно, чтобы всё доказать/решить.


Вот тогда реально хорошо понимаешь материал.

В математике ученые формулируют утверждения вида: "из последовательности символов А при помощи последовательного применения правил преобразования Х можно получить последовательность символов В".

Это только в конструктивной математике. Вообще говоря, много утверждений вида "существует объект, обладающий свойством P" или, выражаясь вашими словами "как не крути правила X, последовательность B из A ты получить не сможешь" (обычно эти теоремы самые важные и сложные).


Примеры:


  • У любого полинома n-степени с комплексными коэффициентами (n≥1) существует хотя бы один комплексный корень (ни слова про то, как его найти).
  • Для любого n ≥ 5 не существует формулы, которая бы выражала корни любого полинома степени n в радикалах.
  • Всякое n-мерное многообразие гомотопически эквивалентно n-мерной сфере тогда и только тогда, когда оно гомеоморфно ей (когда я наконец понял разницу между гомотопиями и гомеоморфизмами, мне это крышу снесло).
вообще, фихтенгольц — это простейшая книга по матану, где всё разжёвывается до мелочей и читателя просто закидывают разнообразными примерами, настолько приближенными к практике, насколько это возможно

Подтверждаю. Я на втором курсе перечитывал этот учебник (начались диффуры, хотелось ещё раз подтянуть матчасть). Он читается как художественная литература. У меня до сих пор дома тома стоят, так и тянет ещё раз почитать.


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


Особенно полезно самому выводить формулы, после этого их уже не нужно помнить, можно помнить только ключевую идею. Более того, вывод формул может приносить огромное удовольствие, ведь каждый раз это как маленькое открытие.

Что, Гриша, тоскуешь по Яндексу? О чём статья-то? Я ничего не понял.


P.S. А, это ответ на другую статью, которая тоже ни о чём. Извини тогда. Как тебе Erlang после C++?

Добавлю также про сильно искажённые факты


К слову, и Reason / Ocaml не поддерживают multi-core, для этого есть Lwt.

Lwt не для multi-core, а для concurrent programming! Вот что написано в оригинальной статье:


Native Reason/OCaml doesn’t have multi-core support yet, but for doing concurrent processes you can use Lwt, which is a promise-like library.

От себя добавлю, что есть похожая библиотека Async, которой посвящена глава в Real World OCaml. Хотя Lwt гораздо более популярена, основные принципы одинаковы.

Скобки здесь при том, что это синтаксический рудимент Лиспа

Скобки — это не рудимент, это преимущество лиспа. Поначалу они действительно кажутся неудобными, но стоит лишь перестроиться и начать думать "сбалансированными выражениями" вместо символов и строк, работать с кодом становится гораздо удобнее, и современные плагины для работы с Lisp (paredit, lispy) сильно помогают. Они превращают редактор текста в редактор синтаксического дерева программы. Вот небольшое демо с демонстрацией базовых возможностей paredit.


После работы с Lisp начинаешь думать по-другому и в других языках: я в основном пишу на C++ в Emacs, и работа со "сбалансированными выражениями" прочно засела в моём workflow.

зачем писать на LISP, и что писать на LISP?

Common Lisp – очень неплохо спроектированный язык. Да, в стандарте есть несколько моментов, которые сейчас не особо актуальны, но в целом язык очень интересный. Честно говоря, я с трудом переношу языки с динамической типизацией (Python и JavaScript снятся мне в кошмарах), но на CL я бы с удовольствием попробовал написать проект.
Для CL есть качественные компиляторы, в языке есть возможность указать типы, если хочется (да, аналог gradual typing был давным давно). Код, который генерит, к примеру, SBCL, на удивление быстр (я сабмитил решения для computer language benchmark game, мой код для SBCL иногда работает ощутимо шустрее, чем мой код для Haskell, оба решения были в топе).


Slime + Emacs – это приятная и мощная среда разработки, в которую вложено много человеко-лет труда. Её действительно иногда нетривиально настроить (нужно разобраться в терминологии, ASDF, системы, вот это всё). К примеру, компиляция совершенно не мешает разработке, ведь можно инкрементально компилировать код по одной функции за раз. При этом можно попросить компилятор показать ассемблерный код любой функции и посмотреть, как добавление аннотаций типов влияет на код, производимый компилятором.


Ну и если в проекте нужна генерация кода, CL тут просто вне конкуренции.


Единственное, что я бы не стал писать на CL – мелкие утилиты командной строки. Модель исполнения с тяжёлым долго-живущим образом не особо к этому располагает.


К слову, у языка довольно много активных пользователей.  Например, бэкэнд ITA (ныне Google Flights) в значительной степени написан на CL.

а что с mangling'ом?

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

Там почти нет темплейтов в API, поэтому манглинга нет.

В С++ манглится всё, что не extern "C", независимо от наличия шаблонов.

Кстати, вставку символов по именам в TeX можно получить в любом моде Emacs через
M-x set-input-method TeX

К Ruby — тривиальная задача, если использовать Helix.

Это не означает, что Rust какой-то особенный. Для C++ тоже давно существуют аналоги: CLIF и SWIG.

Ну так а чем тогда растовый FFI сильно проще плюсового?

Вот тут пример небольшой есть

Там владение объекта не передаётся в сторонний код. Сторонний код видит только указатель на объект, создаваемый и уничтожаемый в rust. Если стороннему коду нужно создавать и уничтожать экземпляры RustObject, нужно написать функции-обёртки для конструктора и деструктора. Один-в-один как в C++.

Попрошу минусующих показать, как вызвать из C rust-функцию, возвращающую Result<Resource, Error> без написания специальных сишных обёрток. C++ исключения — это проблема, но как вы убеждаетесь, что panic! не прилетит из глубин сторонней библиотеки, которой вы пользуетесь? Может, так? Чем это отличается от catch(...)?


Я ничего не имею против Rust, мне просто непонятно, как принципиальные семантические проблемы могут решиться сами собой при смене языка на аналогичный.

Код возврата это просто Union, проблем с ним нет.

Что значит "проблем с ним нет"? Обёртки для си всё равно писать надо. Что если в этом юнионе объекты с деструкторами лежат? Если нужно писать обёртки, то и в плюсах можно написать catch(...) и конвертировать исключения в коды возврата.

А что с классами из с++ делать?

А что делать с RAII-структурами в Rust?


И что делать с исключениями с++ вобще не понятно

Ловить вcё в сишных обёртках и конвертировать в коды возврата. С растовыми статусами этого не придётся делать?

Information

Rating
Does not participate
Location
Zürich, Zürich, Швейцария
Date of birth
Registered
Activity