Re[19]: [Безумная идея] Тьюринг-полные системы типов
От: Mr.Cat  
Дата: 08.10.10 10:24
Оценка:
Здравствуйте, Klapaucius, Вы писали:
MC>>Ага, и идти отлаживать типы. Ненене.
K>Ну а в чем проблема-то?
http://rsdn.ru/forum/philosophy/3980805.aspx
Автор: deniok
Дата: 01.10.10


K>Выполнение программы — это процесс получения конечного объема информации из конечного исходных данных, т.е. процесс ради результата, а не ради процесса. Он обязан завершаться. Ergo — тьюринг-полные языки considered harmful.

Ну да, примерно так. По идее, программа не должна завершаться только в случае гарантированно бесконечного объема входных данных. Тут я не совсем уверен, но вроде для этого язык не обязан быть тьюринг-полным.

MC>>Вот в том-то и заключается вопрос. Можно ли придумать такую систему типов, которая была бы мощной и удобной и в то же время в ней не было бы проблемы останова.

K>Можно, но всегда можно будет придумать систему типов с проблемой останова, с помощью которой можно будет обнаруживать больше ошибок, чем с помощью этой мощной и удобной.
Точно?

MC>>Как это не аргумент? Тоже аргумент. Не везде же нам нужны тьюринг полные языки — часто достаточно тьюринг-неполных dsl.

K>На практике это не так. Сначала делается не тьюринг-полный ДСЛ, а потом кто-то ударяется лбом о неполноту и тьюринг-полноту добавляют. SQL сделали тьюринг полным, даже перловские регекспы, ЕМНИП, полны по тьюрингу. Ну вот теперь делают тьюринг полные системы типов, потому что существует спрос.
То-то последнее время слышатся крики, мол от регекспов избавляться надо. Типа сложные, неподдерживаемые и все дела.
Насчет SQL — возможность производить бесконечный объем выходных данных из конечного — весьма сомнительна, согласись.
Re[21]: [Безумная идея] Тьюринг-полные системы типов
От: cvetkov  
Дата: 08.10.10 10:51
Оценка:
Здравствуйте, Klapaucius, Вы писали:

K>Не обязательно, но и это тоже. Ну вот такие вот они — эти люди — инструменты не по назначению используют. Как предлагаете с этим бороться?

ну уж точно не изобретением тюринг полных типов.
K>Заменить людей на что-то более преспособленное для использования не тьюринг-полных ДСЛ-ей?
"учится, учится и еще раз учится"(с)

а вообще мне не надо с этим боротся, это же мой хлеб плохие разработчики увеличивают количество работы и уменьшают конкуренцию.
... << RSDN@Home 1.2.0 alpha 4 rev. 1227>>
Re[20]: [Безумная идея] Тьюринг-полные системы типов
От: Klapaucius  
Дата: 08.10.10 11:07
Оценка:
Здравствуйте, Mr.Cat, Вы писали:

K>>Ну а в чем проблема-то?

MC>http://rsdn.ru/forum/philosophy/3980805.aspx
Автор: deniok
Дата: 01.10.10


Я, вообще-то, на это сообщение уже ответил. Там какие-то пояснения требуются, или мы уверенно будем двигаться в сторону столкновения с проблемой останова этого треда?

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


И тут на второй круг заходим? Я же уже писал в чем тут дело:

Проблема-то в том, что отличить потенциально бесконечный цикл от бесконечного в общем случае нельзя.
Ну так дело-то в том, что что-то ввести или вывести изолированно нельзя. Если мы хотим что-то ввести — мы, как правило, при этом что-то вводим, а что-то выводим и наоборот. Часто того, что нам бы вводить и выводить не хотелось.

Мы же пишем на тьюринг-полных языках не потому, что нам так хочется зацикливаться, а потому, что на языках, в которых зациклиться нельзя мы не можем написать всего, что нам нужно. Ситуация с системами типов точно такая же.

K>>Можно, но всегда можно будет придумать систему типов с проблемой останова, с помощью которой можно будет обнаруживать больше ошибок, чем с помощью этой мощной и удобной.

MC>Точно?

Точно.

MC>То-то последнее время слышатся крики, мол от регекспов избавляться надо. Типа сложные, неподдерживаемые и все дела.


Конечно надо избавляться, вот только среди альтернатив ничего тьюринг-неполного не предлагается.

MC>возможность производить бесконечный объем выходных данных из конечного — весьма сомнительна


Ну вот волшебная программа, производящая бесконечный объем выходных данных из конечного объема входных:
main = (print . cycle) =<< getLine
... << RSDN@Home 1.2.0 alpha 4 rev. 1476>>
'You may call it "nonsense" if you like, but I'VE heard nonsense, compared with which that would be as sensible as a dictionary!' (c) Lewis Carroll
Re[22]: [Безумная идея] Тьюринг-полные системы типов
От: Klapaucius  
Дата: 08.10.10 11:13
Оценка:
Здравствуйте, cvetkov, Вы писали:

K>>Заменить людей на что-то более преспособленное для использования не тьюринг-полных ДСЛ-ей?

C>"учится, учится и еще раз учится"(с)

Т.е. те, кто не использует для каждой задачи специальный неполный по тьюрингу ДСЛ — неучи?

C>а вообще мне не надо с этим боротся, это же мой хлеб плохие разработчики


Да еще и плохие разработчики?

C>увеличивают количество работы и уменьшают конкуренцию.


Увеличивают и уменьшают по сравнению с чем? Фантастической ситуацией, когда несуществующие "правильные" люди пользуются несуществующими "правильными" инструментами не встречающимся на практике "правильным" способом?
... << RSDN@Home 1.2.0 alpha 4 rev. 1476>>
'You may call it "nonsense" if you like, but I'VE heard nonsense, compared with which that would be as sensible as a dictionary!' (c) Lewis Carroll
Re[21]: [Безумная идея] Тьюринг-полные системы типов
От: Mr.Cat  
Дата: 08.10.10 11:34
Оценка: 6 (1)
Здравствуйте, Klapaucius, Вы писали:
K>Мы же пишем на тьюринг-полных языках не потому, что нам так хочется зацикливаться, а потому, что на языках, в которых зациклиться нельзя мы не можем написать всего, что нам нужно. Ситуация с системами типов точно такая же.
Мы пишем на тьюринг полных языках потому, что не умеем готовить неполные, ящитаю.

MC>>То-то последнее время слышатся крики, мол от регекспов избавляться надо. Типа сложные, неподдерживаемые и все дела.

K>Конечно надо избавляться, вот только среди альтернатив ничего тьюринг-неполного не предлагается.
Хм... А PEG, например, тьюринг полны? От левой рекурсии они уходят. Возможно, и от других способов достижения незавершимости на конечных входных данных?

MC>>возможность производить бесконечный объем выходных данных из конечного — весьма сомнительна

K>Ну вот волшебная программа, производящая бесконечный объем выходных данных из конечного объема входных:
K>
K>main = (print . cycle) =<< getLine
K>

Я имел в виду сомнительную полезность таких программ. Вот эта твоя программа, например, абсолютно бесполезна.
Re[23]: [Безумная идея] Тьюринг-полные системы типов
От: cvetkov  
Дата: 08.10.10 11:47
Оценка:
Здравствуйте, Klapaucius, Вы писали:

C>>"учится, учится и еще раз учится"(с)

K>Т.е. те, кто не использует для каждой задачи специальный неполный по тьюрингу ДСЛ — неучи?
я бы сказал что те то используют инструменты не по назначению недостаточно квалифицированы.
но по сути это близкие высказывания.

C>>а вообще мне не надо с этим боротся, это же мой хлеб плохие разработчики

K>Да еще и плохие разработчики?
недостаточно квалифицированные для выполняемых задач разработчики — плохие разработчики.
так что и тут мне нечем вам возразить.

C>>увеличивают количество работы и уменьшают конкуренцию.

K>Увеличивают и уменьшают по сравнению с чем?
по сравнению с гепотетической ситуацией когда эти разработчики достаточно квалифицированы.
K>Фантастической ситуацией, когда несуществующие "правильные" люди пользуются несуществующими "правильными" инструментами не встречающимся на практике "правильным" способом?
есть в языке такое понятие как Пресуппозиция. Твое высказывание содержит несколько ложных презумпций. Попробуй сформулировать его проще.
... << RSDN@Home 1.2.0 alpha 4 rev. 1227>>
Re[22]: [Безумная идея] Тьюринг-полные системы типов
От: Klapaucius  
Дата: 08.10.10 12:16
Оценка:
Здравствуйте, Mr.Cat, Вы писали:

MC>Мы пишем на тьюринг полных языках потому, что не умеем готовить неполные, ящитаю.


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

K>>Конечно надо избавляться, вот только среди альтернатив ничего тьюринг-неполного не предлагается.

MC>Хм... А PEG, например, тьюринг полны? От левой рекурсии они уходят. Возможно, и от других способов достижения незавершимости на конечных входных данных?

Я-то имел в виду всякие комбинаторные парсеры и прочие EDSL такого рода, которые можно расширять как угодно. Но в случае с PEG идет тот же самый процесс, что и в описанных мной выше случаях. PEG расширяют и приходят к левой рекурсии (понятно, что ценой отказа от линейной сложности парсинга, но и регексы тоже расширили ценой страшных тормозов — это видимо, мало кого волнует на самом деле).

MC>Я имел в виду сомнительную полезность таких программ. Вот эта твоя программа, например, абсолютно бесполезна.


Так надо так и говорить "сомнительная полезность", а не "сомнительная возможность". О том, что такие программы бесполезны я сам написал выше. Но в том и дело, что для того, чтобы писать полезные программы приходится позволять писать целый класс программ бесполезных. При этом во-первых, это не составляет серьезной проблемы, а во-вторых, бывает удобно написать программу как "бесконечную", при том что на самом деле она вечно работать, разуменется, не будет.
... << RSDN@Home 1.2.0 alpha 4 rev. 1476>>
'You may call it "nonsense" if you like, but I'VE heard nonsense, compared with which that would be as sensible as a dictionary!' (c) Lewis Carroll
Re[23]: [Безумная идея] Тьюринг-полные системы типов
От: Mr.Cat  
Дата: 08.10.10 12:31
Оценка:
Здравствуйте, Klapaucius, Вы писали:
K>Я-то имел в виду всякие комбинаторные парсеры и прочие EDSL такого рода, которые можно расширять как угодно.
Понятно, что edsl будет полон, если полон язык, куда он e. Но разве расширяемость предполагает полноту?

K>PEG расширяют и приходят к левой рекурсии

Так ведь левая рекурсия в КС-грамматиках устранима. Можно расширить в рамках КС и потом устранить рекурсию. Я правда не уверен, что только в ней проблема.

MC>>Я имел в виду сомнительную полезность таких программ. Вот эта твоя программа, например, абсолютно бесполезна.

K>Но в том и дело, что для того, чтобы писать полезные программы приходится позволять писать целый класс программ бесполезных.
Тут я с тобой пока не согласен. Приведи пример плз.
Re[21]: [Безумная идея] Тьюринг-полные системы типов
От: deniok Россия  
Дата: 08.10.10 12:37
Оценка:
Здравствуйте, Klapaucius, Вы писали:

K>Здравствуйте, deniok, Вы писали:


K>>>Если "порождаемая новая ошибка" — это бесконечный цикл при компиляции, который невозможно не заметить, то это может быть вполне приемлемой платой за обнаружение большего числа ошибок.

D>>А может и не быть.

K>Да может, конечно.


D>>Какие классы ошибок в коде не могут быть пойманы без тьюринг-полноты системы типов?


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


Я думаю, что
(а) в общем виде эта задача, если я её правильно понял, неразрешима (автоматически);
(б) для конкретной пары приемника и передатчика на языке типов нужно написать ручками доказательство их эквивалентности;
(с) задача верификации доказательств не требует тьюринг-полноты верификатора (например, COQ и прочие подобные верификаторы не полны по Тьюрингу, что не мешает выражать на их языке все существенные теоремы математики с их доказательствами)
Re[24]: [Безумная идея] Тьюринг-полные системы типов
От: Klapaucius  
Дата: 08.10.10 12:38
Оценка:
Здравствуйте, cvetkov, Вы писали:

C>Здравствуйте, Klapaucius, Вы писали:


C>>>"учится, учится и еще раз учится"(с)

K>>Т.е. те, кто не использует для каждой задачи специальный неполный по тьюрингу ДСЛ — неучи?
C>я бы сказал что те то используют инструменты не по назначению недостаточно квалифицированы.

А я вот считаю, что они, зачастую, более квалифицированны, чем люди, рассуждающие о применении "не по назначению". По той простой причине, что "использование не по назначению" бессмысленное сочетание слов, как на него не посмотри.
Способов определить назначение ровно два:
1) Практический, когда мы что-то применяем на практике, и если применить на практике можно, значит назначение соотвествует. Если что-то непрактично, оно и использоваться не будет, а если на практике оправдало себя — вот и назначение определилось. Но тогда мы приходим к тривиальному утверждению, потому как все что используется — используется по назначению.
2) Метафизический, когда голоса в голове осуждают использование чего-то не по назначению, а назначение знают голоса в голове. В этом случае лучше записаться на примем к специалисту или продолжать посещать места, выделенные для отправления религиозного культа.

C>недостаточно квалифицированные для выполняемых задач разработчики — плохие разработчики.


Плохие с точки зрения кого?

C>>>увеличивают количество работы и уменьшают конкуренцию.


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

C>Твое высказывание содержит несколько ложных презумпций.


Ложная презумпция тут была только одна и ваша, зато принципиальная, заключающаяся в том, что нечто широко и с успехом практикующееся считается "использованием не по назначению", а то, от чего пришлось отказаться из практических соображений — "использованием по назначению". Правильная презумпция, разумеется, подразумевает обратное.
... << RSDN@Home 1.2.0 alpha 4 rev. 1476>>
'You may call it "nonsense" if you like, but I'VE heard nonsense, compared with which that would be as sensible as a dictionary!' (c) Lewis Carroll
Re[24]: [Безумная идея] Тьюринг-полные системы типов
От: Mr.Cat  
Дата: 08.10.10 12:49
Оценка:
Здравствуйте, Mr.Cat, Вы писали:
K>>PEG расширяют и приходят к левой рекурсии
MC>Так ведь левая рекурсия в КС-грамматиках устранима. Можно расширить в рамках КС и потом устранить рекурсию.
Тут надо бы мою мысль переформулировать:
1. Вопрос. Какие классы грамматик требуют тьюринг-полного языка для реализации распознавателя?
2. Парсинг — это разбор по грамматике плюс выполнение семантических правил. Предположим, грамматика — КС, тогда есть ли ситуации, когда семантические правила надо выражать исключительно на тьюринг-полном языке?
Re[21]: [Безумная идея] Тьюринг-полные системы типов
От: Трурль  
Дата: 08.10.10 12:55
Оценка:
Здравствуйте, Klapaucius, Вы писали:

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


А должно ли это несоответствие выявляться именно системой типов?
Re[23]: [Безумная идея] Тьюринг-полные системы типов
От: Mr.Cat  
Дата: 08.10.10 12:56
Оценка:
Здравствуйте, Klapaucius, Вы писали:
K>Даже если это и так, то ситуация от этого не меняется. Мой пойнт в том, что в системе типов тьюринг-полнота нужна в точно такой же степени, что и в языках программирования вообще. Вот научитесь готовить неполные и обходится без полных — тогда и поговорим.

K>Так надо так и говорить "сомнительная полезность", а не "сомнительная возможность". О том, что такие программы бесполезны я сам написал выше. Но в том и дело, что для того, чтобы писать полезные программы приходится позволять писать целый класс программ бесполезных. При этом во-первых, это не составляет серьезной проблемы, а во-вторых, бывает удобно написать программу как "бесконечную", при том что на самом деле она вечно работать, разуменется, не будет.


Пока ввести понятие "полезная функция" и сравнить класс полезных функций с классом вычислимых.
Re[25]: [Безумная идея] Тьюринг-полные системы типов
От: cvetkov  
Дата: 08.10.10 13:24
Оценка:
Здравствуйте, Klapaucius, Вы писали:


K>А я вот считаю, что они, зачастую, более квалифицированны, чем люди, рассуждающие о применении "не по назначению". По той простой причине, что "использование не по назначению" бессмысленное сочетание слов, как на него не посмотри.

никогда не слышал выражения "забивать гвозди микроскопом"?
K>Способов определить назначение ровно два:
K>1) Практический, когда мы что-то применяем на практике, и если применить на практике можно, значит назначение соотвествует. Если что-то непрактично, оно и использоваться не будет, а если на практике оправдало себя — вот и назначение определилось. Но тогда мы приходим к тривиальному утверждению, потому как все что используется — используется по назначению.
применить можно, результат не соответствует ожиданиям.
K>2) Метафизический, когда голоса в голове осуждают использование чего-то не по назначению, а назначение знают голоса в голове. В этом случае лучше записаться на примем к специалисту или продолжать посещать места, выделенные для отправления религиозного культа.
тут спорить не с чем.

C>>недостаточно квалифицированные для выполняемых задач разработчики — плохие разработчики.

K>Плохие с точки зрения кого?
плохие с точки зрения решаемой задачи.

C>>>>увеличивают количество работы и уменьшают конкуренцию.

K>Как раз эти факторы и приводят к тому, что неэффективные и непрактичные решения сменяются на эффективные и практичные после преодоления некоторой энерции текущего положени я вещей.
тут дело не в инерции, но допустим я соглашусь.
K>То, что тьюринг-неполные нишевые языки на практике расширяются до тьюринг-полных как раз показывает, что решения о неполноте этих языков были решениями неэффективными и непрактичными.
не вижу связи. если это решение (о расширении до тюринг полных) приводит к неэффетивным и непрактичным программам, то значит решение об ограничении было правильным (эффективным и практичным)

C>>Твое высказывание содержит несколько ложных презумпций.


K>Ложная презумпция тут была только одна и ваша, зато принципиальная, заключающаяся в том, что нечто широко и с успехом практикующееся считается "использованием не по назначению", а то, от чего пришлось отказаться из практических соображений — "использованием по назначению". Правильная презумпция, разумеется, подразумевает обратное.

т.е. расширение регекспов до тюринг полного языка является практичным ходом?
или расширение SQL до тюринг полного языка является практичным ходом?

я не говорю о том что любое такое расширение плохо. просто все примеры которые мы тут видели таковы.
возможно в некоторых случаях в этом и есть смысл.
... << RSDN@Home 1.2.0 alpha 4 rev. 1227>>
Re: [Безумная идея] Тьюринг-полные системы типов
От: batu Украина  
Дата: 08.10.10 20:41
Оценка:
Здравствуйте, 0x7be, Вы писали:

0>Коллеги!


0>В моём перегретом солнцем (я сейчас в южных краях отдыхаю) мозгу крутится идея.

0>Вспомним давний спор между статической и динамической типизацией. Аргументы за статическую — раннее обнаружение ошибок типизации на этапе компиляции программы (и, в более широком смысле — доказательство корректности программы с точки зрения типов). Аргументы за динамическую — статические системы типов, поддерживаемые языками программирования, не только помогают программисту, но иногда и мешают ему, поскольку их выразительная сила ограничена и программист должен тратить дополнительные силы на то, что бы "вписаться" в систему типов языка. Кроме того, иногда (на моей практике достаточно редко) возникают ситуации, когда конкретная система типов просто не позволяет выразить требуемые программисту абстракции.
Вопрос давно созрел. Только тут не одна проблема, а несколько.

0>В чем сущность системы типов, как средства поддержки целостности программы? Её можно выразить просто — обеспечить, что на вход в программу (подпрограмму, процедуру, функцию, метод, предикат etc) будут поданы только те данные, которые эта программа может корректно переварить. Иными словами, необходимо все множество значений, которые могут существовать в данном языке, разбить на два — допустимые для передачи в эту программу и недопустимые. Соответственно, если проверка допустимости осуществляется на этапе анализа программы — это статическая система типов, если в момент выполнения — это динамическая. Если проверки нет — это memory corruption

Проверка предиката это очень логично. Я не вижу проблем ни со статической ни с динамической проверкой. Более того оба вида уже реализованы во многих языках. Так при объявлении в методе параметра типа object наличие свойств проверяется динамически. Осталось мелочи набраться смелости и ввести проверку на предикат при входе в программу. Будет возможна статическая проверка хорошо. Прийдется выполнять динамически ну, так и выполним. Такой вариант я и предложил в своем языке. Допустимы объявления параметров и группы типов, и множества и предикаты.

0>Разные системы типов по-разному справляются с этой задачей, предоставляя программисту разные инструменты для описания этих границ "можно-нельзя". Например, объявляя тип параметра как Integer, я указываю, что принимаются только целые числа. Если мне надо принимать только целые в интервале [-100..100], то я могу написать обертку над Integer или унаследоваться от него и породить класс ConstrainedInteger. Может быть ещё что-то, а может и ничего — все зависит от того, что поддерживается языком. Но в целом суть одна — я неявно описываю некоторый предикат, который для каждого возможного значения дает ответ — принадлежит значение типу или нет.

Вот здесь путаница. Класс и тип необходимо разделить. Класс порождает объект, а тип порождает значение. С ними по разному выполняются операции равенства, да и со сравнением не так просто. А у типов еще и операции.. Да еще типы оказывают влияние на лексический разбор. Но ход мысли правильный.

0>Суть идеи можно описать просто — дать программисту возможность описывать это разграничение максимально гибко. Дать ему язык для описания типов с выразительностью, не уступающей языку, на котором он производит разработку. То есть тьюринг-полный язык. Это может быть спец. язык или некоторое декларативное подмножество основного языка. Спецификации типов на этом языке могут быть вызваны как обычные функции-предикаты для проверки принадлежности заданного значения типу, так и использованы для доказательства взаимоотношения типов (несовместимы, пересекаются, включение, совпадение) в целях статической проверки корректности программы. Предикат с более чем одним параметром описывает параметризованный тип. При какой либо передаче данных производится проверка на совместимость типов. Если типы совместимы — все хорошо. Если типы заведомо несовместимы — ошибка компиляции. Если типы имеют пересечение — генерируется код проверки типа в run-time.

Если короче, то если наследуемые типы не содержат новых свойств, а только условия, то они наследуют и операции, за исключением тех случаев когда они явно определены для нового типа. Определение типа функцией выглядит неказисто в синтаксисе. Определение функции (предиката или множества что одно и тоже) отдельно и потом как обычно объявляем формальный параметр именем этого предиката вместо типа. Статическое выполнение тоже бывает возможно в таком варианте, но это отдельный и длинный разговор.

0>Данный подход, имхо, может иметь смысл в динамических языках для включения в них опциональной статической типизации. В традиционных статически типизированных языках эта идея вряд ли приживется, ибо в них на системы типов помимо обеспечения корректности, завязаны механизмы диспетчеризации вызовов (то есть две совершенно разные ответственности), а озвученная идея подразумевает ортогональность этих аспектов.

Еще одно замечание. Динамической типизацией называют возможность создания данных не только от типов но и от данных. Это порождает массу проблем. Так что я противник динамической типизации в классическом смысле этой парадигмы. Наследование от типа с возможностью добавления новых свойств эффективней реализуется, и без недостатков присущих языкам с динамической типизацией и без ущерба для достоинств присущих языкам с динамической типизацией.

0>Я не предлагаю проработанной концепции и у меня нет ответов на все вопросы. Просто предлагаю обсудить.

0>Спасибо за внимание.
Есть такая концепция.

0>P.S. Я в отпуске, так что отвечать буду нерегулярно.
Re[22]: [Безумная идея] Тьюринг-полные системы типов
От: Klapaucius  
Дата: 22.10.10 08:11
Оценка:
Здравствуйте, deniok, Вы писали:

D>(а) в общем виде эта задача, если я её правильно понял, неразрешима (автоматически);


Да, поэтому я написал не "доказать соотвествие приемника и передатчика", а "выявить несоотвествие приемника и передатчика".

D>(б) для конкретной пары приемника и передатчика на языке типов нужно написать ручками доказательство их эквивалентности;

D>(с) задача верификации доказательств не требует тьюринг-полноты верификатора (например, COQ и прочие подобные верификаторы не полны по Тьюрингу, что не мешает выражать на их языке все существенные теоремы математики с их доказательствами)

Да, но я так понимаю, что для этого понадобится давать верификатору дополнительную информацию. В случае ТC системы типов будут только две грамматики записанные в сигнатуре.
... << RSDN@Home 1.2.0 alpha 4 rev. 1476>>
'You may call it "nonsense" if you like, but I'VE heard nonsense, compared with which that would be as sensible as a dictionary!' (c) Lewis Carroll
Re[22]: [Безумная идея] Тьюринг-полные системы типов
От: Klapaucius  
Дата: 22.10.10 08:11
Оценка:
Здравствуйте, Трурль, Вы писали:

Т>А должно ли это несоответствие выявляться именно системой типов?


Нет, не должно, конечно. Но разговор и не об этом идет.
... << RSDN@Home 1.2.0 alpha 4 rev. 1476>>
'You may call it "nonsense" if you like, but I'VE heard nonsense, compared with which that would be as sensible as a dictionary!' (c) Lewis Carroll
Re[26]: [Безумная идея] Тьюринг-полные системы типов
От: Klapaucius  
Дата: 22.10.10 08:11
Оценка:
Здравствуйте, cvetkov, Вы писали:

K>>А я вот считаю, что они, зачастую, более квалифицированны, чем люди, рассуждающие о применении "не по назначению". По той простой причине, что "использование не по назначению" бессмысленное сочетание слов, как на него не посмотри.

C>никогда не слышал выражения "забивать гвозди микроскопом"?

Это выражение полностью соотвествует выражению "использование не по назначению" + плюс некоторый уклон в инвективу. Ну и соотвественно все сказанное мной для первого выражения я могу повторить и для второго.

C>применить можно, результат не соответствует ожиданиям.


Значит практика применения не сложится. Ну представьте артель забивальшиков гвоздей микроскопами. Где они с их производительностью труда возьмут средства на ремонт и приобретение микроскопов? (Если только они не попали в некоторую благоприятную нишу и не получают бесплатно списанные микроскопы.) Т.е. вполне объективные закономерности выведут их из игры и практика забивания гвоздей микроскопами не сложится.
Это и называется "проверкой на практике". Мы же говорим о уже сложившейся практике. Понятное дело, что обстоятельства могут измениться, тенденция будет переломлена и начнется обратное движение от тьюринг полных языков к наборам тьюринг-неполных ДСЛ-ей, но сейчас мы имеем то, что имеем.

K>>Плохие с точки зрения кого?

C>плохие с точки зрения решаемой задачи.

Но у решаемой задачи нет точки зрения. Есть точка зрения у того, кто использует разработчиков xs для решения задач ys. Если его устраивает соотношение затрат и полезного выхлопа — значит такой способ решения задач вполне имеет право на существование.

K>>Как раз эти факторы и приводят к тому, что неэффективные и непрактичные решения сменяются на эффективные и практичные после преодоления некоторой энерции текущего положени я вещей.

C>тут дело не в инерции.

А в чем?

K>>То, что тьюринг-неполные нишевые языки на практике расширяются до тьюринг-полных как раз показывает, что решения о неполноте этих языков были решениями неэффективными и непрактичными.

C>не вижу связи. если это решение (о расширении до тюринг полных) приводит к неэффетивным и непрактичным программам, то значит решение об ограничении было правильным (эффективным и практичным)

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

K>>Ложная презумпция тут была только одна и ваша, зато принципиальная, заключающаяся в том, что нечто широко и с успехом практикующееся считается "использованием не по назначению", а то, от чего пришлось отказаться из практических соображений — "использованием по назначению". Правильная презумпция, разумеется, подразумевает обратное.

C>т.е. расширение регекспов до тюринг полного языка является практичным ходом?
C>или расширение SQL до тюринг полного языка является практичным ходом?

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

C>я не говорю о том что любое такое расширение плохо. просто все примеры которые мы тут видели таковы.

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

Речь-то идет не о конкретных переходах, а об общей тенденции.
... << RSDN@Home 1.2.0 alpha 4 rev. 1476>>
'You may call it "nonsense" if you like, but I'VE heard nonsense, compared with which that would be as sensible as a dictionary!' (c) Lewis Carroll
Подождите ...
Wait...
Пока на собственное сообщение не было ответов, его можно удалить.