• Haskell. Монады. Монадные трансформеры. Игра в типы
    +1
    Ну да. Можно реализовать частный случай. Но написать обобщенную функцию для произвольной монады, как в hakell, уже не получится. Например, не получится написать функцию типа
    filterM :: Monad m => (a -> m Bool) -> [a] -> m [a]
    
  • Haskell. Монады. Монадные трансформеры. Игра в типы
    +2
    Мне кажется, проблема в системе типов. Система типов обычных языков, типа C#, просто не позволяет делать такие выкрутасы, которые позволяет система типов Haskell.
    Допустим, есть класс типов Monoid
    class Monoid a where
       mempty :: a
       mappend :: a -> a -> a
    


    Я могу «эмулировать» его в C# с помощью интерфейса
    interface Monoid<A>
    {
    	A mempty();
    	A mappend(A a1, A a2);
    }
    

    Затем я могу сделать instanse моноида для конкретного типа с помощью наследования
    class IntMonoidInstance: Monoid<int>
    {
    	int mempty(){ .. }
    	int mappend(int a1, int a2) { .. }
    }
    


    Но этот фокус не сработает для монады.
    Класс типов монады объявлен как
    class Monad m where
       return :: a -> m a
       (>>=) :: forall a b . m a -> (a -> m b) -> m b
    

    Здесь m является не просто типом, как в случае с моноидом. Она является типом, параметризированным другим типом. Другими словами: * -> *.
    Интерфейс для монады в C# должен выглядеть примерно так
    interface Monad<M> where M: * -> *
    {
    	M<A> return<A>();
    	M<B> bind<A, B>(M<A> a1, Func<A, M<B>> a2);
    }
    

    Но C# со своей мощной системой типов не позволяет делать такие штуки. Я не могу объявить интерфейс, параметризированный типом, который параметризирован другим типом.
    Любые реализации монады в C# все равно останутся недо-монадой.
  • Haskell. Монады. Монадные трансформеры. Игра в типы
    +3
    Я с вами категорически не согласен. Я утверждаю, что новичок нуждается в «магии». Если перегружать новичка деталями, то это его еще больше запутает. Я сознательно упустил математическую строгость в пользу понятности.
    Поэтому моя статья написана именно в таких терминах и именно на новичков она и рассчитана.
  • Haskell. Монады. Монадные трансформеры. Игра в типы
    +1
    Я думал об этом. Coq я люблю. Только эта тема не очень востребована.
  • Почему земляне делают глючный софт и железо
    0
    По-моему, верификация hardware — это вообще не про математику и не про доказательства.
    Мне интересны именно «софтварные вакансии».
  • Почему земляне делают глючный софт и железо
    0
    Я смотрел в сторону VHDL, Verilog. Но у меня сложилось впечатление, что это к «формальной верификации» вообще не имеет никакого отношения. Это больше похоже на написание тестов для микросхем. А мне бы хотелось что-нибудь связанное именно с математическим доказательством корректности программ. Зависимые типы, все такое.
  • Почему земляне делают глючный софт и железо
    +1
    Покажите мне вакансию, связанную с формальной верификациейс, и я вам заплачу! Серьезно.
    Формальная верификация — это очень круто и интересно. Мне бы очень хотелось работать в данной области. Но факт в том, что это никому не нужно. И вряд ли это станет мейнстримом в ближайшем будущем. Грусный смайлик.
  • Реализация мультиплеера в игре. Сравнение возможностей Game Center, Steamworks и GameSparks
    0
    В принципе, да, все честно.
  • Реализация мультиплеера в игре. Сравнение возможностей Game Center, Steamworks и GameSparks
    0
    Есть такая программа для инди/студентов.
    https://www.gamesparks.com/indie-student-programme-faq/
    Вы не платите ничего, пока MAU(Monthly Active User) не превышает 100 000.

    Но у них свои критерии инди, и каждый запрос они рассматривают отдельно. По их мнению, наша студия JetDogs не является инди (что, в общем-то, не далеко от истины).
  • Как мы оживляем презентацию
    +1
    Я правильно понял, что чувак пишет правой рукой в правую сторону? А вы потом отзеркалили видео, чтобы надпись выглядела нормально для зрителя. Получается, что у чувака со второй картинки специально отзеркаленная футболка?
  • Музыкальная теория для гиков
    +5
    Музыкальная нотация — худшая из всех систем обозначения или жаргонов, с которыми я когда-либо сталкивалась.

    Полностью согласен с автором. В музыкальной нотации есть масса вещей, которые вызывают у меня WTF-реакцию. Такое ощущение, что её придумывал какой-то наркоман.

    Не знаю, возможно, меня закидают тапками, но вообще-то в России, как и вообще в континентальной Европе (кроме Нидерландов) принято использовать для обозначения ноты Си букву H, а буква B обозначает си бемоль.

    Это, как раз, ярчайший пример нелогичности музыкальной нотации. Казалось бы, что может быть проще, буковками «A», «B», «C» будем обозначать ноты ЛЯ, СИ, ДО, соответственно. Бемолем будем обозначать ноту на пол-тона выше, «Ab», «Bb». Какому гению пришло в голову сделать замену?
    B <-> Bb
    H <-> B
    Вот зачем это нужно было делать? Чтобы всех запутать?
    Я вот часто ищу в интернете аккорды разных песен. Когда встречается аккорд «B», никогда не знаешь — это СИ или СИ-бемоль.
  • Оракул от арифметики
    +9
    Я занимаюсь программированием достаточно долго, пробовал разные языки программирования, разные системы типов, парадигмы. Попутно еще пытаюсь изучать математику: абстрактную алгебру, топологию, теорию категорий и т.п.
    Моё субъективное ощущение в том, что математика ГОРАЗДО сложнее любого языка программирования.
  • Сборка 4-мерного кубика Рубика
    0
    Когда-то давно написал 4-мерного пакмана. Игровое пространство представляло из себя несколько 3-мерных лабиринтов, которые существовали как бы в параллельных измерениях. Между такими лабиринтами существовали «коридоры». На самом деле пространство было абсолютно изотропным и не было никаких выделенных направлений, но объяснить людям, что это и есть 4-мерное пространство было очень сложно. Самой частой фразой, которую я слышал, было «4-ое измерение — это же время!?»
  • λ-исчисление. Часть первая: история и теория
    0
    Правильно ли я понимаю, что в логике первого порядка есть фиксированное число предикатов и я могу их произвольно комбинировать с помощью кванторов и логических операций. Но в логике первого порядка нельзя сформулировать утверждение «для любого предиката P(x) верно ...»
  • λ-исчисление. Часть первая: история и теория
    0
    А можно вопрос в тему? Под логикой предикатов подразумевается логика первого порядка? Я не совсем понимаю, что это такое. Где граница между логикой первого парядка и логикой высшего порядка?
  • Новая книга по Haskell на русском?
    0
    Спасибо тебе, добрый человек :). А почему все-таки его нет в стандартной библиотеке?
  • Новая книга по Haskell на русском?
    0
    А ещё не хватает объяснения вот таких простых вещей, как выход из вложенного цикла, например.

    По поводу приведенной выше статьи, кто-нибудь может мне объяснить, где лежит монада EitherT? Я уже весь интернет излазил — где-то пишут, что он лежит в Control.Monad.Either, кто-то пишет, что в Control.Monad.Trans.Either. В моей версии хаскеля (Haskell Platform 2013.2.0.0) его нет нигде. Его выкинули из стандартной библиотеки? Если да, то зачем? Что мне делать, если я хочу EitherT вместо дибильного ErrorT?
  • Утрата слабой связанности
    0
    Зачем программировать вообще? Есть же давным давно написанный ИИ, который может сам программы писать. Главное, никому не показывать. Межпрограммерский заговор ведь :)
  • Математический фокус для MP3, JPEG и Гомера Симпсона
    0
    Про Гомера Симпсона и JPG тоже не очень верное сравнение.
    В случае с Гомером имеем функцию
    t -> (x, y)
    к которой применяем ПФ.

    А в случае JPG имеется функция (от двух переменных !!!)
    (x, y) -> color
    к которой применяется ФП, при чем дважды, по обеим переменным
  • Resumable функции
    0
    Да ничто не мешает. Теоретически могло быть и то, и то.
  • Resumable функции
    +1
    Я понимаю, что шаблоны и generics — это не одно и то же. Generics из C# красиво и элегантно вписан в систему типов, а шаблон в C++ — это тупо макрос, который тупо подставляет типы в нужные места, а потом пытается скомпилить.
    Я понимаю, что макросы — это тоже хорошо. Местами, они бывают незаменимы. Но я бы предпочел язык с мощной системой типов, языку с мощной системой макросов.
  • Resumable функции
    0
    По сравнению с C#, например.
  • Resumable функции
    +1
    А в C# надо реализовать шаблоны, как в C++

    Странно. Я всегда считал, что в С++ самые ужасные шаблоны.
  • Команда математиков за полгода написала 600-страничную книгу, используя GitHub
    +1
    А планируется ли создание какого-нибудь proof assistants, основанного на HoTT? Мне, как пользователю Coq, очень интересно.
  • Парадокс доказательства
    0
    Тоже задавался таким вопросом. Насколько я понял, вся классическая математика построена на теории множеств, а Coq — на теории типов. А это не одно и то же. Поправьте, если я не прав.
  • Мягкое введение в Coq: начало
    0
    Похоже, что так и есть. Вроде даже видел какие-то вакансии, связанные с Verilog/VHDL, где-то в Питере. На сколько я понял, это что-то связанное с проектированием микроконтроллеров и доказательство их корректной работы. Конечно, хотелось бы работать с чем-то более высокоуровневым.
  • Мягкое введение в Coq: начало
    +1
    Coq — очень крутая и интересная штука. Сам очень люблю подоказывать чего-нибудь, поломать голову. После него Haskell кажется детской игрушкой. Единственный недостаток, найти ему промышленное применение очень сложно. Я периодически поглядываю вакансии, не требуется ли кому-нибудь coq-программист, и пока ничего не нашел, к сожалению.
  • Жизнь на плоскости Лобачевского
    0
    Ну вот, значит вы меня понимаете. Всегда найдется какой-нибудь умник и скажет: «Простите, все это, конечно, интересно, а какое этому может быть практическое применение?»
  • Жизнь на плоскости Лобачевского
    +2
    И еще, раз уж пошел такой разговор, у меня есть желание написать парочку статей на математическую тему, но у меня есть сомнения следующего рода:
    — являются ли такие статьи уместны на хабре (особенно, если это чистая математика, без какого-то практического применения)
    — востребованы ли они читателями хабра.
  • Жизнь на плоскости Лобачевского
    +1
    Ну вот опять что-то не то. Ресурс, наверно, полезный, но опять все по принципу «вопрос-ответ». Школьнику задали задачку в школе, он пришел на форум, спросил — получил ответ. А хочется, чтобы человек написал статью про какой-нибудь раздел математики да еще понятным языком. А ты прочитал, и сразу захотелось все изучить. Не хватает духа хабра :).
  • Жизнь на плоскости Лобачевского
    +3
    Отличная статья. Спасибо! Хочу больше статей на математическую тему. Кстати, никто не подскажет, может существует какой-то ресурс, где собраны подобные статьи? Эдакий хабр с математическим уклоном. Все сайты, которые я до этого видел, либо похожи на сборник олимпиадных задач, либо ответы на ЕГЭ.
  • Как научиться писать книги
    +1
    Поддерживаю во всем. Продумать мир, персонажей, исключить «рояли в кустах» — все это на порядок важнее, чем какие-то там «уникальный сюжет», «читатель желает быть обманутым» и т.п.
  • Интроверт, программист, интроверт-программист
    0
    Ни разу не встречал утверждения, что тип определить просто. Ни в соционике, ни еще где-то.
  • Интроверт, программист, интроверт-программист
    0
    Мне показалось, еще и рациональности.

    Автор, кто вы по тиму, признавайтесь?
  • Байты не помещаются в метрическую систему
    –5
  • Алгоритм анонимной коллективной подписи
    0
    Интересно было бы придумать какой-то формальный язык, который бы описывал все криптографические протоколы. И еще какой-нибудь способ проверки, что нужные условия выполняются. Правда, я не представляю, как можно доказать, что некто X, зная Y не может из этого вычислить Z.
    На сколько я понимаю, на данный момент для каждого такого протокола доказательство его свойств — сложная нетривиальная задача.
  • Алгоритм анонимной коллективной подписи
    +1
    Кстати, хорошая идея, раздать случайно ключи. Можно попытаться прикрутить протокол «Покер по телефону».
    Да и на хабре где-то была статья, как играть в покер втроем.

  • Как я нахожу время?
    +1
    Теперь у меня есть бесполезный клочок бумаги и $70.000 долгов

    Ну вот. Теперь все подумают, что высшее образование никому не нужно.
  • 50% прибыли в App Store и Play получают всего 25 разработчиков
    0
    Тоже часто думаю на эту тему. Вот интересно, что будет если сделать нелинейную зависимость между прибылью, полученной с приложения, и прибылью, которую получат в результате разработчики? Например логарифмическую зависимость:
    если приложение заработало 10$, то разработчик получает 1у.е.
    если приложение заработало 100$, то разработчик получает 2у.е.
    если приложение заработало 1000$, то разработчик получает 3у.е.
    Получится ли искусственно обойти закон Парето?
  • Недвоичная логика
    +2
    Честно говоря, я так и не понял, чем троичная лучше, и при чем здесь основание логарифма?
    Преимущество трехзначной логики над бинарной легче всего продемонстрировать на примере операции сравнения двух чисел: здесь троичная логика сразу выдает результат (больше, меньше или равно)…

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