Здравствуйте, vdimas, Вы писали:
V>Здравствуйте, thesz, Вы писали:
T>>Для стандартизации компонент типы нужны? Нужны.
V>Вот тут и упираемся, ибо сами типыпринципиально зависят от подробности конкретной задачи. Другое дело, что давно витает в воздухе идея стандартизировать св-ва типов, дабы можно было обобщать алгоритмы, в С++ на шаблонах и в некоторых функциональных это где-то работает на наглядном синтаксическом уровне (хотя на неявном уровне, на уровне ошибок компиляции, если тип не имеет нужного члена, поля или метода). А на популярных .Net или Java даже банальное сложение через контракты выглядит убого и работает так же в плане эффективности.
Дело не в юридической стандартизации, а во внедрениии в прикладное языкостроение достижений теории типов (и связанной с ней теории доменов). Если мы держимся в рамках соответствующей математики, то получаем довольно сильные гарантии правильности программы, прошедшей тайпчекер. Фактически большинство современных теорем-пруверов основаны на какой-то версии типизации лямбда-исчисления; сделать из этого удобный прикладной язык, не потеряв строгих гарантий — вот чэллендж сегодняшнего дня. А у типов современных массовых языков инструментарий их построения слегка бедноват и кривоват.
V>Тут вот периодически пробегает человек, который разрабатывает некое единое семантическое представление программ, ИМХО, из области попыток решить этот вопрос.
Тут опять проблема в кодификации этого семантического единства. На чем она будет основана — на общепринятом (делаем так, поскольку в большинстве современных языков так) или на Карри-Ховарде-Жирарде-Рейнолдсе-etc (делаем так, потому что система типов оказывается изоморфной некоторой богатой логической системе).
Здравствуйте, deniok, Вы писали:
D>Дело не в юридической стандартизации,
Пока что вершиной стандартизации является контракт (не обязательно тот, который сущность "interface" из некоторых языков).
D>а во внедрениии в прикладное языкостроение достижений теории типов (и связанной с ней теории доменов). Если мы держимся в рамках соответствующей математики, то получаем довольно сильные гарантии правильности программы, прошедшей тайпчекер.
Нужна идея, как синтаксически красиво объявлять произвольные по-сущности своей контракты. Например, изобрети синтаксис на контракт на банальный оператор + для призвольного типа и рядом — на поддержку некоей произвольной операции, выглядящей как посылка сообщения экземпляру.
D>Фактически большинство современных теорем-пруверов основаны на какой-то версии типизации лямбда-исчисления; сделать из этого удобный прикладной язык, не потеряв строгих гарантий — вот чэллендж сегодняшнего дня.
В непротиворечивый синтаксис всё упирается. Чем больше возможностей в языке (при нашем-то бедном алфавите значков или того хуже — институте ключевых слов), тем больше комбинаторно-вызываемых возможных неоднозначностей. Заметь, нотационный язык математики куда как богаче, чем возможности нашей клавы.
D>А у типов современных массовых языков инструментарий их построения слегка бедноват и кривоват.
Угу, потому как слегка "простоват", и то, в этой простоте стандарт современного развитого языка — это увесистый такой томик. Куда дальше? С этим что делать? Давай ИДЕЮ!
D>Тут опять проблема в кодификации этого семантического единства. На чем она будет основана — на общепринятом (делаем так, поскольку в большинстве современных языков так) или на Карри-Ховарде-Жирарде-Рейнолдсе-etc (делаем так, потому что система типов оказывается изоморфной некоторой богатой логической системе).
У него задумка чуть круче (ибо задумка — минимум ограничений на модель, т.е. при желании много чего сделать можно), мы вот разве что за реализацию боимся, хотя я, лично, может и доживу до первой подобной системы — суть базы знаний нашей многострадальной IT. (интересно, автор это понимает?)
Здравствуйте, vdimas, Вы писали:
V>Нужна идея, как синтаксически красиво объявлять произвольные по-сущности своей контракты. Например, изобрети синтаксис на контракт на банальный оператор + для призвольного типа и рядом — на поддержку некоей произвольной операции, выглядящей как посылка сообщения экземпляру.
Тут как раз есть масса разных подходов, причем даже известно, как ad hoc полиморфизм сводить к параметрическому (в Хаскелле класс типов транслируется в словарик, передающийся как неявные аргументы функции, типа VTBL, но привязанная не к объекту, а к функции). Вот пример проблемы, в принципе решенной, но требующей использования более богатых систем, чем используемые сейчас в мэйнстриме: написать контракт, гарантирующий на входе функции сортированность массива. Динамическая проверка требует O(N) времени. Поэтому хочется статической — во время компиляции. На зависимых типах такие контракты писать можно, причем не с помощью закулисной машинерии, а от первооснов, на языке типов. Но депендент-тайп-комьюнити пока еще не создало язык, про который бы все сказали "да, это готово к тому, чтобы идти в массы." Ситуация напоминает середину 80-х в функциональном программировании: есть куча очень похожих языков, надо поиграть с деталями и родить общепризнанно хороший результат (так в конце 80-х Хаскелл появился).
V>В непротиворечивый синтаксис всё упирается. Чем больше возможностей в языке (при нашем-то бедном алфавите значков или того хуже — институте ключевых слов), тем больше комбинаторно-вызываемых возможных неоднозначностей. Заметь, нотационный язык математики куда как богаче, чем возможности нашей клавы.
Это не проблема, математики не вырисовывают же квантор общности нигде, кроме как на доске, а пишут в TeX'е \forall. Ну и программисты на Хаскелле пишут forall, а при публикации статей\документации это превращается в квантор общности
D>>А у типов современных массовых языков инструментарий их построения слегка бедноват и кривоват.
V>Угу, потому как слегка "простоват", и то, в этой простоте стандарт современного развитого языка — это увесистый такой томик. Куда дальше? С этим что делать? Давай ИДЕЮ!
Я боюсь меня побьют. Но намекну. Определение бестипового лямбда-исчисления: две операции (аппликация и абстракция) и одно правило редукции (бета, ну можно ещё альфа-редукцию для практических целей). Это дает все исчисление. Типизация исчисления — это ещё несколько правил, порождающих чистую систему типов (PTS). Добавим сюда индуктивные типы (еще несколько правил) и получим уже систему типов, с которой можно жить. В том смысле, что у нас есть универсальное ядро, а все более высокоуровневые конструкции можно декларировать в терминах трансляции в это ядро. Причем заметь, процесс этой трансляции может верифицироваться ядром, как уже рабочей системой.
То есть Стандарт — не юридический текст на человеческом языке, а формальная система с формализованными (а значит верифицируемыми) синтаксисом и семантикой.
Главное, чтобы инженерные вопросы (типа эффективного представления Integer, Float и строк) не шли в ущерб формальной целостности.
D>>А у типов современных массовых языков инструментарий их построения слегка бедноват и кривоват. V>Угу, потому как слегка "простоват", и то, в этой простоте стандарт современного развитого языка — это увесистый такой томик. Куда дальше? С этим что делать? Давай ИДЕЮ!
А ты почитай то, про что deniok пишет. Вот тебе и идея.
Стандарт современного развитого языка как охапка хвороста — объём большой, а весу мало. Тогда, как описание той же теории типов с основными теоремами (но без их доказательств) "уместится на полях этой книги", перефразируя Ферма.
D>>Тут опять проблема в кодификации этого семантического единства. На чем она будет основана — на общепринятом (делаем так, поскольку в большинстве современных языков так) или на Карри-Ховарде-Жирарде-Рейнолдсе-etc (делаем так, потому что система типов оказывается изоморфной некоторой богатой логической системе).
Вот про это и читай, ага.
Yours truly, Serguey Zefirov (thesz NA mail TOCHKA ru)
T>>Для стандартизации компонент типы нужны? Нужны. V>Вот тут и упираемся, ибо сами типыпринципиально зависят от подробности конкретной задачи. Другое дело, что давно витает в воздухе идея стандартизировать св-ва типов, дабы можно было обобщать алгоритмы, в С++ на шаблонах и в некоторых функциональных это где-то работает на наглядном синтаксическом уровне (хотя на неявном уровне, на уровне ошибок компиляции, если тип не имеет нужного члена, поля или метода). А на популярных .Net или Java даже банальное сложение через контракты выглядит убого и работает так же в плане эффективности.
Type erasure спасёт отца русской демократии.
V>Тут вот периодически пробегает человек, который разрабатывает некое единое семантическое представление программ, ИМХО, из области попыток решить этот вопрос.
1972 год.
Ученик Колмогорова Пер Мартин-Лёф разработал первую версию теории типов.
Пер Мартин-Лёф никогда не прибегал на RSDN.
Yours truly, Serguey Zefirov (thesz NA mail TOCHKA ru)
Здравствуйте, deniok, Вы писали:
V>>В непротиворечивый синтаксис всё упирается. Чем больше возможностей в языке (при нашем-то бедном алфавите значков или того хуже — институте ключевых слов), тем больше комбинаторно-вызываемых возможных неоднозначностей. Заметь, нотационный язык математики куда как богаче, чем возможности нашей клавы.
D>Это не проблема, математики не вырисовывают же квантор общности нигде, кроме как на доске, а пишут в TeX'е \forall. Ну и программисты на Хаскелле пишут forall, а при публикации статей\документации это превращается в квантор общности
<skip>
D>Определение бестипового лямбда-исчисления: две операции (аппликация и абстракция) и одно правило редукции (бета, ну можно ещё альфа-редукцию для практических целей). Это дает все исчисление. Типизация исчисления — это ещё несколько правил, порождающих чистую систему типов (PTS). Добавим сюда индуктивные типы (еще несколько правил) и получим уже систему типов, с которой можно жить. В том смысле, что у нас есть универсальное ядро, а все более высокоуровневые конструкции можно декларировать в терминах трансляции в это ядро. Причем заметь, процесс этой трансляции может верифицироваться ядром, как уже рабочей системой.
D>То есть Стандарт — не юридический текст на человеческом языке, а формальная система с формализованными (а значит верифицируемыми) синтаксисом и семантикой.
D>Главное, чтобы инженерные вопросы (типа эффективного представления Integer, Float и строк) не шли в ущерб формальной целостности.
Вот хороший пример с ТеХ, насколько такие программы будут читабельны?
Здравствуйте, vdimas, Вы писали:
V>Вот хороший пример с ТеХ, насколько такие программы будут читабельны?
Ты о чём? Мне писать удобней и быстрее
forall x . P x
А читать приятнее
Это все настолько эквивалентно, что нет совершенно никакой разницы как писать или читать. Транслируй в то представление, которое сегодня больше нравится и не переживай о читабельности.
Здравствуйте, deniok, Вы писали:
V>>Вот хороший пример с ТеХ, насколько такие программы будут читабельны?
D>Ты о чём? Мне писать удобней и быстрее D>
D>forall x . P x
D>
D>А читать приятнее
D>
D>Это все настолько эквивалентно, что нет совершенно никакой разницы как писать или читать. Транслируй в то представление, которое сегодня больше нравится и не переживай о читабельности.
Р должно что-то делать с типом (X x), т.е. X должен поддерживать некий контракт, который неплохо как-то продекларировать на уровне Р.
Здравствуйте, vdimas, Вы писали:
D>>
V>Р должно что-то делать с типом (X x), т.е. X должен поддерживать некий контракт, который неплохо как-то продекларировать на уровне Р.
Пока что это не более чем применение терма P к терму x, живущему под квантором общности. Чтобы придать этому какой-то специальный смысл надо определить исчисление, с которым идет работа. Например в Жирарда P будет конструктором типа с кайндом *->*.
Я к тому, что до деклараций контрактов и самого понятия контракта тут далековато. Пропозициональную логику высшего порядка построить можно, да.
Здравствуйте, deniok, Вы писали:
D>Я к тому, что до деклараций контрактов и самого понятия контракта тут далековато.
Тогда и смысла в этом мало.
В математической нотации подобное выражение могло встречаться в разных местах, и быть по-сути:
— аксиомой
— условием
— операцией
— еще что-то
Сдается мне, что нас интересует предпоследнее для фактической применимости в ЯП. Я напираю на контракт лишь потому, что скриптово-динамических языков и так уже хватает. Хочется каким-то образом получить свободу выражения выч.логики в рамках статической типизации. А это означает, что нам нужны ограничения на св-ва типов, то бишь определённого рода контракты.
Здравствуйте, vdimas, Вы писали:
V>- аксиомой V>- условием V>- операцией V>- еще что-то
V>Сдается мне, что нас интересует предпоследнее для фактической применимости в ЯП. Я напираю на контракт лишь потому, что скриптово-динамических языков и так уже хватает. Хочется каким-то образом получить свободу выражения выч.логики в рамках статической типизации. А это означает, что нам нужны ограничения на св-ва типов, то бишь определённого рода контракты.
Ну так P x и есть применение P к x, то есть, иными словами, операция. Другое дело, что мы ещё не решили, какие зависимости допустимы. Например, P — терм, x — терм (банально); P — тип, x — тип (слабая лямбда омега, конструируемые типы) ; P — терм, x — тип (явный полиморфизм, то есть лямбда2); и, наконец, P — тип, x — терм (зависимые типы). И еще мы не решили можно ли задавать соответствующие лямбда-абстракции: \тип . тип, скажем.
А что такое "выч.логика" — я не очень понимаю. Если пытаться описать это понятие формально, то мы приходим к какой-то формальной логической системе. Вот как раз разные типизации лямбда-исчисления эквивалентны разным логическим системам. Скажем система лямбда2 эквивалентна пропозициональной логике второго порядка. И в ней можно много чего записать. Скажем, ex falso sequitar quodlibet, то есть "изо лжи следует что угодно". Вводим для обозначения лжи
и получаем
Здесь тип (правые скобки) — теорема, а лямбда-терм с этим типом (левые скобки) — ее конструктивное доказательство. (Если некоторый тип населён, то есть существуют термы с таким типом, то теорема, выраженная типом верна, то есть любой терм этого типа — доказательство).
Системы с зависимыми типами гораздо богаче, поскольку они позволяют выразить естественным образом различные логики предикатов, а не только пропозициональные.
Здравствуйте, YoungPioneer, Вы писали:
YP>Просьба оценить идею:
YP>Каждая программа будет состоять из файлов-модулей — похоже на нынешние .dll библиотеки. Главное отличие — интерфейсная часть основных модулей — стандартизована, подобно тому, как сейчас стандартизованы интерфейсы составных частей компьютера — процессор, жесткий диск и т.д.Любой производитель может начать выпуск мониторов, причем работать они будут даже без нового драйвера — в Windows предусмотрен "стандартный монитор".
... YP>Реализована такая модель может быть на уровне com, .net или других системах и языках программирования. Главное — стандартизация, принимаемая большинством.
YP>Заранее благодарен за комментарии.
Небольшой оффтоп. Недавно бывал в будущем, правда более отдаленном, чем вы. Не могу не поделится некоторыми впечатлениями.
Особенно понравилась идея распределенных вычислений. В 2874 году, из которого я как раз вернулся, этот метод позволяет с помощью одного обычного x86-процессора добиться мощности и распараллеливания, недостижимого самыми мощными суперкомпьютерами нашего времени. Вы наверное спросите почему в 2874 году используют именно x86 процессоры. Всё очень просто, объясняю: берется оди единственный x86-процессор, экземпляр какого-нибудь 1980 года, и с помощью языка TSPL (Time-Space Processor Language) (это язык программирования пространства-временных характеристик) программируется таким образом, чтобы в течение необходимого для вычислений промежутка времени выполнить задачу. Допустим, мы можем запрограммировать x86 таким образом, чтобы с 1980 по 2100 год, в перерывах между своими прямыми вычислениями, процессор занимался вычислением нужной нам задачи. Владелец x86 обычно ничего не замечает в этом случае.
Результаты вычислений считываются также с помощью средства TSPL и записываются в любые пространственно-временные структуры, чтобы к моменту, когда эти результаты потребуются, их можно было бы легко прочитать. Запись и считывание с помощью пространственно-временных структур — вещь достаточно захватывающая, но на пальцаз её объяснить трудно. Попытаюсь это сделать, приведя несложный пример. Если наш x86 стоит в компьютере верстальщика, то результаты вычислений можно записываться в виде распределения опечаток и отклонений букв в печатных материалах. Главное требование — гарантировать что к моменту считывания результатов эти структуры должны быть доступны (в нашем примере печатные материалы будут в 2874 году доступны в электронных библиотеках всемирной истории и опечатки, а также пространственные микро-отклонения букв можно будет с легкостью считать, зная исходный алгоритм (в TimeLang это называется "матрица считывания")).
Настящие гуру TSPL в 2874 году для записи результатов используют опосредованное программирование нагрузки винчестеров в наших сегодняшних кластерах и как результат — их микро-влияние на климат, а считывание происходит в результате разностного анализа исторических погодных данных (разность ожидаемой рассчитанной погоды погоды и актуальной, вызванной влиянием нагрева винчестеров планеты).
Так что, как видите, выбор структур, как и вообще программирование на TSPL, в некотором роде является искусством. Ведь в каждом конкретном случае нужно выбрать какие структуры использовать и как их потом считывать.
Аппаратной платформой для TSPL служит пространственно-временной континуум и небольшая машина времени, способная засылать в прошлое электрические импульсы, которая будет создана в 2554 году. До создания TSPL пройдет ещё несколько сотен лет.
Грандиозным и непостижимым парадоксом использования TSPL является то, что все результаты вычислений этого языка уже записаны в пространстве-времени. В 2874 году исследователи изучают вопрос — не является ли наша Вселенная исключительно агрегированной массой результатов всевозможных вычислений, не является ли каждый проходящий в ней процесс вычислителем, инициированным чьими-то вычислениями? Одна из исследовательских групп, которую я посетил, занимается интересным и захватывающих вопросом — они пытаются раскодировать результаты без использования матрицы считывания (как я говорил выше, такая матрица позволяет вам правильно прочесть результаты ваших вычислений), т.е. анализируя любые-прелюбые всевозможные данные, они пытаются вычислить такие матрицы и на их основе прочесть результаты. Естественно, для своих невероятно громоздких комбинаторных перестановок и вычислений они тоже используют средства TSPL.
Нет сомнений, что какие-то языковые особенности данного текста также являются частью результатов чьих-то TSL-вычислений.
P.S. Кроме TSPL там есть и другие языки. Например NIL (Nature Influence Language) — язык природных влияний. Он позволяет обойтись без процессоров (ибо TSPL ограничен периодов когда первые процессоры были изобретены). NIL позволяет с помощью машины времени засылать в прошлое микро-изменения природных характеристик таким образом, чтобы законы природы сами являлись вычислителем. Принцип считывания остается аналогичным TSPL, но теперь считывать можно не только артефакты работы процессоров, как в случае с TSPL, но и характеристик природных явлений к нужному моменту (например написали программу на NIL в 2874 году, запустили, и сразу же считываем результаты например с географической карты очертаний материка и интерпретируем их с помощью матрицы считывания). Глубже понять суть NIL мне не удалось, поэтому боюсь не смогу объяснить принцип его работы.
Здравствуйте, Erop, Вы писали:
E>Заботай MAC OS X, в области Cocao, а MAC OS Classic в области AE... Там нечто очень похожее есть и уже много лет работает...
А можно хороших ссылок на обзоры/инфу о программирование под Cocoa в частоности и МакОсь в общем? Поиском то ли пользоваться не умею, то ли не везёт: всё время какие-то юзерские странички попадаются, не программерские.
То, что описал YoungPioneer — в принципе, и есть идеал программирования.
Собирать программы из частей как из конструктора — это же и есть идеал компонентной модели, — RAD, то к чему стремится .Net, .Java, объектно-ориентированное программирование вообще.
Другое дело, что с программами так просто все не получается. Слишком сложны к ним требования. Просто так интерфейсы на все случаи жизни не разработаешь.
В некоторых конкретных случаях это уже сделано: библиотеки UI Control'ов, plug-in'ы, аудио- и видеофильтры от разных разработчиков (VST, DirectX), которые можно последовательно соединять, получая фильтры любой сложности, еще, наверно, можно найти много примеров.
Но в общем случае это невозможно, не существует соответствующего подхода.
Такой метод, позволяющий любые программы сводить к набору стандартных компонентов, легко соединяющихся друг с другом, несомненно, произвел бы революцию в программировании.
То, что описал YoungPioneer — в принципе, и есть идеал программирования.
Собирать программы из частей как из конструктора — это же и есть идеал компонентной модели, — RAD, то к чему стремится .Net, .Java, объектно-ориентированное программирование вообще.
Другое дело, что с программами так просто все не получается. Слишком сложны к ним требования. Просто так интерфейсы на все случаи жизни не разработаешь.
В некоторых конкретных случаях это уже сделано: библиотеки UI Control'ов, plug-in'ы, аудио- и видеофильтры от разных разработчиков (VST, DirectX), которые можно последовательно соединять, получая фильтры любой сложности, еще, наверно, можно найти много примеров.
Но в общем случае это невозможно, не существует соответствующего подхода.
Такой метод, позволяющий любые программы сводить к набору стандартных компонентов, легко соединяющихся друг с другом, несомненно, произвел бы революцию в программировании, но пока что его не видно даже на горизонте.
(интересно, автор это понимает?)
