Re[19]: [Безумная идея] Тьюринг-полные системы типов - Философия программирования

Здравствуйте, Klapaucius, Вы писали:
K>Мы же пишем на тьюринг-полных языках не потому, что нам так хочется зацикливаться, а потому, что на языках, в которых зациклиться нельзя мы не можем написать всего, что нам нужно. Ситуация с системами типов точно такая же.
Мы пишем на тьюринг полных языках потому, что не умеем готовить неполные, ящитаю.

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

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

K>main = (print . cycle) =<< getLine
K>

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

Коллеги!

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

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

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

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

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

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

P.S. Я в отпуске, так что отвечать буду нерегулярно.

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

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

G>>А в чем проблема в таком случае сравнить типы?

D>В Тьюринг-полноте. Если на уровне типов можно оперировать любыми вычислимыми функциями, то можно поступить, например, так.

D>

D>MyType b := If b Then Int Else Double
D>Test := MyType (Exists (n>2, x>0, y>0, z>0) x^n+y^n=z^n)
D>

D>Вопрос: что делать проверяльщику, чтобы решить уравнение
D>

D>Test = Double
D>

D>Эндрю Уайлсу звонить?

Что делать любому другому языку если
int i = b ? 1 : 0;
int x = x / i;

Генерить эксепшин, не ?

Здравствуйте, gandjustas, Вы писали:
G>Зачем? Пусть отваливается, невычислимый тип — очевидно ошибка.
А как мы поймем, что тип невычислимый?

Лично я считаю, что тьюринг-полная система типов (ну или как ни назови программу времени компиляции) — это в некотором роде ересь. Ведь всегда предполагается, что 1)исходный код программы конечен 2)компиляция гарантированно завершается.

Здравствуйте, gandjustas, Вы писали:
MC>>А как мы поймем, что тип невычислимый?
G>Попробуем вычислить

И долго будем пробовать (по времени)?

MC>>Лично я считаю, что тьюринг-полная система типов (ну или как ни назови программу времени компиляции) — это в некотором роде ересь. Ведь всегда предполагается, что 1)исходный код программы конечен 2)компиляция гарантированно завершается.
G>Не вижу противоречий. Любой бесконечный тип (который нельзя вычислить за конечное, по сути ограниченное некоторым числом, время) в программе — ошибка.
G>При наличии тьюринг полной системы типов появятся ошибки компиляции при вычислении типа.
В том и фигня, что вполне возможно, что ты не сможешь за конечное время эту ошибку выявить. Проблема останова, однако.

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

G>например 1000 вызовов.

а если не хватит?

придется подбирать константу. и чем юольше эта константа тем долше придется ждать при реальной ошибке.

к тому же 1000 это явно мало.

... << RSDN@Home 1.2.0 alpha 4 rev. 1227>>

Здравствуйте, gandjustas, Вы писали:
G>Да ни разу не проблема останова, потому что мне не нужно анализировать вычисление типа, мне его выполнить надо.
Она самая. Для тьюринг-полной системы типов у нас нет возможности за конечное время убедиться в том, что компиляция займет конечное время. Для тьюринг-неполных систем типов, а-ля хаскель98, компилятор может за конечное время убедиться, что компиляция никогда не завершится — и выдать ошибку.

Тут стоит отметить, что в ряде языков типы уже тьюринг-полны (где-то могу напутать): haskell с рядом расширений ghc, c++ — а что толку.

Здравствуйте, Mr.Cat, Вы писали:

MC>Тут стоит отметить, что в ряде языков типы уже тьюринг-полны (где-то могу напутать): haskell с рядом расширений ghc, c++ — а что толку.

У C++ есть серьезное ограничение на глубину рекурсии при вычислении типов. А у haskell вроде с этим получше.

Здравствуйте, 0x7be, Вы писали:

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

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

Еще одна более интересная проблема.
Можно определить тип "упорядоченный список" (как — обращайтесь к thesz). Как объяснить компилятору что "упорядоченный список" является "списком"?
В хаскеле например такое сделать нельзя, поэтому потребуется копирование списка. В итоге получаем что механизм, который предназначен для оптимизации программы, заставляет нас писать более медленные программы.

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

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

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

Думаю зависимые типы помогут в решении этих проблем.

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

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

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

Что значит "сравнивать типы на равенство"? Зачем это делать?

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

G>Что значит "сравнивать типы на равенство"? Зачем это делать?

Чтобы, например, знать, можно ли выполнить swap(a,b). Если тип a равен типу b, то можно.

Здравствуйте, 0x7be, Вы писали:

Баян. И проблемы известные: http://rsdn.ru/forum/decl/3452020.1.aspx

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

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

G>>Что значит "сравнивать типы на равенство"? Зачем это делать?

D>Чтобы, например, знать, можно ли выполнить swap(a,b). Если тип a равен типу b, то можно.

Я думаю что мощную систему типов и mutable значения совместить будет непросто.

Здравствуйте, Mr.Cat, Вы писали:

MC>Тут стоит отметить, что в ряде языков типы уже тьюринг-полны (где-то могу напутать): haskell с рядом расширений ghc, c++ — а что толку.
Странно, что-то я в Haskell не видел такого. Надо бы погуглить.
А есть ссылки есть на описание этих расширений?

Здравствуйте, Mr.Cat, Вы писали:

MC>А вообще, сейчас в тред набегут адепты зависимых типов и докажут нам кузькину мать.
С удовольствием их выслушаю

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

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

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

M>Здравствуйте, 0x7be, Вы писали:
M>Баян. И проблемы известные: http://rsdn.ru/forum/decl/3452020.1.aspx
Ну, может быть, удастся сделать не так страшно

Здравствуйте, 0x7be, Вы писали:

0>Коллеги!

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

Как-то думал о подобной верификации. После нескольких попыток написать InsertSort на псевдокодах пришёл к выводу что получится очень громоздко и не удобно и в разы увеличит размер исходников.
Во-первых, про упомянутые расчеты.
имхо программа на половину будет состоять из приведения типов. Причем часто эти приведения типов будут выглядеть как Integer(получен из stdin от пользоваетля)->ConstrainedInteger[0,M+N*X] где M,N,X какая фигня типа "длина входящего вектора умноженная на два".

Как правильно было замечено, работать с элементарными типами будет ОЧЕНЬ больно:
Так как компилятор не в состоянии вывести доказательства всех утверждений, то сложные мат расчеты с участием ConstrainedInteger'ами можно будет использовать в учебниках по теории групп и колец(а так как сложение int'ов идёт по модулю 2^32, то выводить типы с их участием будет вообще весело).

Во-вторых. Выражение некоторых вещей будет выглядить отвратительно и судя по неинтуитивности Coq и прочего это не исправить. Пример. Рассмотрим алгоритм

Collection middleSelect(Collection coll)
{
     Collection result;
     int i = coll.length / 2;
     do{
             result.add(coll[i])
             i/=2;
     }while(i);
     return result;
}

Он делает какую-то странную выборку — берет серединный элемент, потом берет левую часть коллекции и берет её серединный элемен, потом берет левую часть левой части коллекции и берет её серединный элемент, т.д.
т.е. из коллекции 0,1,2,3,4,5,6,7,8....15 он возьмет 8,4,2,1,0.

Внимание вопрос. Что можно сказать про длину возвращаемой Collection? Вообще она где-то в районе log2(coll.length)+1.
А как теперь доказать это компилятору чтобы он вернул коллекцию в типе которые была заложена информация об log2? Это не получится доказать элегантно и автоматически в общем случае. Это получится доказать лишь используя кучу математических выкладок. Гипотетически если сделать громадную stdlib для помощи доказательств, то это можно упростить до чего-то

middleSelect(Collection coll[coll.length>=1]) -> Collection[length = log2(coll.length)+1]
{
     Collection result;     
     j=coll.length/2
     for i in 0..log2(coll.length) 
             result.add(coll[j])
             j/=2
     return result; //тут компилятору даже без помощи пользователя довольно легко вывести нужный тип 
}

Примечательно что второй код больше описывает тип получаемого результата(for i in 0..log2(coll.length)) чем сам результат(и я кстати не уверен что это идентичные ф-ции, ну да ладно). Причем если в stdlib'е не будет подходящей ф-ции(log2 в нашем случае), то автору middleSelect придётся либо писать замахнуться на медаль Филдса прямо в коде, либо забить на нормальный вывод типов и ограничится фигней вроде result.length <= coll.length(точности которой может очень сильно не хватить пользователю ф-ции middleSelect) рассуждая "как нибудь потом докажу"

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

G>Вот как раз в типах вроде ConstrainedInteger возникают основные проблемы. Вот у тебя есть ConstrainedInteger[0,100] , сумма двух таких значений будет какого типа?
Либо Integer, либо ConstrainedInteger заведомо вмещающий результат.

G>Как определить сумму в таком случае?
G>Как потом определить сумму для двух любых ConstrainedInteger?
G>Как определить обобщенную функцию, которая использует оператор (+), чтобы в нем можно было использовать и Integer , и ConstrainedInteger?
Ну, например, определить три функции сложения:
Integer -> Integer -> Integer
Integer -> ConstainedInteger -> Integer
ConstainedInteger -> ConstainedInteger -> ConstainedInteger

G>Еще одна более интересная проблема.
G>Можно определить тип "упорядоченный список" (как — обращайтесь к thesz). Как объяснить компилятору что "упорядоченный список" является "списком"?
G>В хаскеле например такое сделать нельзя, поэтому потребуется копирование списка. В итоге получаем что механизм, который предназначен для оптимизации программы, заставляет нас писать более медленные программы.
Сказать по правде, не понимаю в чем тут принципиальная проблема. Упорядоченный список явно должен быть подтипом списка.
Есть ссылки на примеры с этой проблемой?

G>В хаскеле все именно так.
Видимо мне стоит освежить свои знания о Хаскелле

G>На самом деле мало сделать систему типов полной по тьюрингу (такие уже есть), а еще надо добиться того чтобы такая система работала во благо программиста. Если система типов будет доставлять неудобства, то её будут обходить или просто не использовать.
Абсолютно согласен.

G>Думаю зависимые типы помогут в решении этих проблем.
Произведу раскопки в этом направлении

Здравствуйте, 0x7be, Вы писали:

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

G>>Вот как раз в типах вроде ConstrainedInteger возникают основные проблемы. Вот у тебя есть ConstrainedInteger[0,100] , сумма двух таких значений будет какого типа?
0>Либо Integer, либо ConstrainedInteger заведомо вмещающий результат.
возвращать просто integer по понятным причнам не стоит.
Например выражение a+b+c, где все три ConstrainedInteger может резко перестать компилироваться.

G>>Как определить сумму в таком случае?
G>>Как потом определить сумму для двух любых ConstrainedInteger?
G>>Как определить обобщенную функцию, которая использует оператор (+), чтобы в нем можно было использовать и Integer , и ConstrainedInteger?
0>Ну, например, определить три функции сложения:
0>Integer -> Integer -> Integer
0>Integer -> ConstainedInteger -> Integer
0>ConstainedInteger -> ConstainedInteger -> ConstainedInteger
А выделенное как?

G>>Еще одна более интересная проблема.
G>>Можно определить тип "упорядоченный список" (как — обращайтесь к thesz). Как объяснить компилятору что "упорядоченный список" является "списком"?
G>>В хаскеле например такое сделать нельзя, поэтому потребуется копирование списка. В итоге получаем что механизм, который предназначен для оптимизации программы, заставляет нас писать более медленные программы.
0>Сказать по правде, не понимаю в чем тут принципиальная проблема. Упорядоченный список явно должен быть подтипом списка.
0>Есть ссылки на примеры с этой проблемой?
Ну посмотри определение типа списка в хаскеле. Оно вообще-то нерасширяемо. Нельзя сделать подтип списка. Можно сделать другой список (упорядоченный например), а потом копировать один в другой. В итоге мы получим доказательство корректности с помощью системы типов, но путем уменьшения быстродействия. Хотя случаи возвращения из функции упорядоченного массива можно было бы покрыть тестами.

Здравствуйте, 0x7be, Вы писали:

0>Здравствуйте, Mr.Cat, Вы писали:

MC>>Тут стоит отметить, что в ряде языков типы уже тьюринг-полны (где-то могу напутать): haskell с рядом расширений ghc, c++ — а что толку.
0>Странно, что-то я в Haskell не видел такого. Надо бы погуглить.
0>А есть ссылки есть на описание этих расширений?

Еще D посмотри, там там смутно и неоднозначно сделанное в C++ насчет compile time вычислений довели до логического
конца для этого типа языков http://www.digitalmars.com/d/function.html#interpretation

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

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

0>>Странно, что-то я в Haskell не видел такого. Надо бы погуглить.
0>>А есть ссылки есть на описание этих расширений?

K>Демонстрация тьюринг-полноты системы типов Хаскеля.
K>Необходимиые расширения:
K>Multi-parameter type classes.
K>Functional dependencies.
K>Undecidable Instances
K>По этой же теме полезно ознакомиться с:
K>Type families

А еще думаю полезно будет Existential type

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

G>возвращать просто integer по понятным причнам не стоит.
G>Например выражение a+b+c, где все три ConstrainedInteger может резко перестать компилироваться.
Ну, если определена операция integer + ConstrainedInteger, то компилироваться будет. Правда тип результата будет более общим, чем хотелось бы.

G>А выделенное как?
Сорри, не понял изначального вопроса.
В чем там подвох?

G>Ну посмотри определение типа списка в хаскеле. Оно вообще-то нерасширяемо. Нельзя сделать подтип списка. Можно сделать другой список (упорядоченный например), а потом копировать один в другой. В итоге мы получим доказательство корректности с помощью системы типов, но путем уменьшения быстродействия. Хотя случаи возвращения из функции упорядоченного массива можно было бы покрыть тестами.
Спасибо, посмотрю.

Здравствуйте, 0x7be, Вы писали:

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

G>>возвращать просто integer по понятным причнам не стоит.
G>>Например выражение a+b+c, где все три ConstrainedInteger может резко перестать компилироваться.
0>Ну, если определена операция integer + ConstrainedInteger, то компилироваться будет. Правда тип результата будет более общим, чем хотелось бы.

G>>А выделенное как?
0>Сорри, не понял изначального вопроса.
0>В чем там подвох?

Ну вот у нас есть операторы:
Iteneger + Iteneger => Integer
Iteneger + ConstrainedInteger => Integer
ConstrainedInteger + ConstrainedInteger => ConstrainedInteger

Теперь хотим создать функцию

add :: a -> b -> c
add a b = a + b

Какие типы (ограничения) должны быть чтобы add скомпилировалась?

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

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

G>Я думаю что мощную систему типов и mutable значения совместить будет непросто.

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

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

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

G>>Я думаю что мощную систему типов и mutable значения совместить будет непросто.

D>mutable это просто пример. В любом случае проверяльщик типов вынужден будет решать тИповые уравнения, и проверка типов на равенство для этого необходима.
А в чем проблема в таком случае сравнить типы?

Здравствуйте, 0x7be, Вы писали:

Можно простой пример проблеммы и псевдокодное решение?

... << RSDN@Home 1.2.0 alpha 4 rev. 1111>>

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

G>А в чем проблема в таком случае сравнить типы?

В Тьюринг-полноте. Если на уровне типов можно оперировать любыми вычислимыми функциями, то можно поступить, например, так.

MyType b := If b Then Int Else Double
Test := MyType (Exists (n>2, x>0, y>0, z>0) x^n+y^n=z^n)

Вопрос: что делать проверяльщику, чтобы решить уравнение

Test = Double

Эндрю Уайлсу звонить?

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

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

G>>А в чем проблема в таком случае сравнить типы?

D>В Тьюринг-полноте.
Да ну, для тьюринг полноты нужна рекурсия. Не нужно умение решать уравнения.

D>Если на уровне типов можно оперировать любыми вычислимыми функциями, то можно поступить, например, так.

D>

D>MyType b := If b Then Int Else Double
D>Test := MyType (Exists (n>2, x>0, y>0, z>0) x^n+y^n=z^n)
D>

D>Вопрос: что делать проверяльщику, чтобы решить уравнение
D>

D>Test = Double
D>

D>Эндрю Уайлсу звонить?

Такое уравнение тебе никто не решит, типы тут не причем.

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

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

D>>

D>>MyType b := If b Then Int Else Double
D>>Test := MyType (Exists (n>2, x>0, y>0, z>0) x^n+y^n=z^n)
D>>

D>>Вопрос: что делать проверяльщику, чтобы решить уравнение
D>>

D>>Test = Double
D>>

D>>Эндрю Уайлсу звонить?

PC_>Что делать любому другому языку если
PC_>int i = b ? 1 : 0;
PC_>int x = x / i;

PC_>Генерить эксепшин, не ?

А в чём тут исключение? Чем это принципиально хуже, чем

Test := MyType (Exists (n>0, m>0) 2*n=m)

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

G>Да ну, для тьюринг полноты нужна рекурсия. Не нужно умение решать уравнения.

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

D>>Если на уровне типов можно оперировать любыми вычислимыми функциями, то можно поступить, например, так.

D>>

D>>MyType b := If b Then Int Else Double
D>>Test := MyType (Exists (n>2, x>0, y>0, z>0) x^n+y^n=z^n)
D>>

D>>Вопрос: что делать проверяльщику, чтобы решить уравнение
D>>

D>>Test = Double
D>>

D>>Эндрю Уайлсу звонить?

G>Такое уравнение тебе никто не решит, типы тут не причем.

15 лет уже как решили.

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

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

G>>Да ну, для тьюринг полноты нужна рекурсия. Не нужно умение решать уравнения.

D>Если нет уравнений, то смысл системы богатой типов непонятен. Любая разумная система типов делает проверку правильности типизации, сравнивая тот тип, что должен быть, и тот, который получается. Технически это и есть решение системы тИповых уравнений. При наличии рекурсии в типах следует очень тонко продумывать механизм типизации, чтобы процесс такого решения был гарантированно завершаем.

А его можно настолько тонко продумать, не убив полноту по Тьюрингу при этом? Чтот мне это проблему останова напоминает

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

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

G>>Да ну, для тьюринг полноты нужна рекурсия. Не нужно умение решать уравнения.

D>Если нет уравнений, то смысл системы богатой типов непонятен.
Почему?

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

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

D>>>Если на уровне типов можно оперировать любыми вычислимыми функциями, то можно поступить, например, так.

D>>>

D>>>MyType b := If b Then Int Else Double
D>>>Test := MyType (Exists (n>2, x>0, y>0, z>0) x^n+y^n=z^n)
D>>>

D>>>Вопрос: что делать проверяльщику, чтобы решить уравнение
D>>>

D>>>Test = Double
D>>>

D>>>Эндрю Уайлсу звонить?

G>>Такое уравнение тебе никто не решит, типы тут не причем.

D>15 лет уже как решили.
Ага, приведешь решение здесь?

Здравствуйте, Курилка, Вы писали:
К>А его можно настолько тонко продумать, не убив полноту по Тьюрингу при этом?
Я так понимаю, предложение состоит в том, чтобы убит полноту по Тьюрингу как-нить так аккуратно — чтобы это не сказалось на выразительности системы типов в наиболее распространенных сценариях.

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

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

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

Это от конкретной системы типов зависит.

D>>При наличии рекурсии в типах следует очень тонко продумывать механизм типизации, чтобы процесс такого решения был гарантированно завершаем.
G>Зачем? Пусть отваливается, невычислимый тип — очевидно ошибка.

Кому очевидно? Проблема останова, как известно, неразрешима.

D>>15 лет уже как решили.
G>Ага, приведешь решение здесь?

держи

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

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

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

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

D>Это от конкретной системы типов зависит.
Уже лучше. Ты предлагаешь систему типов виде логического ЯП, там действительно может не существовать решений для многих выражений.
Если использовать ФЯ, то все окажется проще.

D>>>При наличии рекурсии в типах следует очень тонко продумывать механизм типизации, чтобы процесс такого решения был гарантированно завершаем.
G>>Зачем? Пусть отваливается, невычислимый тип — очевидно ошибка.
D>Кому очевидно? Проблема останова, как известно, неразрешима.
А не надо решать проблему останова, надо просто вычислить тип (как обычную функцию). Уйдет в бесконечную рекурсию — ограничить кол-во рекурсивных вызовов.

Здравствуйте, Mr.Cat, Вы писали:

MC>Здравствуйте, gandjustas, Вы писали:
G>>Зачем? Пусть отваливается, невычислимый тип — очевидно ошибка.
MC>А как мы поймем, что тип невычислимый?
Попробуем вычислить

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

При наличии тьюринг полной системы типов появятся ошибки компиляции при вычислении типа.

Здравствуйте, Mr.Cat, Вы писали:

MC>И долго будем пробовать (по времени)?
Можно оставить на усмотрение программиста.
Так же как если запустить while(1 == 1) {}, со временем можно понять что что-то идет не так.
Только в отличии от программы, при компиляции можно выводить полезную информацию.

... << RSDN@Home 1.2.0 alpha 4 rev. 1111>>

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

D>Здравствуйте, 0x7be, Вы писали:
D>Можно простой пример проблеммы и псевдокодное решение?
Да мне тут уже объяснили, что я немного не туда копаю. Так что я пока предпочитаю сконцентрироваться на чтении тех ссылок, которыми меня тут снабдили

Здравствуйте, 0x7be, Вы писали:

0>Да мне тут уже объяснили, что я немного не туда копаю. Так что я пока предпочитаю сконцентрироваться на чтении тех ссылок, которыми меня тут снабдили

Не забудне потом поделиться тем что накопаете.

... << RSDN@Home 1.2.0 alpha 4 rev. 1111>>

Здравствуйте, Mr.Cat, Вы писали:

MC>Здравствуйте, gandjustas, Вы писали:
MC>>>А как мы поймем, что тип невычислимый?
G>>Попробуем вычислить

MC>И долго будем пробовать (по времени)?
например 1000 вызовов.

MC>>>Лично я считаю, что тьюринг-полная система типов (ну или как ни назови программу времени компиляции) — это в некотором роде ересь. Ведь всегда предполагается, что 1)исходный код программы конечен 2)компиляция гарантированно завершается.
G>>Не вижу противоречий. Любой бесконечный тип (который нельзя вычислить за конечное, по сути ограниченное некоторым числом, время) в программе — ошибка.
G>>При наличии тьюринг полной системы типов появятся ошибки компиляции при вычислении типа.
MC>В том и фигня, что вполне возможно, что ты не сможешь за конечное время эту ошибку выявить. Проблема останова, однако.
Да ни разу не проблема останова, потому что мне не нужно анализировать вычисление типа, мне его выполнить надо.

Здравствуйте, dotneter, Вы писали:
MC>>И долго будем пробовать (по времени)?
D>Можно оставить на усмотрение программиста.
Ага, и пусть он сам трахается с подбором констант.

D>Так же как если запустить while(1 == 1) {}, со временем можно понять что что-то идет не так.
В рантайме существуют юзкейсы для потенциально бесконечного цикла. В вот компайл тайме — скорее нет. Отсюда и идея: не вводить в язык то, для чего нет юзкейсов.

D>Только в отличии от программы, при компиляции можно выводить полезную информацию.
А в программе стало быть нельзя? Смешно же.

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

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

G>>например 1000 вызовов.

C>а если не хватит?

C>придется подбирать константу. и чем юольше эта константа тем долше придется ждать при реальной ошибке.

C>к тому же 1000 это явно мало.

Можно сделать директивой компиляции.

Здравствуйте, Mr.Cat, Вы писали:

MC>Здравствуйте, dotneter, Вы писали:
MC>>>И долго будем пробовать (по времени)?
D>>Можно оставить на усмотрение программиста.
MC>Ага, и пусть он сам трахается с подбором констант.
Имелся в виду не подбор констант а прямой аналог с while, запускаем компиляцию, смотрим если зависло значит где то накосячили, и нужно пройтись дебагом или посмотреть логи компиляции.
D>>Так же как если запустить while(1 == 1) {}, со временем можно понять что что-то идет не так.

D>>Только в отличии от программы, при компиляции можно выводить полезную информацию.
MC>А в программе стало быть нельзя? Смешно же.
Речь о штатоной работе того и другова.

... << RSDN@Home 1.2.0 alpha 4 rev. 1111>>

Здравствуйте, Mr.Cat, Вы писали:

D>>Можно оставить на усмотрение программиста.
MC>Ага, и пусть он сам трахается с подбором констант.

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

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

Юзкейсы для потенциально бесконечного цикла есть и в компайл тайм. А вот для бесконечного ни там ни там их нет. Проблема-то в том, что отличить потенциально бесконечный цикл от бесконечного в общем случае нельзя.
Вообще, для программиста для времени выполнения и времени компиляции юзкейсы не отличаются, они отличаются для пользователя программы.

MC>Отсюда и идея: не вводить в язык то, для чего нет юзкейсов.

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

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

... << RSDN@Home 1.2.0 alpha 4 rev. 1476>>

Здравствуйте, Klapaucius, Вы писали:
K>В данном случае, например, если программист успевает выпить чашку кофе, а компиляция еще продолжается — человек принимает решение, что это, пожалуй, многовато и компиляцию можно прерывать.
Ага, и идти отлаживать типы. Ненене.

K>Юзкейсы для потенциально бесконечного цикла есть и в компайл тайм.
Я считаю, что нет. Компиляция — это процесс получения конечного объема бинарников из конечного объема исходников, т.е. процесс ради результата, а не ради процесса. Он обязан завершаться.

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

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

Здравствуйте, dotneter, Вы писали:
D>Имелся в виду не подбор констант а прямой аналог с while, запускаем компиляцию, смотрим если зависло значит где то накосячили, и нужно пройтись дебагом или посмотреть логи компиляции.
Вот, deniok хорошо мысль сформулировал: http://rsdn.ru/forum/philosophy/3980805.aspx

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

G>Можно сделать директивой компиляции.

это убивает всю идею проверки типов.
получается что если я получаю ошибку компиляции то я не знаю что случилось: типы у меня не правильные или константа маловата (а потом появятся и другие константы управляющие стратегией оптимизации вычеслений)

не говоря уже о том что вычесление типов хотелось бы тоже сделать типизированным

... << RSDN@Home 1.2.0 alpha 4 rev. 1227>>

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

D>Ну, дело в том, что основной прикладной смысл системы типов — ловить ошибки и несоответствия спецификациям, а не порождать новые. В этом смысле выигрыш собственно от тьюринг-полноты не очень понятен.

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

... << RSDN@Home 1.2.0 alpha 4 rev. 1476>>

Здравствуйте, Mr.Cat, Вы писали:

K>>В данном случае, например, если программист успевает выпить чашку кофе, а компиляция еще продолжается — человек принимает решение, что это, пожалуй, многовато и компиляцию можно прерывать.
MC>Ага, и идти отлаживать типы. Ненене.

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

MC>Я считаю, что нет. Компиляция — это процесс получения конечного объема бинарников из конечного объема исходников, т.е. процесс ради результата, а не ради процесса. Он обязан завершаться.

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

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

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

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

На практике это не так. Сначала делается не тьюринг-полный ДСЛ, а потом кто-то ударяется лбом о неполноту и тьюринг-полноту добавляют. SQL сделали тьюринг полным, даже перловские регекспы, ЕМНИП, полны по тьюрингу. Ну вот теперь делают тьюринг полные системы типов, потому что существует спрос.

... << RSDN@Home 1.2.0 alpha 4 rev. 1476>>

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

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

K>SQL сделали тьюринг полным,
Зачем?
K>даже перловские регекспы, ЕМНИП, полны по тьюрингу.
И что в этом хорошего? и так write-only код сделели еще более не читаемым.
K>Ну вот теперь делают тьюринг полные системы типов, потому что существует спрос.
Спрос существует потому-что люди используют инструменты не по назначению.

... << RSDN@Home 1.2.0 alpha 4 rev. 1227>>

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

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

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

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

K>>SQL сделали тьюринг полным,
C>Зачем?

Чтоб жизнь медом не казалась, очевидно.

K>>даже перловские регекспы, ЕМНИП, полны по тьюрингу.
C>И что в этом хорошего?

Ничего.

C>Спрос существует потому-что люди используют инструменты не по назначению.

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

... << RSDN@Home 1.2.0 alpha 4 rev. 1476>>

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

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

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

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

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

... << RSDN@Home 1.2.0 alpha 4 rev. 1476>>

Здравствуйте, Klapaucius, Вы писали:
MC>>Ага, и идти отлаживать типы. Ненене.
K>Ну а в чем проблема-то?
http://rsdn.ru/forum/philosophy/3980805.aspx

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

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

MC>>Как это не аргумент? Тоже аргумент. Не везде же нам нужны тьюринг полные языки — часто достаточно тьюринг-неполных dsl.
K>На практике это не так. Сначала делается не тьюринг-полный ДСЛ, а потом кто-то ударяется лбом о неполноту и тьюринг-полноту добавляют. SQL сделали тьюринг полным, даже перловские регекспы, ЕМНИП, полны по тьюрингу. Ну вот теперь делают тьюринг полные системы типов, потому что существует спрос.
То-то последнее время слышатся крики, мол от регекспов избавляться надо. Типа сложные, неподдерживаемые и все дела.
Насчет SQL — возможность производить бесконечный объем выходных данных из конечного — весьма сомнительна, согласись.

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

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

а вообще мне не надо с этим боротся, это же мой хлеб

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

... << RSDN@Home 1.2.0 alpha 4 rev. 1227>>

Здравствуйте, Mr.Cat, Вы писали:

K>>Ну а в чем проблема-то?
MC>http://rsdn.ru/forum/philosophy/3980805.aspx

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

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

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

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

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

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

Точно.

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

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

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

Ну вот волшебная программа, производящая бесконечный объем выходных данных из конечного объема входных:

main = (print . cycle) =<< getLine

... << RSDN@Home 1.2.0 alpha 4 rev. 1476>>

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

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

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

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

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

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

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

Увеличивают и уменьшают по сравнению с чем? Фантастической ситуацией, когда несуществующие "правильные" люди пользуются несуществующими "правильными" инструментами не встречающимся на практике "правильным" способом?

... << RSDN@Home 1.2.0 alpha 4 rev. 1476>>

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

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

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

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

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

... << RSDN@Home 1.2.0 alpha 4 rev. 1227>>

Здравствуйте, Mr.Cat, Вы писали:

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

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

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

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

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

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

... << RSDN@Home 1.2.0 alpha 4 rev. 1476>>

Здравствуйте, Klapaucius, Вы писали:
K>Я-то имел в виду всякие комбинаторные парсеры и прочие EDSL такого рода, которые можно расширять как угодно.
Понятно, что edsl будет полон, если полон язык, куда он e. Но разве расширяемость предполагает полноту?

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

... << RSDN@Home 1.2.0 alpha 4 rev. 1476>>

Здравствуйте, Mr.Cat, Вы писали:
K>>PEG расширяют и приходят к левой рекурсии
MC>Так ведь левая рекурсия в КС-грамматиках устранима. Можно расширить в рамках КС и потом устранить рекурсию.
Тут надо бы мою мысль переформулировать:
1. Вопрос. Какие классы грамматик требуют тьюринг-полного языка для реализации распознавателя?
2. Парсинг — это разбор по грамматике плюс выполнение семантических правил. Предположим, грамматика — КС, тогда есть ли ситуации, когда семантические правила надо выражать исключительно на тьюринг-полном языке?

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

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

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

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

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

Пока ввести понятие "полезная функция" и сравнить класс полезных функций с классом вычислимых.

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

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

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

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

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

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

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

... << RSDN@Home 1.2.0 alpha 4 rev. 1227>>

Здравствуйте, 0x7be, Вы писали:

0>Коллеги!

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

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

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

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

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

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

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

0>P.S. Я в отпуске, так что отвечать буду нерегулярно.

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

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

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

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

Да, но я так понимаю, что для этого понадобится давать верификатору дополнительную информацию. В случае ТC системы типов будут только две грамматики записанные в сигнатуре.

... << RSDN@Home 1.2.0 alpha 4 rev. 1476>>

Здравствуйте, Трурль, Вы писали:

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

Нет, не должно, конечно. Но разговор и не об этом идет.

... << RSDN@Home 1.2.0 alpha 4 rev. 1476>>

Здравствуйте, 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>>

	От:	Mr.Cat
	Дата:	29.09.10 20:35
	Оценка:	+3

	От:	deniok
	Дата:	01.10.10 10:18
	Оценка:	8 (1) +1

	От:	dilmah
	Дата:	30.09.10 11:34
	Оценка:	1 (1) +1

	От:	Klapaucius
	Дата:	30.09.10 07:33
	Оценка:	6 (1)

	От:	Mr.Cat
	Дата:	30.09.10 08:12
	Оценка:	6 (1)

От:	PC_2	http://code.google.com/p/rsinterpretator/
Дата:	30.09.10 19:28
Оценка:

От:	gandjustas	http://blog.gandjustas.ru/
Дата:	29.09.10 20:23
Оценка:

От:	Курилка	http://kirya.narod.ru/
Дата:	30.09.10 21:16
Оценка: