заметки на полях (фильтрации)

[thedeemon]

На языках программирования можно ввести отношение частичного порядка "А < Б", когда с языка А на язык Б пересесть можно, и это ощущается как прогресс, а вот обратно возвращаться очень неохота и мучительно. Если не ошибаюсь, lionet в свое время заметил, что в этом отношении заметны две вершины - хаскель и лисп, с их высоты все остальные языки кажутся недостаточно хорошими. Но занятно другое: у этого отношения есть также два дна, по сравнению с которыми все другие языки выглядят превосходными, - это PHP и C++. :)

После ряда других языков мне заставить себя писать что-то на С++ очень сложно, но иногда такая необходимость возникает. Помогает сгладить моральные мучения лишь возможность найти в языке крупицы чего-то хорошего. Нынче вот взялся за новую реализацию своего фирменного super resolution движка, и что меня сейчас радует и выручает, это присутствующие в языке элементы зависимых типов. У меня код оперирует блоками разных размеров и векторами разной точности: это могут быть целые координаты в кадре низкого разрешения, в кадре высокого разрешения, а также координаты с полупиксельной и четвертьпиксельной точностью. Плюсовые шаблоны позволили описать эти вещи как семейства типов, индексированные целочисленными значениями, т.е. натурально зависимые типы получились:

#define VP_LOWRES  1
#define VP_HIRES   2
#define VP_HALF    3
#define VP_QUARTER 4

template <int Prec>
class Vec
{
public:
    int x, y;

    Vec(int vx, int vy) : x(vx), y(vy) {}
    Vec operator+(Vec<int Prec> &a) { return Vec<Prec>(x + a.x, y + a.y); }
    Vec operator-(Vec<int Prec> &a) { return Vec<Prec>(x - a.x, y - a.y); }
    Vec<Prec + 1> refine()          { return Vec<Prec + 1>(x*2, y*2); }
    ...
};

class Plane
{
    ...
    template<int W> void readBlockQP(Vec<VP_QUARTER> v, MonoBlock<W> &block);
    ...
}

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

К слову о зависимых типах. Одна тривиальная мысль о них мне лично оказалась весьма полезной для понимания. Мы привыкли в функциональных языках обозначать тип функции из А в В как А -> B, где А и В какие-то конкретные типы вроде Bool и Int, элементами которых служат значения вроде true и 2. Теперь добавим в систему типов еще один тип, назовем его Type, элементами которого являются типы. Тогда A -> Type будет просто типом функции, которая каждому элементу А сопоставляет какой-то тип. Это и получится зависимый тип, и именно так он и обозначается в соответствующих языках. Например, пишут B : A -> Type и говорят, что В - это зависимый от А тип, или семейство типов, индексированное значениями из А. Но эту же запись можно воспринимать и буквально - как обычную функцию, просто кодомен у нее не совсем обычный.

Comments

[soonts.livejournal.com]

>в этом отношении заметны две вершины - хаскель и лисп, с их высоты все остальные языки кажутся недостаточно хорошими
C# третья.

[geekyfox.livejournal.com]

Это ты зря про пехепе :)

Пехепе - вполне себе сравнительно неплохой невыразительный язык :)

[clayrat.livejournal.com]

> Тогда A -> Type будет просто типом функции, которая каждому элементу А сопоставляет какой-то тип. Это и получится зависимый тип, и именно так он и обозначается в соответствующих языках.

это ж Pi-тип? но ведь есть и Sigma!

[dmytrish.livejournal.com]

Знатный вы троль, батенька. Практичность языка вряд ли имеет отношение к элегантности.

Впрочем, слова «недостаточно хорошими» действительно нуждаются в уточнении — для чего и по каким критериям.

[soonts.livejournal.com]

OK, напишу подробнее.

Во-первых, в C# есть очень полезные вещи, которые даже не снились конкурентам, например LINQ и async-await.

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

И наконец, высокое качество рантайма и прилагаемой библиотеки классов.

[dmytrish.livejournal.com]

Ок, эти слова подтолкнули меня к просветлению.

*в священном ужасе выбросил SICP в окно*

[lionet.livejournal.com]

1. Посмотри на упоминание Haskell в статье http://en.wikipedia.org/wiki/Language_Integrated_Query — откуда ноги растут у фич, которые "не снились конкурентам".
2. async-await собирается в хаскеле или том же clojure (Lisp) из примитивных фич языка. В C# это добавили в качестве конструкции языка. Тоже говорит не о выразительности языка, а о "выраженности" — как в PHP: чего напихали в сам язык, то и выражается на этом языке.
2. > Во-фторых, язык практически не навязывает стиля программирования. — то, что у языка нет ограничений, это ещё не повод называть его элегантным. Минимум ограничений и максимум свободы — у языка ассемблера.

Про рантайм и библиотеку классов умолчу пока.

[dmytrish.livejournal.com]

Мне кажется странным само утверждение, что C# практически не навязывает стиль программмирования. Весьма сомнительно, что в C# возможно логическое программирование или метапрограммирование без эквилибристических попыток выразить эту предметную область императивным языком.

Даже функциональщина в C# выражается неуклюже (в нем вообще есть хотя бы const?), насколько я могу судить из своих скудных знаний о нем.

[soonts.livejournal.com]

>откуда ноги растут у фич
.NET 3.5 - 2007.
DSH package - первая версия с пометкой "proof of concept implementation only" 2011.
Ты уверен, что ноги растут именно в ту сторону, в которую тебе кажется?

>собирается в хаскеле или том же clojure (Lisp) из примитивных фич языка
Ты сам использовал async-await в реальной жизни?
Подозреваю что нет.
За разумное число строк кода ты не соберёшь ни из чего аналог.
Там огромную кучу сложности аккуратно спрятали за элегантной конструкцией из двух ключевых слов: маршалинг исключений, scheduler интегрированный в thread pool, интеграцию почти со всеми асинхронными API из framework, минимизацию context switches, synchronization contexts, поддержку cancellation, и много чего ещё.

>Минимум ограничений и максимум свободы — у языка ассемблера.
Я говорил не про свободу простреливать себе ноги, а про свободу выбора стиля программирования.
В ассемблере с этим даже хуже чем в Java.

[lionet.livejournal.com]

> Ты уверен, что ноги растут именно в ту сторону, в которую тебе кажется?

О да. Ищи LINQ здесь (статья 2009 года). http://fprog.ru/2009/issue1/lev-walkin-editorial/

> За разумное число строк кода ты не соберёшь ни из чего аналог. Там огромную кучу сложности аккуратно спрятали

Так об этом и речь. Огромная махровая куча, которую, чтобы правильно готовить, нужно решать в языке и в инфраструктуре кучу проблем. Где здесь элегантность языка просвечивает? Вместо того, чтобы выразить нечто в библиотеке, пришлось им решать огромную кучу сложности и прятать в сам язык, потому что пользователь C# сам эту сложность соорудить не в состоянии.

Вместе с тем, примитивы Erlang'а (промышленный стандарт в плане элегантности подхода к concurrency) делаются на Haskell всего лишь в виде библиотеки.

Подход "порешаем кучу сложностей и встроим конструкцию прямо в язык" имеет право на существование. Только, во-первых, этот подход периодически сбоит (чего стоит одна история с провалившейся попыткой решить "все сложности", когда пытались прикрутить STM к .Net), а во-вторых, это ничего общего не имеет с элегантностью языка. Практично? Да. Удобно? Да. Но не более.

> В ассемблере с этим даже хуже чем в Java.

Верно. В C# тоже с этим не всё так хорошо как в лиспе, например.

[soonts.livejournal.com]

>Ищи LINQ здесь (статья 2009 года)
Концепции и парадигмы — это для архитектурных астронавтов термины, я ими не пользуюсь.
Реализация Linq2SQL появилась в Haskel на 4+ года позже, чем в C#.

>Где здесь элегантность языка просвечивает?
В том и элегантность, что огромную кучу сложной, но необходимой логики спрятали за двумя несложными для понимания ключевыми словами.

>пользователь C# сам эту сложность соорудить не в состоянии
Он в состоянии соорудить практически то же самое, что только отсутствием синтаксического сахара будет отличаться от того как щас сделано.
Просто по объективным причинам объём работы большой.

>ничего общего не имеет с элегантностью языка. Практично? Да. Удобно? Да.
Именно это я и называю элегантностью.
Язык программирования — это не произведение искусства, а инструмент для решения реальных задач.

>В C# тоже с этим не всё так хорошо как в лиспе, например.
Лисп даже не умеет традиционного статически типизированного ООП.

[justy-tylor.livejournal.com]

Когда главной фичей новой версии языка стал распиареный async-await, который и так можно (или можно лучше) сделать на практически любом языке с замыканиями, без изменения компилятора... было наглядно продемонстрировано, что пользователей держат за дебилов. Ну или за тех, кто любит многокода, и дальше Java/PHP мира не видел.

А ведь когда-то была многообещающая платформа. Но дальше каждый сам делает свои выводы.

[thedeemon.livejournal.com]

Нет, это не он, хоть и похож внешне.

"A -> Type" определяет тип функций, которые для любого х из А нам вернут какой-то тип.
Пи-тип "(a:A) -> B a" (где В : A -> Type) определяет тип функций, которые для любого х из А вернут одно значение из того типа, который вернула В.

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

А какого типа Type?

[nivanych.livejournal.com]

> назовем его Type, элементами которого являются типы

Привыкли, понимаешь, к идрисам всяким... ;-)

[nivanych.livejournal.com]

И не такой сложный и запутанный, как Pёrl!

[nivanych.livejournal.com]

> фильтрации

Где фильтрации — не увидел.
Торможу или "не то" имелось в виду?

[nivanych.livejournal.com]

> в C# возможно логическое программирование

По этим обычно понимают что-то пролого-подобное, которое динамическое, а значит, без ущерба для выразительности, может быть использовано в качестве библиотеки.
Правда, если такое есть compile-time, это уже серьёзнее, но вряд ли обычно это имеют в виду.

[thedeemon.livejournal.com]

Амстерда Стокгольмский синдром. :)

Re: А какого типа Type?

[thedeemon.livejournal.com]

Во всех приличных местах, включая Идрис, делается бесконесная иерархия Int : Type0 : Type1 : Type2 ... Но поскольку различие между этими вселенными важно лишь во время тайп-чекинга, но не особо важно при написании программ, в Идрисе они все называются Type, и получается, что как бы Type : Type, только компилятор сам расставляет их индексы в иерархии.

Re: А какого типа Type?

[nivanych.livejournal.com]

А, вон оно как. Не знал такое про идрис.
Думал, оно импредикативное. Забавно, спасибо.

[vp.livejournal.com]

Я люто плюсую все сказанное относительно C#.

Не навязывает стиля программирования. Предлагаемый инструментарий настолько широк, что я вообще никуда с него не хотел бы слазить.
Основная парадигма - да, ООП, но если нужно - вот вам линк, если мало - вот вам вся та же мощная инфраструктура, но обернутая в полностью функциональный и готовый для продакшына F#. И еще есть же mono!

Мне кажется, что C# напрасно обделяют вниманием.

Re: А какого типа Type?

[sassa-nf.livejournal.com]

А что делает бесконечная иерархия? Способ не определять конец иерархии?

[dmytrish.livejournal.com]

В том и элегантность, что огромную кучу сложной, но необходимой логики спрятали за двумя несложными для понимания ключевыми словами. — а зачем вообще нужна эта вся сложность, если то же самое делается в упомянутых языках намного проще? И кроме того, позволяет ли async/await эту сложность переиспользовать, комбинировать, природно порождать новые конструкции языка?

Язык программирования — это не произведение искусства, а инструмент для решения реальных задач. — с этого я и начинал. Но тем самым вы ограничиваете себя именно кругом «реальных задач», это и есть «зона комфорта» C#, в то время, как более развитые языки (H. и L.) обладают существенной гибкостью, которая позволяет им неплохо себя чувствовать in the wild, в поле, в котором еще никто подобных задач не решал (и откуда и приходят все фичи, которыми так гордится сообщество C#, похоже, не подозревая о существовании хотя бы Microsoft Research, словно их дают незримые майкрософтовские боги — именно это подразумевалось под «пользователь C# сам эту сложность соорудить не в состоянии», у него есть возможность, потенциальность, но откуда возьмутся идеи?). Вы и не подозреваете, сколько прекрасных идей и инструментов все еще нет в C# и не будет.

Лисп даже не умеет традиционного статически типизированного ООП. — Clojure очень даже умеет, поскольку она работает поверх JVM, вот только сами кложуристы избегают тыкать палочкой в goop без особой необходимости. Думаю, соорудить Java-style велосипед вполне возможно и в Common Lisp, но зачем?!

Re: А какого типа Type?

[nivanych.livejournal.com]

Конец иерархии определён в каждой конкретной программе.
Это способ сделать систему предикативной (не определять понятия через самих себ), но оставив гибкость.

[geekyfox.livejournal.com]

Это не стокгольмский синдром, это амстердамский опыт работы :)

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

Вон на питоне или жаваскрипте в принципе можно сделать стойку на ушах навроде хламидомонадического комбинатора, но это будет неподдерживаемый ФАРШЪ.