Как стать автором
Обновить

Обзор языка Idris

Функциональное программирование *
Из песочницы
Agda is too mainstream!

«Предвидение»

Материалов о языке Idris на русском практически нет, попробую это исправить кратким обзором. Также постараюсь сделать текст понятным для начинающих, не-функциональных и незнакомых с зависимыми типами программистов, и потому тем, кто знаком с подобными языками, может быть проще отмотать в конец или сразу прочесть официальную документацию. Писать серьёзное введение в язык и теорию не берусь, но надеюсь показать, о чём это вообще.

Итак, Idris — чистый функциональный язык программирования общего назначения с зависимыми типами.
Читать дальше →
Всего голосов 33: ↑31 и ↓2 +29
Просмотры 19K
Комментарии 7

Курсы Computer Science клуба, весна 2017

Блог компании Образовательные проекты JetBrains GPGPU *Big Data *Функциональное программирование *

Computer Science клуб вот уже 10 лет проводит открытые курсы по компьютерным наукам. Большинство лекций стараниями Лекториума записаны на видео и лежат в открытом доступе. В этом семестре выложены уже три новых курса, которые до этого не читались в клубе: «Программирование с зависимыми типами на языке Idris», «Вычисления на GPU. Основные подходы, архитектура, оптимизации», «Методы и системы обработки больших данных».
Читать дальше →
Всего голосов 29: ↑29 и ↓0 +29
Просмотры 6.6K
Комментарии 8

Шесть парадигм программирования, которые изменят ваш взгляд на код

Блог компании Productivity Inside SQL *Scala *Prolog *
Перевод
Периодически я натыкаюсь на языки программирования, которые настолько самобытны, что меняют моё представление о коде в целом. В этой статье я хотел бы поделиться некоторыми из самых любимых моих находок.

Здесь вы не найдёте устаревшего посыла «функциональное программирование спасёт мир!»; мой список состоит из куда менее популярных наименований. Готов поспорить, многие из читателей вообще не слышали о большинстве языков и парадигм, о которых пойдёт речь, так что надеюсь, вам будет так же интересно с ними разбираться, как и мне.

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


Читать дальше →
Всего голосов 40: ↑36 и ↓4 +32
Просмотры 52K
Комментарии 49

Паттерн Model-Update-View и зависимые типы

C++ *Haskell *Интерфейсы *Scala *Elm *


Model-Updater-View — функциональный паттерн, успешно применяемый в языке Elm в основном для разработки пользовательских интерфейсов. Что бы им воспользоваться надо создать тип Model, представляющий полное состояние программы, тип Message, описывающий события внешней среды, на которые программа должна реагировать, меняя свое состояние, функцию updater, которая из старого состояния и сообщения создает новое состояние прораммы и функции view, которая вычисляет по состоянию программы требуемые воздействия на внешнюю среду, которые порождают события типа Message. Паттерн очень удобный, но у него есть маленький недостаток — он не позволяет описать какие события имеют смысл для конкретных состояний программы.

Схожая проблема возникает (и решается) и при использовании ОО-паттерна State.

Язык Elm простой, но очень строгий — он проверяет, что функция updater хоть как-то обрабатывает все возможные сочетания модели-состояние и сообщения-события. По этому приходится писать лишний, пусть и тривиальный — как правило оставляющий модель без изменений, код. Я хочу продемонстрировать, как этого можно избежать в более сложных языках — Idris, Scala, C++ и Haskell.
Читать дальше →
Всего голосов 16: ↑16 и ↓0 +16
Просмотры 8.8K
Комментарии 2

Как сделать ещё больше некорректных состояний ещё более невыразимыми

Haskell *Функциональное программирование *

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

Читать дальше →
Всего голосов 28: ↑28 и ↓0 +28
Просмотры 4.6K
Комментарии 14

Зависимые типы — будущее языков программирования

Блог компании Издательский дом «Питер» Семантика *Программирование *Проектирование и рефакторинг *Математика *
Перевод
Всем привет!

Несмотря на диковинность и некоторую отвлеченность рассматриваемой сегодня темы — надеемся, что она сможет разнообразить вам выходные. В конце поста помещаем три ссылки от автора, позволяющие познакомиться с зависимой типизацией в Idris, F* и JavaScript
Читать дальше →
Всего голосов 40: ↑35 и ↓5 +30
Просмотры 24K
Комментарии 105

Как развернуть односвязный список на собеседовании

Ненормальное программирование *Программирование *Функциональное программирование *

Привет, Хабр.


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


image

Читать дальше →
Всего голосов 208: ↑186 и ↓22 +164
Просмотры 89K
Комментарии 472

Тесты или типы

Программирование *Функциональное программирование *
Перевод

Привет, Хабр. На днях я искал, как сделать что-то в Idris, и наткнулся на неплохой пост, вольный перевод которого выглядит вполне уместным. Вольности и отсебятину, где необходимо, я буду обозначать ⟦вот такими закорючками в начале и в конце⟧.


Когда стоит использовать тесты, а когда — типы? Какую информацию и какие гарантии мы получаем в обмен на наши усилия по их написанию?


Мы рассмотрим простой и немного надуманный пример, выраженный на Python, C, Haskell и Idris. Мы также увидим, что можно сказать о реализации без каких-либо дополнительных знаний о ней, в каждом из случаев.


Мы не будем учитывать разнообразные чёрные ходы, позволяющие явно нарушать гарантии языка (например, расширения C, unsafePerformIO в Haskell, небезопасные приведения типов), иначе нельзя было бы сделать вообще никаких выводов, и этот пост получился бы довольно коротким. ⟦Кроме того, у того же хаскеля есть подмножество Safe Haskell, явно и транзитивно запрещающее использование этих и ряда других трюков, могущих нарушить целостность языка.⟧

Читать дальше →
Всего голосов 52: ↑51 и ↓1 +50
Просмотры 7.1K
Комментарии 12