thedeemon: (passport)
[personal profile] thedeemon
На языках программирования можно ввести отношение частичного порядка "А < Б", когда с языка А на язык Б пересесть можно, и это ощущается как прогресс, а вот обратно возвращаться очень неохота и мучительно. Если не ошибаюсь, [livejournal.com profile] 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 и говорят, что В - это зависимый от А тип, или семейство типов, индексированное значениями из А. Но эту же запись можно воспринимать и буквально - как обычную функцию, просто кодомен у нее не совсем обычный.

Date: 2013-05-07 06:46 pm (UTC)
From: [identity profile] soonts.livejournal.com
>в этом отношении заметны две вершины - хаскель и лисп, с их высоты все остальные языки кажутся недостаточно хорошими
C# третья.

Date: 2013-05-07 09:03 pm (UTC)
From: [identity profile] dmytrish.livejournal.com
Знатный вы троль, батенька. Практичность языка вряд ли имеет отношение к элегантности.

Впрочем, слова «недостаточно хорошими» действительно нуждаются в уточнении — для чего и по каким критериям.
Edited Date: 2013-05-07 09:04 pm (UTC)

Date: 2013-05-07 09:26 pm (UTC)
From: [identity profile] soonts.livejournal.com
OK, напишу подробнее.

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

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

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

(no subject)

From: [identity profile] dmytrish.livejournal.com - Date: 2013-05-07 10:02 pm (UTC) - Expand

(no subject)

From: [personal profile] wizzard - Date: 2013-05-09 12:04 am (UTC) - Expand

(no subject)

From: [identity profile] lionet.livejournal.com - Date: 2013-05-07 10:03 pm (UTC) - Expand

(no subject)

From: [identity profile] dmytrish.livejournal.com - Date: 2013-05-07 10:35 pm (UTC) - Expand

(no subject)

From: [identity profile] nivanych.livejournal.com - Date: 2013-05-08 05:31 am (UTC) - Expand

(no subject)

From: [personal profile] wizzard - Date: 2013-05-09 12:03 am (UTC) - Expand

(no subject)

From: [identity profile] nivanych.livejournal.com - Date: 2013-05-09 04:53 am (UTC) - Expand

(no subject)

From: [identity profile] soonts.livejournal.com - Date: 2013-05-09 08:21 am (UTC) - Expand

(no subject)

From: [identity profile] maxim.livejournal.com - Date: 2013-05-09 09:24 am (UTC) - Expand

(no subject)

From: [identity profile] mstone.livejournal.com - Date: 2013-05-10 12:42 am (UTC) - Expand

(no subject)

From: [identity profile] soonts.livejournal.com - Date: 2013-05-07 10:46 pm (UTC) - Expand

(no subject)

From: [identity profile] lionet.livejournal.com - Date: 2013-05-07 10:59 pm (UTC) - Expand

(no subject)

From: [identity profile] soonts.livejournal.com - Date: 2013-05-07 11:29 pm (UTC) - Expand

(no subject)

From: [identity profile] dmytrish.livejournal.com - Date: 2013-05-08 07:38 am (UTC) - Expand

(no subject)

From: [identity profile] soonts.livejournal.com - Date: 2013-05-08 05:54 pm (UTC) - Expand

(no subject)

From: [identity profile] sassa-nf.livejournal.com - Date: 2013-05-08 07:28 pm (UTC) - Expand

(no subject)

From: [identity profile] soonts.livejournal.com - Date: 2013-05-08 07:53 pm (UTC) - Expand

(no subject)

From: [identity profile] sassa-nf.livejournal.com - Date: 2013-05-09 07:17 am (UTC) - Expand

(no subject)

From: [identity profile] soonts.livejournal.com - Date: 2013-05-09 08:15 am (UTC) - Expand

(no subject)

From: [identity profile] sassa-nf.livejournal.com - Date: 2013-05-09 08:48 am (UTC) - Expand

(no subject)

From: [identity profile] soonts.livejournal.com - Date: 2013-05-09 09:19 am (UTC) - Expand

(no subject)

From: [identity profile] sassa-nf.livejournal.com - Date: 2013-05-09 12:12 pm (UTC) - Expand

(no subject)

From: [identity profile] soonts.livejournal.com - Date: 2013-05-09 12:33 pm (UTC) - Expand

(no subject)

From: [identity profile] sassa-nf.livejournal.com - Date: 2013-05-09 06:57 pm (UTC) - Expand

(no subject)

From: [identity profile] soonts.livejournal.com - Date: 2013-05-09 09:33 pm (UTC) - Expand

(no subject)

From: [identity profile] sassa-nf.livejournal.com - Date: 2013-05-09 09:54 pm (UTC) - Expand

(no subject)

From: [identity profile] soonts.livejournal.com - Date: 2013-05-09 10:11 pm (UTC) - Expand

(no subject)

From: [identity profile] sassa-nf.livejournal.com - Date: 2013-05-10 07:24 am (UTC) - Expand

(no subject)

From: [identity profile] soonts.livejournal.com - Date: 2013-05-10 02:30 pm (UTC) - Expand

(no subject)

From: [identity profile] sassa-nf.livejournal.com - Date: 2013-05-08 08:33 am (UTC) - Expand

(no subject)

From: [identity profile] soonts.livejournal.com - Date: 2013-05-08 06:08 pm (UTC) - Expand

(no subject)

From: [identity profile] sassa-nf.livejournal.com - Date: 2013-05-08 06:27 pm (UTC) - Expand

(no subject)

From: [identity profile] soonts.livejournal.com - Date: 2013-05-08 06:41 pm (UTC) - Expand

async/await делает что?

From: [identity profile] bik-top.livejournal.com - Date: 2013-05-09 09:53 am (UTC) - Expand

Re: async/await делает что?

From: [identity profile] sassa-nf.livejournal.com - Date: 2013-05-09 11:09 am (UTC) - Expand

Re: async/await делает что?

From: [identity profile] bik-top.livejournal.com - Date: 2013-05-09 11:34 am (UTC) - Expand

Re: async/await делает что?

From: [identity profile] soonts.livejournal.com - Date: 2013-05-09 11:52 am (UTC) - Expand

Re: async/await делает что?

From: [identity profile] soonts.livejournal.com - Date: 2013-05-09 12:16 pm (UTC) - Expand

Re: async/await делает что?

From: [identity profile] sassa-nf.livejournal.com - Date: 2013-05-09 06:59 pm (UTC) - Expand

Re: async/await делает что?

From: [identity profile] soonts.livejournal.com - Date: 2013-05-09 11:51 am (UTC) - Expand

Re: async/await делает что?

From: [identity profile] bik-top.livejournal.com - Date: 2013-05-09 11:54 am (UTC) - Expand

await

From: [identity profile] bik-top.livejournal.com - Date: 2013-05-09 09:22 am (UTC) - Expand

(no subject)

From: [identity profile] si14.livejournal.com - Date: 2013-05-09 10:14 pm (UTC) - Expand

(no subject)

From: [identity profile] lionet.livejournal.com - Date: 2013-05-09 11:19 pm (UTC) - Expand

(no subject)

From: [identity profile] si14.livejournal.com - Date: 2013-05-10 12:56 am (UTC) - Expand

(no subject)

From: [identity profile] lionet.livejournal.com - Date: 2013-05-10 02:51 am (UTC) - Expand

(no subject)

From: [identity profile] soonts.livejournal.com - Date: 2013-05-10 02:56 pm (UTC) - Expand

(no subject)

From: [identity profile] justy-tylor.livejournal.com - Date: 2013-05-07 11:52 pm (UTC) - Expand

(no subject)

From: [identity profile] soonts.livejournal.com - Date: 2013-05-08 06:10 pm (UTC) - Expand

(no subject)

From: [identity profile] justy-tylor.livejournal.com - Date: 2013-05-08 11:04 pm (UTC) - Expand

(no subject)

From: [identity profile] soonts.livejournal.com - Date: 2013-05-08 11:17 pm (UTC) - Expand

(no subject)

From: [identity profile] justy-tylor.livejournal.com - Date: 2013-05-08 11:43 pm (UTC) - Expand

(no subject)

From: [identity profile] soonts.livejournal.com - Date: 2013-05-08 11:49 pm (UTC) - Expand

(no subject)

From: [identity profile] justy-tylor.livejournal.com - Date: 2013-05-09 12:06 am (UTC) - Expand

(no subject)

From: [identity profile] soonts.livejournal.com - Date: 2013-05-09 08:19 am (UTC) - Expand

(no subject)

From: [identity profile] fi_mihej.livejournal.com - Date: 2013-05-10 04:26 pm (UTC) - Expand

(no subject)

From: [identity profile] justy-tylor.livejournal.com - Date: 2013-05-10 06:10 pm (UTC) - Expand

(no subject)

From: [identity profile] fi_mihej.livejournal.com - Date: 2013-05-10 04:14 pm (UTC) - Expand

(no subject)

From: [identity profile] justy-tylor.livejournal.com - Date: 2013-05-10 04:39 pm (UTC) - Expand

(no subject)

From: [personal profile] wizzard - Date: 2013-05-09 12:04 am (UTC) - Expand

(no subject)

From: [identity profile] nivanych.livejournal.com - Date: 2013-05-09 05:11 am (UTC) - Expand

(no subject)

From: [identity profile] soonts.livejournal.com - Date: 2013-05-09 08:23 am (UTC) - Expand

(no subject)

From: [personal profile] wizzard - Date: 2013-05-09 12:05 am (UTC) - Expand

(no subject)

From: [identity profile] vp.livejournal.com - Date: 2013-05-08 06:35 am (UTC) - Expand

(no subject)

From: [identity profile] soonts.livejournal.com - Date: 2013-05-08 06:45 pm (UTC) - Expand

(no subject)

From: [identity profile] vp.livejournal.com - Date: 2013-05-08 07:07 pm (UTC) - Expand

(no subject)

From: [identity profile] maxim.livejournal.com - Date: 2013-05-09 02:35 am (UTC) - Expand

(no subject)

From: [identity profile] soonts.livejournal.com - Date: 2013-05-09 08:18 am (UTC) - Expand

(no subject)

From: [identity profile] maxim.livejournal.com - Date: 2013-05-09 08:44 am (UTC) - Expand

(no subject)

From: [identity profile] soonts.livejournal.com - Date: 2013-05-09 08:54 am (UTC) - Expand

(no subject)

From: [identity profile] maxim.livejournal.com - Date: 2013-05-09 08:56 am (UTC) - Expand

(no subject)

From: [identity profile] vp.livejournal.com - Date: 2013-05-09 11:54 am (UTC) - Expand

(no subject)

From: [identity profile] bik-top.livejournal.com - Date: 2013-05-09 09:18 am (UTC) - Expand

Date: 2013-05-09 03:49 am (UTC)

Date: 2013-05-07 07:57 pm (UTC)
From: [identity profile] geekyfox.livejournal.com
Это ты зря про пехепе :)

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

Date: 2013-05-08 05:10 am (UTC)
From: [identity profile] nivanych.livejournal.com
И не такой сложный и запутанный, как Pёrl!

Date: 2013-05-08 08:40 am (UTC)
From: [identity profile] geekyfox.livejournal.com
Ну да. По сравнению с перлом/питоном/жаваскриптом пехепе (субъективно) выигрывает.

Date: 2013-05-08 05:35 am (UTC)
From: [identity profile] thedeemon.livejournal.com
Амстерда Стокгольмский синдром. :)

Date: 2013-05-08 08:19 am (UTC)
From: [identity profile] geekyfox.livejournal.com
Это не стокгольмский синдром, это амстердамский опыт работы :)

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

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

(no subject)

From: [identity profile] nivanych.livejournal.com - Date: 2013-05-08 09:14 am (UTC) - Expand

(no subject)

From: [identity profile] geekyfox.livejournal.com - Date: 2013-05-08 10:08 am (UTC) - Expand

Date: 2013-05-07 08:46 pm (UTC)
From: [identity profile] clayrat.livejournal.com
> Тогда A -> Type будет просто типом функции, которая каждому элементу А сопоставляет какой-то тип. Это и получится зависимый тип, и именно так он и обозначается в соответствующих языках.

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

Date: 2013-05-08 01:28 am (UTC)
From: [identity profile] thedeemon.livejournal.com
Нет, это не он, хоть и похож внешне.

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

Первое для каждого х возвращает целое пространство, второе лишь точку в этом пространстве. Расслоение и сечение.
Edited Date: 2013-05-08 01:29 am (UTC)

Date: 2013-05-08 11:26 am (UTC)
From: [identity profile] sassa-nf.livejournal.com
думаю, в этом замечании всё-таки есть смысл.

B:A -> Type говорит нам о существовании типа, хотя нас и не интересует в месте употребления, что это за тип.

Примерно так:

B: ∃ C . A → C

Таким образом, мы заявляем, что вместо B можно подставить что угодно, строящее какой-то тип, возможно зависящий от значения A.

Как и с экзистенциальными типами в Х-е, вместо Type можно было бы написать ⊥, но вот тогда уж точно была бы путаница - хотя мы и не имеем в виду, что B строит значение типа bottom, выглядело бы именно так. На самом деле нам нужно выразить, что определение умеет работать с любым типом, включая bottom - что эквивалентно высказыванию, что определение не зависит от типа, возвращаемого B.
Edited Date: 2013-05-08 11:32 am (UTC)

(no subject)

From: [identity profile] thedeemon.livejournal.com - Date: 2013-05-09 04:30 pm (UTC) - Expand

(no subject)

From: [identity profile] sassa-nf.livejournal.com - Date: 2013-05-09 06:07 pm (UTC) - Expand

(no subject)

From: [identity profile] thedeemon.livejournal.com - Date: 2013-05-09 06:47 pm (UTC) - Expand

(no subject)

From: [identity profile] sassa-nf.livejournal.com - Date: 2013-05-09 07:42 pm (UTC) - Expand

Date: 2013-05-08 11:40 am (UTC)
From: [identity profile] sassa-nf.livejournal.com
Мне кажется, вы правы

B: A→Type ⇔ B: ∃ C . (x:A) → C x, да, но чтобы понять рекурсию нужно понять рекурсию :)
Edited Date: 2013-05-08 11:40 am (UTC)

Date: 2013-05-09 04:34 pm (UTC)
From: [identity profile] thedeemon.livejournal.com
Какой тип у С?

Мы не можем определить пи-тип (x:A) → C x, не определив понятие зависимого типа С → Type, иначе что будет значить "С х"?

(no subject)

From: [identity profile] sassa-nf.livejournal.com - Date: 2013-05-09 05:33 pm (UTC) - Expand

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

Date: 2013-05-08 05:10 am (UTC)
From: [identity profile] nivanych.livejournal.com
> назовем его Type, элементами которого являются типы

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

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

Date: 2013-05-08 05:38 am (UTC)
From: [identity profile] thedeemon.livejournal.com
Во всех приличных местах, включая Идрис, делается бесконесная иерархия Int : Type0 : Type1 : Type2 ... Но поскольку различие между этими вселенными важно лишь во время тайп-чекинга, но не особо важно при написании программ, в Идрисе они все называются Type, и получается, что как бы Type : Type, только компилятор сам расставляет их индексы в иерархии.

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

Date: 2013-05-08 05:44 am (UTC)
From: [identity profile] nivanych.livejournal.com
А, вон оно как. Не знал такое про идрис.
Думал, оно импредикативное. Забавно, спасибо.

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

Date: 2013-05-08 07:28 am (UTC)
From: [identity profile] sassa-nf.livejournal.com
А что делает бесконечная иерархия? Способ не определять конец иерархии?

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

From: [identity profile] nivanych.livejournal.com - Date: 2013-05-08 07:58 am (UTC) - Expand

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

From: [identity profile] sassa-nf.livejournal.com - Date: 2013-05-08 08:43 am (UTC) - Expand

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

From: [identity profile] nivanych.livejournal.com - Date: 2013-05-08 09:12 am (UTC) - Expand

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

From: [identity profile] thedeemon.livejournal.com - Date: 2013-05-09 04:23 pm (UTC) - Expand

Date: 2013-05-08 05:17 am (UTC)
From: [identity profile] nivanych.livejournal.com
> фильтрации

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

Date: 2013-05-09 05:16 am (UTC)
From: [identity profile] nivanych.livejournal.com
> две вершины - хаскель и лисп

Если уж говорить про чисто языки, то всякое типозависимое — не выглядит ли вершиной?

Date: 2013-05-09 04:21 pm (UTC)
From: [identity profile] thedeemon.livejournal.com
Для кого-то возможно, если есть такие люди, которым после агды хаскель (и все остальное) противен донельзя. Но этими 0-2 человеками можно и пренебречь. :) Отношение то чисто субъективное, и подходить к нему следует статистически: много ли людей считают переход с хаскеля/coq на C# прогрессом или наоборот плюются.

(no subject)

From: [identity profile] nivanych.livejournal.com - Date: 2013-05-09 04:37 pm (UTC) - Expand

(no subject)

From: [identity profile] thedeemon.livejournal.com - Date: 2013-05-09 05:19 pm (UTC) - Expand

Wait, oh shi~

Date: 2013-05-18 08:41 am (UTC)
From: [identity profile] bik-top.livejournal.com
А куда делись ветки с обсуждением поддержки асинхронности и CPS в языке?

Re: Wait, oh shi~

Date: 2013-05-18 10:03 am (UTC)
From: [identity profile] thedeemon.livejournal.com
Не знаю, куча комментов пропала куда-то. Я не трогал.
Козел сожрал, что-ли?

Date: 2013-07-04 10:08 pm (UTC)
From: [identity profile] urod.livejournal.com
С PHP согласен, с С++ и Лиспом нет.

Мне нравится С++ гораздо больше, чем С или, напротив, Java. Когда же я с С++ попытался перейти на Лисп, новый язык оказался неприятным и неудобным. Так, например, вместо

a[i]++;

надо писать

(setf (svref a i) (add (svref a i) 1))

Даже само название Lisp, то есть, по-русски, Спип, означает, что язык ИДЕОЛОГИЗИРОВАННЫЙ, как СССР. В нём неуютно.

Date: 2013-07-05 10:22 am (UTC)
From: [identity profile] thedeemon.livejournal.com
Мне лично лисп не нравится совсем. Просто по наблюдениям, люди, которые им увлекаются, на нем и застревают, на другие языки потом отказываются хорошо смотреть, считая лисп вершиной.

Profile

thedeemon: (Default)
Dmitry Popov

February 2026

S M T W T F S
12 34567
891011121314
15161718192021
22232425262728

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags
Page generated Mar. 16th, 2026 06:13 am
Powered by Dreamwidth Studios