Здравствуйте, 0x7be, Вы писали:
0>Справедливости ради надо сказать, что я зависимые типы изначально не думал применять
Я просто отвечал на вопрос Павла.
0>Мне кажется, что алгебраических типов с паттернматчингом вполне хватит для комфортной работы с такими протоколами. 0>Впрочем, раз уж зависимые типы упомянули, подумаю над их приложимостью к этой идее.
В твоей задаче они не особо нужны. Но с их помощью можно ее решить не напрягаясь.
... << RSDN@Home 1.2.0 alpha 4 rev. 1472>>
Пусть это будет просто:
просто, как только можно,
но не проще.
(C) А. Эйнштейн
Здравствуйте, dotneter, Вы писали:
D>Здравствуйте, Pavel Dvorkin, Вы писали:
PD>>ее с консоли введут.
Можно проще. Из консоли поступает строка, мы может либо продолжать работать со строкой, либо сделать проверку, потом int.Parse и наделим значение типом говорящим о том что это не просто строка а число, дальше можно продолжить и добавить в тип еще информацию о знаке и т.д.
Здравствуйте, WolfHound, Вы писали:
PD>>Тогда упростим. Я подобный вопрос уже несколько раз задавал. От своего невежества, конечно. Только почему-то никто на него не ответил. Вот давай ответь. WH>Я тебя уже не первый год тыкаю носом в эту ссылку. WH>http://en.wikipedia.org/wiki/Dependent_type
Да не в ссылке же дело. В идее о том, что можно предсказать результат без исполнения. Вот это мне и сомнительно.
WH>Вот тебе ссылки про адаптацию этой теории для практики. WH>http://scholar.google.com/scholar?hl=ru&q=type+refinements+programming&btnG=%D0%9F%D0%BE%D0%B8%D1%81%D0%BA&as_ylo=&as_vis=0 WH>Только ты же всеравно учиться не будешь.
PD>>Ну вот я тебе пример привел выше, с минусом и корнем. Объясни просто и понятно, каким образом, не запуская программы, можно проверить правильность порядка вызова функций. Продемонстрируй свои знания в ответ на мое невежество. WH>Я тебе уже много всякого разного показывал но ты все проигнорировал. WH>Заниматься твоим образованием мне лень.
То есть ты пополнил список тех, кому я этот вопрос задал и кто ответить так и не смог. Неудивительно.
WH>В рамках C# это не решается. Тут как минимум type refinements нужны, а их в C# нет.
Здравствуйте, 0x7be, Вы писали:
0>То есть нет возможности вызвать функцию обработки данных до её загрузки или если загрузка обломалась. 0>И нет возможности вызвать функцию скачки результата, если данные не были обработаны.
А теперь представь себе, что если загрузка обломалась, то надо выполнить операцию восстановления работоспособности сервера (или БД), после чего окажется, что загрузка уже прошла (для БД это странно, конечно, но в других случаях возможно, что некая инициализация обязана не только открыть канал, но и загрузить первую порцию данных).
Или если данные не обработаны, то нельзя скачивать результат, но можно (и нужно!) произвести ренинициализацию БД. Данные неправильно считаны, надо все с начала делать. Опять же с БД маловероятно, а в другом случае может быть.
Понимаешь, в чем проблема. Логика действий , вообще говоря, зависит от того, как выполнены предыдущие действия. Она может быть сколь угодно сложной, и все ее варианты могут быть оценены только путем выполнения и изучения результатов. А ты хочешь каким-то образом без того, чтобы эти результаты получить, сделать вывод о том, правильная ли эта логика (== потребовать от компилятора. чтобы он ее верифицировал).
Разумеется, есть множество алгоритмов или задач, которые допускают такую верификацию. Если логика достаточно проста, иными словами, этих путей исполнения немного (а лучше всего 1), то можно до исполнения определить, верна ли логика. Но в общем случае нет.
Вот тебе простой пример (из какой-то книги, которую я в молодости читал). Алгоритм одевания мужчины. Весь перечислять не буду, но ясно, что носки нужно надеть раньше, чем ботинки, а пиджак позже, чем рубашку. Хотя и тут вариантов много. Можно в таком порядке : носки, рубашку, пиджак , брюки,, ботинки. А можно и в таком порядке — носки, брюки, рубашку, пиджак, ботинки . А впрочем, и так можно, хотя и странно : рубашку, пиджак, брюки, носки, ботинки. Хотя после 3-го этапа выглядеть будешь весьма глупо
Вот и посчитай, сколько тут вариантов, и попробуй оцени без выполнения, правилен ли выбранный. Теоретически возможно. Построить граф всех правильных путей и проверить, есть ли наш путь в этом графе. Но возни тут намного больше, чем если проверить наш алгоритм на коллеге
А ведь пример простенький, и предметов одежды меньше десяти, и условий нет. А когда еще условия появляются ? Не удалось повязать галстук — вместо шляпы изволь одеть кепку. Не надел носки — в ботинках идти нельзя, а можно только в шлепанцах, а это значит, что нельзя и пиджак с галстуком надевать. И т.д. И т.п.
ИМХО все это чистый академизм, не имеющий отношения к реальной работе. Теоретизировать можно, а потом все это уйдет в архив вполне благополучно. Как с Сигуларити. Мне ее WolfHound пару лет назад усиленно пропагандировал, мол, новое слово, ОС на основе управляемого и верифицируемого кода. Новое — да, но и только. А теперь говорят, что ее вовсе закрыли (http://rsdn.ru/forum/life/4229495.1.aspx
Здравствуйте, Pavel Dvorkin, Вы писали:
PD>Вот тебе простой пример...
Спору нет, применимость любой модели программирования ограничена и на роль серебряной пули я этот подход и не предлагал.
В простых сценариях я применял подобные вещи на практике с успехом (правда, не осознав до конца, что я делаю).
Как он покажет себя на более сложных — это вопрос, который нуждается в проверке практикой. Не замахиваясь на революцию, я вполне допускаю, что из этого может получится неплохой инструмент, облегчающий программирование некоторого класса задач.
PD>ИМХО все это чистый академизм, не имеющий отношения к реальной работе. Теоретизировать можно, а потом все это уйдет в архив вполне благополучно.
Академизм понятие относительное. Кое-что из того, что раньше считалось "академизмом" и оторванным от жизни изобретением, мы сейчас широко пользуемся. Функциональное программирование, управляемый код, автоматическое управление памятью — все эти концепции в момент своего появления вызывали подозрение в "академизме".
Если разбираться в причинах этого "академизма", то есть желание как можно больше аспектов программы выражать формальным образом, что бы компилятор мог статически доказывать корректность программы относительно этого аспекта. С другой стороны, это требует соответствующей теоретической базы, подготовки людей, поддержки со стороны языка и дополнительных затрат при программировании, то есть дается совсем не бесплатно. Где-то на балансе выигрыша и стоимости надо искать решение.
Здравствуйте, Pavel Dvorkin, Вы писали:
PD>Да не в ссылке же дело. В идее о том, что можно предсказать результат без исполнения. Вот это мне и сомнительно.
По этой ссылке написано как это сделать.
PD>То есть ты пополнил список тех, кому я этот вопрос задал и кто ответить так и не смог. Неудивительно.
Ну разумеется.
Если ответы тупо игнорируются...
Ссылки я тебе дал.
Если есть желание образовывайся.
Если нет, то перестань бравировать своим невежеством. Не смешно уже.
... << RSDN@Home 1.2.0 alpha 4 rev. 1472>>
Пусть это будет просто:
просто, как только можно,
но не проще.
(C) А. Эйнштейн
Здравствуйте, WolfHound, Вы писали:
WH>По этой ссылке написано как это сделать.
PD>>То есть ты пополнил список тех, кому я этот вопрос задал и кто ответить так и не смог. Неудивительно. WH>Ну разумеется. WH>Если ответы тупо игнорируются... WH>Ссылки я тебе дал. WH>Если есть желание образовывайся. WH>Если нет, то перестань бравировать своим невежеством. Не смешно уже.
Не смешно тебе, ну и не смейся. Мне от этого ни холодно, ни жарко. Когда мне кто-то объяснит (тупо, на пальцах, идею) всего этого, я ее оценю и решу, стоит ли мне этим вообще интересоваться. Пока же вижу одно — никто не в состоянии на мои примеры привести аргументы, которые дали бы мне такое основание.
А вообще все это так далеко от реальных моих нужд, как почившая вроде бы в бозе Сингуларити от Windows 7 или Linux.
Здравствуйте, adontz, Вы писали:
A>Влад, как раз ты сейчас и балаболишь. вот у меня есть 1000 классов. И них 47 штук — stateful, а 953 stateless (как правило они ещё и immutable). То есть даже если этот метод распрекрасный и делает всё что только можно придумать, 47 классов это потолок его внедряемости.
Я, кстати, сам ещё не понял до конца, может быть ли протокол у stateless класса Я исключительно поддерживаю идею делать беспротокольные интерфейсы. Если у меня будет выбор сделать интерфейс без протокола или навернуть на него формализм описания протокола, то я однозначно выберу первый вариант.
Но иногда выбора нет и вот тогда...
Здравствуйте, 0x7be, Вы писали:
0>Здравствуйте, VladD2, Вы писали:
VD>>Nemerle тут может помочь только тем, что его код открыт и можно реализовать нужную функциональность в компиляторе. Но синтаксические навороты тут мало что дадут. Эта фича требует вмешательства в типизатор. 0>Хм. А как тебе следующий подход: метапрограмма, в самом общем виде — это программа которая обрабатывает другие программы. Помимо кодогенерации или трансформации она может заниматься и верификацией. Чисто теоретически легко себе представить макрос, который обходит AST программы, ищет все места использования типа, помеченного нужным атрибутом, и следит за тем, что бы выполнялись ограничения.
AST тут мало, надо еще знать, что оно делает.
Представь, что у тебя функции твоего интерфейса вызываются по одной через цепочки из десятка других функций, которые сами по себе при этом могут зваться в циклах, по условиям (т.е. иногда могут и не зваться, или зваться для разных объектов) и т.д. и т.п. Тебе придется в твоем анализаторе воспроизвести почти всю логику программы, чтобы отследить всё везде.
Здравствуйте, Pavel Dvorkin, Вы писали:
PD>Не смешно тебе, ну и не смейся. Мне от этого ни холодно, ни жарко. Когда мне кто-то объяснит (тупо, на пальцах, идею) всего этого, я ее оценю и решу, стоит ли мне этим вообще интересоваться. Пока же вижу одно — никто не в состоянии на мои примеры привести аргументы, которые дали бы мне такое основание.
Тебе объяснение на пальцах зависимых типов? Так его на RSDN уже несколько раз давали, поиск в руки
Здравствуйте, VladD2, Вы писали: VD>Здравствуйте, jazzer, Вы писали:
VD>>>То и говорю. Наличие состояния и контроль за ним еще не означает, что это КА. J>>В общем случае — может быть VD>А наш случай частный?
В том виде, в котором он сформулирован (набор методов и ограничения на последовательность вызовов) — да.
J>> (хотя математически сам компьютер — это КА, и соответственно все, что на нем работает, тоже КА),
VD>Ой как интересно! С удовольствием послушаю о том какое состояние конечное у компьютера.
В школу. Конечность автомата относится к конечности множества состояний.
VD>А машина Тьюринга или лямбда-исчисления Черча — это тоже КА? Тогда можно за одно рассказать и о конечном состоянии машины Тьюринга.
машина Тьюринга работает с бесконечной лентой, так что только по одной этой причине она уже не КА. Про конечное состояние ты уже повеселил нас выше.
Мы тут решаем реальные задачи на реальных компьютерах, у нас тут нет никаких бесконечных лент, все конечно.
J>> но вот в этом конкретном обсуждаемом случае я вижу КА в чистом и незамутненном виде. Объясни, почему то, о чем говорит 0x7be — это не КА.
VD>Да всем. Нет входных данных, например.
Входные данные — последовательность вызовов в программе.
VD>Да и вообще никаких атрибутов КА.
Правда? ну и какие, по-твоему, атрибуты у КА, что их тут "никаких" нет? Список атрибутов КА с пояснениями, почему их нет тут, очень поможет дальнейшему обсуждению.
VD>Не, безусловно, многие задачи можно описать в том числе и КА. Но и без них тоже можно. При этом КА описывают не все задачи. Например, бесконечные (рекурсивные) или задачи требующие для работы дополнительной памяти (например, парсинг).
Реальные задачи на реальных компьютерах — все. Всегда, когда у тебя возникают различные состояния — у тебя КА. Любой парсер представляет собой КА с по крайней мере четырьмя состояниями "еще не начали", "в процессе", "закончили успешно", "обнаружена ошибка". Сам компьютер — это КА, это медицинский факт.
VD>По сему не надо привязывать сюда КА. Они тут не причем. Вот внутри уникального типа может использоваться КА для обработки логики. Но уникаьные типы сами по себе — это всего лишь контроль за тем, чтобы в один момент времени на объект не было более одной ссылки. А логика у него может быть любой сложности, как укладывающейся в КА, так и не укладывающейся.
Причем тут уникальные типы, если они, как ты правильно отметил, всего лишь гарантируют единственность ссылки? Как они, сами по себе, помогут нам выразить требования?
VD>>>КА — это реализация. А оных может быть много. С монадами знаком? J>>Знаком. Чем КА-то не угодил, если он укладывается в требования 0x7be? VD>Тем что ты их за уши притянул. Я с тем же успехом могу притянуть монады. Они тоже позволяют связать вычисления.
Понятно. А если б я все написал на монадах, ты бы сказал, что они не катят, потому что можно описать все то же самое на зависимых типах. И по кругу до КА. Суперская логика.
J>> И КА — это в первую очередь математическая абстракция VD>Есть много мат.абстракций. И что?
И то, что я могу использовать любую подходящую, если она решает задачу. Я вижу, что КА ее решает. Ты мне пока что даже и намека не дал на то, что КА ее не решает, только пустопорожнее сотрясание воздуха со смехотворными аргументами типа "а еще можно на монадах".
VD>Эта интересна тем, что ты ей уделил больше внимания?
Эй, господин модератор, ты вообще никак не можешь без переходов на личности?
J>>объекта с состоянием и графом разрешенных переходов: http://en.wikipedia.org/wiki/Finite-state_machine. Так что это не КА — реализация, а КА допускает много реализаций.
VD>Где ты переходы то усмотрел? У тебя метод может получить ссылку и она может остаться в нем.
И что? Какое это отношение имеет к состояниям? которые мы хотим ограничить? У тебя какое-то в высшей степени оригинальное понятие о КА. Хотя судя по твоему перлу насчет конечного состояния компьютера, вывод тут только один может быть.
J>>Да ну? А если файл открыть не удалось, много тебе скажут дескриптор и смещение?
VD>Многое. Хэндл будет некорректным (например, равный нулю).
Я про такое использование дескриптора написал в следующем же предложении, ты его вообще прочитал или так отвечаешь, по рэндому?
VD>Меня другое интересно. А что делать, если система типов сложнее чем в случае открытия файлов?
В смысле — что делать? Программить, вестимо. Ну сложнее, и что с того? Значит, и программа получится сложнее
VD>Пойми. Ну, нельзя прописать какую-то сложную логику в типах. Только простой набор связей. Там и вычислений то никаких не будет. Это чистая декларация.
Нам не нужна сложная логика. Нам нужна реализация КА во время компиляции, и только.
Здравствуйте, jazzer, Вы писали:
J>Здравствуйте, Pavel Dvorkin, Вы писали:
PD>>Не смешно тебе, ну и не смейся. Мне от этого ни холодно, ни жарко. Когда мне кто-то объяснит (тупо, на пальцах, идею) всего этого, я ее оценю и решу, стоит ли мне этим вообще интересоваться. Пока же вижу одно — никто не в состоянии на мои примеры привести аргументы, которые дали бы мне такое основание.
J>Тебе объяснение на пальцах зависимых типов? Так его на RSDN уже несколько раз давали, поиск в руки
Нет. Объяснение, каким образом может контролироваться правильность последовательности вызовов в моем примере
Здравствуйте, Pavel Dvorkin, Вы писали:
PD>Нет. Объяснение, каким образом может контролироваться правильность последовательности вызовов в моем примере PD>http://rsdn.ru/forum/philosophy/4236549.1.aspx
Здравствуйте, jazzer, Вы писали:
J>Здравствуйте, Pavel Dvorkin, Вы писали:
PD>>Нет. Объяснение, каким образом может контролироваться правильность последовательности вызовов в моем примере PD>>http://rsdn.ru/forum/philosophy/4236549.1.aspx
PD>>в compile-time.
J>Я правильно понимаю, что тебе, фактически, надо гарантировать, что sqrt не будет вызван для отрицательного числа?
Нет. Мне доказывают, что можно сделать нечто, что позволит определить правильность порядка вызова функций без запуска программы, статически. Я привожу пример, когда ИМХО невозможно без запуска определить, правилен порядок или нет. Вот и все.
Здравствуйте, Pavel Dvorkin, Вы писали:
PD>Нет. Мне доказывают, что можно сделать нечто, что позволит определить правильность порядка вызова функций без запуска программы, статически. Я привожу пример, когда ИМХО невозможно без запуска определить, правилен порядок или нет. Вот и все.
Я тебе уже несколько лет привожу ссылки на статьи, где описаны и теория и практика.
Даны все теоремы и их доказательства.
Продемонстрированы работающие компиляторы, которые это делают на практике.
Причем все статьи прошли рецензию и опубликованы в уважаемых изданиях.
Все что нужно сделать, это прочитать статьи с включенным мозгом.
А ты все не возможно да не возможно.
Такое поведение называется воинствующее невежество.
... << RSDN@Home 1.2.0 alpha 4 rev. 1472>>
Пусть это будет просто:
просто, как только можно,
но не проще.
(C) А. Эйнштейн
Здравствуйте, WolfHound, Вы писали:
WH>Здравствуйте, Pavel Dvorkin, Вы писали:
PD>>Нет. Мне доказывают, что можно сделать нечто, что позволит определить правильность порядка вызова функций без запуска программы, статически. Я привожу пример, когда ИМХО невозможно без запуска определить, правилен порядок или нет. Вот и все. WH>Я тебе уже несколько лет привожу ссылки на статьи
Чем повторять все это лучше бы взял и привел пример кода на Agda2 (или другом языке с зависимыми типами) для данной задачи с корнем. Для знающего человека там вряд ли больше нескольких строк.
Здравствуйте, Pavel Dvorkin, Вы писали:
PD>Здравствуйте, jazzer, Вы писали:
J>>Здравствуйте, Pavel Dvorkin, Вы писали:
PD>>>Нет. Объяснение, каким образом может контролироваться правильность последовательности вызовов в моем примере PD>>>http://rsdn.ru/forum/philosophy/4236549.1.aspx
PD>>>в compile-time.
J>>Я правильно понимаю, что тебе, фактически, надо гарантировать, что sqrt не будет вызван для отрицательного числа?
PD>Нет. Мне доказывают, что можно сделать нечто, что позволит определить правильность порядка вызова функций без запуска программы, статически. Я привожу пример, когда ИМХО невозможно без запуска определить, правилен порядок или нет. Вот и все.
Ну, просто порядок вызовов статически определить не проблема, правильно? См. Boost.Proto, например.
Т.е. отталкиваемся от того, что порядок узнать мы можем и проверить его тоже можем (оставим пока за скобками то, что в этом примитивном случае у тебя проверяющий код будет сравним с самим кодом). Осталось только проверить, правильная ли версия выбирается в зависимости от знака аргумента. Для этого нужно знак вынести в тип (т.е. на выходе if должна быть не просто f, а Positive(f) для главной ветки и NonPositive(f) для ветки else) — это и есть зависимые типы:
struct Positive { float f; };
struct NonPositive { float f; };
// и т.д. для Negative, Zero и т.д.
Positive sqrt(Positive);
NonPositive minus(Positive);
Positive minus(NonPositive);
Здесь видно, что и minus(sqrt(Positive)), и minus(sqrt(minus(NonPositive))) даст NonPositive, а sqrt(NonPositive) просто не скомпилируется.
Управляющие структуры обычный С++ нетипизированы (в том смысле, как я написал выше). Поэтому придется написать свой if как-то так:
template <class Then, class Else>
void if_positive(float f, Then then_, Else else_)
{
if (f>0) then_( Positive(f) ); else_( NonPositive(f) );
};
как видишь, теперь у нас рантайм-свойство переменной (знак) выражено в типе, и когда ты будешь звать if_positive и попробуешь передать ему sqrt в качестве else — программа не скомпилируется.
Здравствуйте, WolfHound, Вы писали:
WH>Здравствуйте, Pavel Dvorkin, Вы писали:
PD>>Нет. Мне доказывают, что можно сделать нечто, что позволит определить правильность порядка вызова функций без запуска программы, статически. Я привожу пример, когда ИМХО невозможно без запуска определить, правилен порядок или нет. Вот и все. WH>Я тебе уже несколько лет привожу ссылки на статьи, где описаны и теория и практика. WH>Даны все теоремы и их доказательства. WH>Продемонстрированы работающие компиляторы, которые это делают на практике. WH>Причем все статьи прошли рецензию и опубликованы в уважаемых изданиях. WH>Все что нужно сделать, это прочитать статьи с включенным мозгом. WH>А ты все не возможно да не возможно. WH>Такое поведение называется воинствующее невежество.
Пока мне кто-нибудь не объяснит на пальцах, как можно разрулить ту ситуацию, которуя я описал, я не намерен тратить свое время на изучение этих теорем и работающих компиляторов с маргинальных языков. Это называется обыкновенным скептицизмом. Если кто-то мне скажет, что можно из воздуха получать золото, я сначала попрошу объяснить мне химию или физику этого процесса, и если объяснение будет удовлетворительным — только тогда займусь изучением сам. А до тех пор и с места не сдвинусь. Хорош бы я был, если бы последовал твоему совету несколько лет назад и начал всерьез интересоваться Сингуларити. Мне эта затея с самого начала показалась несерьезной, так оно и оказалось. Хотя и работающий прототип был, и запустить можно было.
простоя не намерен, как ребенок, бросаться на всякую новую игрушку. Много я этих игрушек видел — сначала шум до потолка, потом всеобщее забвение.
Ты объяснить не способен или не хочешь, ну и ладно. Сейчас jazzer пытается, посмотрим, что получится
Здравствуйте, 0x7be, Вы писали:
0>Хм. А как тебе следующий подход: метапрограмма, в самом общем виде — это программа которая обрабатывает другие программы. Помимо кодогенерации или трансформации она может заниматься и верификацией. Чисто теоретически легко себе представить макрос, который обходит AST программы, ищет все места использования типа, помеченного нужным атрибутом, и следит за тем, что бы выполнялись ограничения.
AST для этого должно быть типизированным.
О том, что надо сделать в немерел я тут говорил где-то рядом. Нужно добавить пару событий в компилятор которые позволят вмешаться в процесс обработки типизированного АСТ на последних стадиях. Это не будет макросом, но конечно же будет похожим на них.
Есть логика намерений и логика обстоятельств, последняя всегда сильнее.
Здравствуйте, jazzer, Вы писали:
PD>>Нет. Мне доказывают, что можно сделать нечто, что позволит определить правильность порядка вызова функций без запуска программы, статически. Я привожу пример, когда ИМХО невозможно без запуска определить, правилен порядок или нет. Вот и все.
J>Ну, просто порядок вызовов статически определить не проблема, правильно? См. Boost.Proto, например. J>Т.е. отталкиваемся от того, что порядок узнать мы можем и проверить его тоже можем (оставим пока за скобками то, что в этом примитивном случае у тебя проверяющий код будет сравним с самим кодом).
Порядок чего ? Вызовов в рантайме ? Проверяющий код будет при этом не сравним с самим кодом, а просто равен ему. И ничего тут не поможет. Вот пример, я его уже приводил
float func(float f)
{
// итерационный процесс решения некоторого уравнения, для которого f - стартовая точка. Уравнение имеет 2 корня, один >0, другой <0if(root>0)
DoX(root);
else DoY(root)
}
Можно ли определить, какая функция будет вызвана : DoX или DoY без этого проведения этого итерационного процесса в полном объеме ? Если бы это было возможно, математики человеку, которое такое решение бы предложил, при жизни памятник поставили.
И в моем примере с sqrt вопрос не в том, должен ли быть аргумент sqrt положительным. Вопрос в другом — правильно ли я задал порядок действий. Твое решение того примера см. ниже, а пока модифицирую его
if(x<0)
y = sin(cos(x));
else
y = cos(sin(x));
Тут все аргументы годятся , и этот код никаких исключений вызвать не должен. Но правильно ли я его написал ? Может, надо было написать if(x<0) ? И ты берешься в compile-time без тестирования сказать, правильно или нет ?
>Осталось только проверить, правильная ли версия выбирается в зависимости от знака аргумента. Для этого нужно знак вынести в тип (т.е. на выходе if должна быть не просто f, а Positive(f) для главной ветки и NonPositive(f) для ветки else) — это и есть зависимые типы: J>
J>struct Positive { float f; };
J>struct NonPositive { float f; };
J>// и т.д. для Negative, Zero и т.д.
J>Positive sqrt(Positive);
J>NonPositive minus(Positive);
J>Positive minus(NonPositive);
J>
J>Здесь видно, что и minus(sqrt(Positive)), и minus(sqrt(minus(NonPositive))) даст NonPositive, а sqrt(NonPositive) просто не скомпилируется.
J>Управляющие структуры обычный С++ нетипизированы (в том смысле, как я написал выше). Поэтому придется написать свой if как-то так: J>
J>template <class Then, class Else>
J>void if_positive(float f, Then then_, Else else_)
J>{
J> if (f>0) then_( Positive(f) ); else_( NonPositive(f) );
J>};
J>
J>как видишь, теперь у нас рантайм-свойство переменной (знак) выражено в типе, и когда ты будешь звать if_positive и попробуешь передать ему sqrt в качестве else — программа не скомпилируется.
J>Идея понятна?
Идея-то , конечно, понятна, и ее можно изложить двумя словами, без всяких примеров — размножить типы в зависимости от возможных значений и сыграть на несовместимости типов разных структур. Этот фокус известен давно. Ты с Win API, наверное, знаком ? Там есть хендлы, по существу — целые числа, а реализованы как указатели на пустые структуры, для каждого типа хендла — свой тип структуры. Поэтому вот такое
HPEN hPen = ...
HBRUSH hBrush = hPen;
не пройдет при компиляции.
Но применимость такой идеи ничтожна, и по сути ограничивается именно таким примером, ну может, еще парочкой иных. А в том же примере с sqrt и положительными- неотрицательными и т.д. стоит лишь слегка его усложнить (например, разделить все множество не на 2 (положительные и неположительные), а, скажем, на 10-20 интервалов- и сразу вся эта затея превратится в необозримое чудовище. А если таких чудовищ будет с десяток (а это пустяки), то в этом хаосе уже никто не разберется. Я никак не могу поверить в серьезность подобной затеи.
