LINUX.ORG.RU

Встреча функциональных программистов в Санкт-Петербурге

 , ,


3

1

25 октября в Санкт-Петербурге состоится очередная встреча функциональных программистов.

Темы докладов:

  • Обзор Clojure. Доклад рассматривает Clojure с практической точки зрения: основы синтаксиса, нужные утилиты и библиотеки, подводные камни. Предварительное знание Clojure не требуется.
  • Зачем нужны зависимые типы. В докладе будут рассмотрены теоретические аспекты систем зависимых типов на примере системы Мартина-Лёфа. Также будут даны примеры использования зависимых типов: изоморфизм Карри-Ховарда, вычисления во время компиляции, инварианты, проверяемые во время компиляции, безопасный printf.

Участие бесплатное. Необходима предварительная регистрация.

>>> Подробности

★★★★★

Проверено: Shaman007 ()

Clojure, Haskell... Lisp уже не в моде?

NaN ()

Там будут совсем суровые лекции? Или достаточно иметь базовые знания ФП?

GblGbl ★★★★★ ()

Этот программист больше нефункционален! (с)

anonymous ()

а может кто-нибудь в пару предложениях, в пределах одного комментария объяснить — зачем нужны зависимые типы? :)

и от кого именно они являются зависимыми...

(ориентируясь на средненького императивного программиста :))

user_id_68054 ★★★★★ ()
Ответ на: комментарий от ymn

не совсем в двух предложениях — но всё-таки «объяснение понятия зависимых типов для мальчиков-дебилов» думаю тоже подойдёт :-) .. спасибо!

user_id_68054 ★★★★★ ()
Последнее исправление: user_id_68054 (всего исправлений: 1)

После встречи функциональных программистов программисты стали не функциональными .

amazpyel ★★★ ()
Последнее исправление: amazpyel (всего исправлений: 1)

Ужо набигут мужики с крестами разгонять...

Зачем нужны зависимые типы

Налицо подрыв экономической основы тоталитарных сект

slackwarrior ★★★★★ ()

читаешь заголовок и думаешь, что будет что-то крутое. а там какой-то jvm-crap в лице clojure. скучно. второй доклад — это хаскель, как я понимаю? тоже скучно.

anonymous ()
Ответ на: комментарий от anonymous

второй доклад — это хаскель, как я понимаю

Coq/Agda/etc

ymn ★★★★★ ()

Отличная новость. Скажу своим, может быть их заинтересует. Заодно в Питер съездят на халяву, а отпускные с каждого пополам возьму.

Etch ()
Ответ на: комментарий от AlexKiriukha

ЛОРчую.
Видео на mirror.yandex.ru выложите, пожалуйста.
Ютуб не благословлён Эдвардом Сноуденом.

NeProfessor ()

функциональных программистов

Звучит почти так же страшно, как «программистов на Delphi» или «программистов на Си».

Если бы оно называлось как-то типа «Встреча программистов, использующих функциональные языки»...

...Ага, сходил по ссылке. Там всего-то навсего «Functional programming meetup». Т.е. функциональное, разумеется, программирование, а не программисты.

hobbit ★★★★★ ()

Встреча программистов-функционалов в Санкт-Петербурге.

dvrts ★★★ ()
Ответ на: комментарий от user_id_68054

а может кто-нибудь в пару предложениях, в пределах одного комментария объяснить — зачем нужны зависимые типы? :)
и от кого именно они являются зависимыми...

Например, от стрелок. Единственный вариант, который я пока вижу. Нужно просто-типизированное LC это будет одна конструкция из стрелок/2-стрелок, нужно LC с зависимыми типами - другая, с субструктурными (линейными, в частности) - ещё третья. Т.е. фиксированное подмножество теории категорий само по себе довольно бедная метатеория, просто язык, в котором можно выразить все эти вещи. Мартин-Лёф предлагал формулировать разные теории типов в рамках метатеории LF, вот также это можно делать в рамках метатеории ТК.

Ну, например, берём декартово-замкнутую категорию Set, она же классический топос, т.е. категория всех малых множеств и тотальных функций, в agda она так и называется - «Set». Берём категорию всех малых категорий и функторов Cat (Set1 в agda) и утверждаем:

  • Любой тип который может использоваться (ADTs, GADTs, Inductive families) это объект Set (объект топоса, в общем случае), т.е., как следствие, множество - множество всех термов данного типа.
  • Любой параметрически-полиморфный тип это эндофунктор на Set, т.е. специального вида стрелка в Cat. (Непараметрический тип, который объект в Set, это вырожденный случай функтора из терминальной категории (как-то так)).
  • Любой конструктор типа данных который может быть это стрелка в Set (стрелка в топосе, вообще).
  • Любая функция которая может быть это тоже стрелка в Set, но отдельным классом (чтобы не путать стрелки-конструкторы и стрелки-функции). Как следствие, «функция» - тотальная функция между множествами.
  • Любая композиция стрелок с учётом декартовых произведений и экспоненциалов это любой правильно составленный терм в данной системе (тут типизация из коробки).
  • Любое определение конкретной редукции это 2-стрелка (струнная диаграмма).
  • Любой конкретный ход редукций (вычислений) это композиции 2-стрелок (струнных диаграмм). + Правила построения редукций из коробки.

Например:

-- Тут рисуем коммутативную диаграмму:
ℕ : Set
0 : 1 → ℕ
s : ℕ → ℕ

-- Продолжаем коммутативную диаграмму:
+ : ℕ → (ℕ → ℕ)

-- Рисуем две струнных диаграммы, которые можно сочетать:
e₁(+) : + ∘ a ∘ 0 ⇒ a
e₂(+) : + ∘ a ∘ (s ∘ b) ⇒ s ∘ (+ ∘ a ∘ b)

и это просто ТК (можно представить формальный синтаксис такого языка), безотносительно какого-либо ЯП, но понятно из каких ADT и функции это получилось.

Тут ещё интересно, что можно легко добавлять конструкторы и правила редукций (как если бы в хаскеле можно было дописывать ADT и pattern matching cases по разным модулям).

Сами по себе 2-стрелки это непосредственно струнные диаграммы, т.е., рисуя коммутативные диаграммы, получим схемы типов, рисуя струнные - flow chart.

  • Любая конкретная оптимизация это 3-стрелка. Правила построения оптимизаций тоже из коробки.

Например, если есть линейная рекурсия:

f x = z
f y = g (f (h y))

(f не появляется в g и h), т.е.:

-- любая стрелка вида:
f : x + y → r

-- с 2-стрелками вида:
e₁(f) : f ∘ x ⇒ z
e₂(f) : f ∘ y ⇒ g ∘ f ∘ h ∘ y

то она убирается такой 3-стрелкой:

-- Рисуем диаграмму между струнными:
o(f, f′) : e(f) ≡> e(f′ ∘ z)

-- TCO форма:
e₁(f′) : f′ ∘ a ∘ x ⇒ a
e₂(f′) : f′ ∘ a ∘ y ⇒ f′ ∘ (g ∘ a) ∘ (h ∘ y)

и остаётся только TCO.

Процесс унификации по 3-стрелкам это процесс оптимизаций, а процесс унификации по 2-стрелкам - интерпретации или компиляции (тогда нужен target). Как компилировать в target - конструкторы, например, достаточно точно отражаются в си-подобные структуры и объединения в памяти, можно даже в случае (s : ℕ → ℕ) или (_:_ : a → [a] → [a]) или вообще (con : [no `t' appears] → t → t) пытаться делать не связные списки, а аллоцируемые/реаллоцируемые массивы. Про компиляцию редукций ничего не скажу - только, наверно, тут, в первую очередь, нужен критерий линейности представляемого терма и/или его линеаризация.

anonymous ()
Ответ на: комментарий от anonymous

пытался прочитать — но сломал мозг...

..больше ни когда не буду программировать :)

похоже моё призвание это подметать улицы...

user_id_68054 ★★★★★ ()
Ответ на: комментарий от anonymous

Даа, это не навязшая в зубах копипаста про эндофункторы и зигохистоморфный препроморфизм. Респект.

tailgunner ★★★★★ ()

безопасный printf.

Вчера когда программировал обрезался printf..

anonymous ()
Ответ на: комментарий от anonymous

Вчера когда программировал обрезался printf..

Так ты теперь муслик? Или таки ой-вэй? (:-)

anonymous ()

Хочу встречу процедурных программистов!

Dron ★★★★★ ()
Ответ на: комментарий от Dron

А не боишься побочных эффектов? Они же не «чистые».

Virtuos86 ★★★★★ ()

Нормальное enterpriZe приложение должно быть создано на языке с типизацией:

1. строгой

2. статической

3. безопасной

4. именованной

5. явной

Иначе - это фуфло, поделие кульхацкерское, а не надёжное приложение.

Ну, что же. Есть фрик-ученые. Есть фрик-певицы и прочие фрик-артисты.

А теперь появились фрик-программисты.

Bioreactor ★★★★★ ()

Я б сходил, но добираться до офиса Яндекса (и обратно) — сомнительное удовольствие.

anonymous ()
Ответ на: комментарий от Bioreactor

Не посоветуете такой язык?

Не Ada и очень желательно безо всяких сборок мусора.

x86_64 ★★★ ()

как туда добираться то, метро далеко. Кто то пойдет?

BillDver ★★★ ()
Ответ на: комментарий от northerner

я - школьница, начинающая изучать ФП и не хочу обниматься с вонючими мужиками.

anonymous ()

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

timbaland ()
Вы не можете добавлять комментарии в эту тему. Тема перемещена в архив.