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

Кложурка — лиспик на явке.

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

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

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

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

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

http://nponeccop.livejournal.com/114309.html

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

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

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

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

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

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

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

Coq/Agda/etc

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

Видео было бы хорошо.

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

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

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

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

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

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

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

Например, от стрелок. Единственный вариант, который я пока вижу. Нужно просто-типизированное 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) пытаться делать не связные списки, а аллоцируемые/реаллоцируемые массивы. Про компиляцию редукций ничего не скажу - только, наверно, тут, в первую очередь, нужен критерий линейности представляемого терма и/или его линеаризация.

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

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

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

Изыди!

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

Ясно.

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

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

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

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

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

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

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

1. строгой

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

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

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

5. явной

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

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

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

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

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

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

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

Им понравилась идея обнимашек из темы про встречу MskHUG

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

На паскале, штоль?

Может, некоторые мужики будут мытые.

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

Тоже не первой свежести. Оригинал и один-два примера.

Пардон, вот оригинал.