заметки на полях (фильтрации)
May. 8th, 2013 01:19 amНа языках программирования можно ввести отношение частичного порядка "А < Б", когда с языка А на язык Б пересесть можно, и это ощущается как прогресс, а вот обратно возвращаться очень неохота и мучительно. Если не ошибаюсь,
lionet в свое время заметил, что в этом отношении заметны две вершины - хаскель и лисп, с их высоты все остальные языки кажутся недостаточно хорошими. Но занятно другое: у этого отношения есть также два дна, по сравнению с которыми все другие языки выглядят превосходными, - это PHP и C++. :)
После ряда других языков мне заставить себя писать что-то на С++ очень сложно, но иногда такая необходимость возникает. Помогает сгладить моральные мучения лишь возможность найти в языке крупицы чего-то хорошего. Нынче вот взялся за новую реализацию своего фирменного super resolution движка, и что меня сейчас радует и выручает, это присутствующие в языке элементы зависимых типов. У меня код оперирует блоками разных размеров и векторами разной точности: это могут быть целые координаты в кадре низкого разрешения, в кадре высокого разрешения, а также координаты с полупиксельной и четвертьпиксельной точностью. Плюсовые шаблоны позволили описать эти вещи как семейства типов, индексированные целочисленными значениями, т.е. натурально зависимые типы получились:
В результате блоки разного размера - это разные типы, и векторы разной точности - разные типы, реально очень помогает не запутаться. Плюс компилятору подспорье: у многих циклов число итераций теперь известно статически, можно хорошо оптимизировать. В иных языках для таких вещей можно использовать phantom types, но там может быть сложнее сделать функцию refine, переводящую вектор на следующий уровень точности, в соседний слой семейства. Все-таки очень удобно, когда с параметром типа можно делать всякую арифметику и использовать его сразу на двух уровнях: типов и выражений.
К слову о зависимых типах. Одна тривиальная мысль о них мне лично оказалась весьма полезной для понимания. Мы привыкли в функциональных языках обозначать тип функции из А в В как А -> B, где А и В какие-то конкретные типы вроде Bool и Int, элементами которых служат значения вроде true и 2. Теперь добавим в систему типов еще один тип, назовем его Type, элементами которого являются типы. Тогда A -> Type будет просто типом функции, которая каждому элементу А сопоставляет какой-то тип. Это и получится зависимый тип, и именно так он и обозначается в соответствующих языках. Например, пишут B : A -> Type и говорят, что В - это зависимый от А тип, или семейство типов, индексированное значениями из А. Но эту же запись можно воспринимать и буквально - как обычную функцию, просто кодомен у нее не совсем обычный.
После ряда других языков мне заставить себя писать что-то на С++ очень сложно, но иногда такая необходимость возникает. Помогает сгладить моральные мучения лишь возможность найти в языке крупицы чего-то хорошего. Нынче вот взялся за новую реализацию своего фирменного 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 и говорят, что В - это зависимый от А тип, или семейство типов, индексированное значениями из А. Но эту же запись можно воспринимать и буквально - как обычную функцию, просто кодомен у нее не совсем обычный.
no subject
Date: 2013-05-07 06:46 pm (UTC)C# третья.
no subject
Date: 2013-05-07 09:03 pm (UTC)Впрочем, слова «недостаточно хорошими» действительно нуждаются в уточнении — для чего и по каким критериям.
no subject
Date: 2013-05-07 09:26 pm (UTC)Во-первых, в C# есть очень полезные вещи, которые даже не снились конкурентам, например LINQ и async-await.
Во-фторых, язык практически не навязывает стиля программирования. Можно unsafe code с арифметикой указателей и ручным управлением памятью, можно динамический язык вообще без проверки имён методов, даже эту вашу функциональщину можно.
И наконец, высокое качество рантайма и прилагаемой библиотеки классов.
(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:async/await делает что?
From:Re: async/await делает что?
From:Re: async/await делает что?
From:Re: async/await делает что?
From:Re: async/await делает что?
From:Re: async/await делает что?
From:Re: async/await делает что?
From:Re: async/await делает что?
From:await
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:no subject
Date: 2013-05-09 03:49 am (UTC)no subject
Date: 2013-05-07 07:57 pm (UTC)Пехепе - вполне себе сравнительно неплохой невыразительный язык :)
no subject
Date: 2013-05-08 05:10 am (UTC)no subject
Date: 2013-05-08 08:40 am (UTC)no subject
Date: 2013-05-08 05:35 am (UTC)АмстердаСтокгольмский синдром. :)no subject
Date: 2013-05-08 08:19 am (UTC)В пехепе выразительность языка согласована с возможностями рантайма и глубиной системы типов. Вот ю си из вот ю гет, всё по честному.
Вон на питоне или жаваскрипте в принципе можно сделать стойку на ушах навроде хламидомонадического комбинатора, но это будет неподдерживаемый ФАРШЪ.
(no subject)
From:(no subject)
From:no subject
Date: 2013-05-07 08:46 pm (UTC)это ж Pi-тип? но ведь есть и Sigma!
no subject
Date: 2013-05-08 01:28 am (UTC)"A -> Type" определяет тип функций, которые для любого х из А нам вернут какой-то тип.
Пи-тип "(a:A) -> B a" (где В : A -> Type) определяет тип функций, которые для любого х из А вернут одно значение из того типа, который вернула В.
Первое для каждого х возвращает целое пространство, второе лишь точку в этом пространстве. Расслоение и сечение.
no subject
Date: 2013-05-08 11:26 am (UTC)B:A -> Type говорит нам о существовании типа, хотя нас и не интересует в месте употребления, что это за тип.
Примерно так:
B: ∃ C . A → C
Таким образом, мы заявляем, что вместо B можно подставить что угодно, строящее какой-то тип, возможно зависящий от значения A.
Как и с экзистенциальными типами в Х-е, вместо Type можно было бы написать ⊥, но вот тогда уж точно была бы путаница - хотя мы и не имеем в виду, что B строит значение типа bottom, выглядело бы именно так. На самом деле нам нужно выразить, что определение умеет работать с любым типом, включая bottom - что эквивалентно высказыванию, что определение не зависит от типа, возвращаемого B.
(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:no subject
Date: 2013-05-08 11:40 am (UTC)B: A→Type ⇔ B: ∃ C . (x:A) → C x, да, но чтобы понять рекурсию нужно понять рекурсию :)
no subject
Date: 2013-05-09 04:34 pm (UTC)Мы не можем определить пи-тип (x:A) → C x, не определив понятие зависимого типа С → Type, иначе что будет значить "С х"?
(no subject)
From:А какого типа Type?
Date: 2013-05-08 05:10 am (UTC)Привыкли, понимаешь, к идрисам всяким... ;-)
Re: А какого типа Type?
Date: 2013-05-08 05:38 am (UTC)Re: А какого типа Type?
Date: 2013-05-08 05:44 am (UTC)Думал, оно импредикативное. Забавно, спасибо.
Re: А какого типа Type?
Date: 2013-05-08 07:28 am (UTC)Re: А какого типа Type?
From:Re: А какого типа Type?
From:Re: А какого типа Type?
From:Re: А какого типа Type?
From:no subject
Date: 2013-05-08 05:17 am (UTC)Где фильтрации — не увидел.
Торможу или "не то" имелось в виду?
no subject
Date: 2013-05-09 05:16 am (UTC)Если уж говорить про чисто языки, то всякое типозависимое — не выглядит ли вершиной?
no subject
Date: 2013-05-09 04:21 pm (UTC)(no subject)
From:(no subject)
From:Wait, oh shi~
Date: 2013-05-18 08:41 am (UTC)Re: Wait, oh shi~
Date: 2013-05-18 10:03 am (UTC)Козел сожрал, что-ли?
Задолбали со своим C#, пост не про это!
From:no subject
Date: 2013-07-04 10:08 pm (UTC)Мне нравится С++ гораздо больше, чем С или, напротив, Java. Когда же я с С++ попытался перейти на Лисп, новый язык оказался неприятным и неудобным. Так, например, вместо
a[i]++;
надо писать
(setf (svref a i) (add (svref a i) 1))
Даже само название Lisp, то есть, по-русски, Спип, означает, что язык ИДЕОЛОГИЗИРОВАННЫЙ, как СССР. В нём неуютно.
no subject
Date: 2013-07-05 10:22 am (UTC)