Здравствуйте, VladD2, Вы писали:
WH>>В любом случае все последующие апелляции к С++ будут игнорироваться. Ибо язык сильно не той системы. VD>А есть другие источники данных?
Немерле подойдет? Дело в том что нет никаких основания считать что диагностика будет хуже чем в немерле при выводе типов.
VD>Не...а. Отладчики пока что не умеют отлаживать вычисления в типах. Более того оные проходят в недрах компилятора и выделенной фазы не имеют.
Так это от типов и компилятора зависит.
В данном случае метакод это обыкновенный код просто выполняется оптимизатором.
VD>А с чего бы это код не отличим от метакода? Ты не забыл, что это не Немерле. В Ur предлагается писать метакод на базе типов высшего порядка. Как я понимаю — это совершенно другой язык нежели прикладной.
Там все метапрограммирование основано на хитром fold'е который умеет сворачивать типы.
VD>Возможно ты прав. А возможно нет. Без экспериментов и научной базы это не установить.
Я очень редко ошибаюсь на счет алгоритмов.
VD>Ага, но проблемы могут быть те же. Напомню, проблемой являлась очень сильная связанность. Когда типы уже выведены преобразовывать что-то становится весьма сложно, так как все цепляется друг за друга.
А там нет преобразований AST как таковых.
Там все основано на частичных вычислениях.
Те мы просто пишем код в котором очень много вычислений происходит над константами времени компиляции(типы в частности).
Далее все вычисления которые зависят исключительно от констант проводит компилятор.
А благодаря тому что константы у нас попадаются весьма интересные, а именно типы и имена челенов типов то мы можем получать МП на всю катушку.
VD>>>А вот на счет строгости вообще большие сомнения. Как раз макра отдаляет все очень хоршо. Макры понятны и очевидны. WH>>Тебе. WH>>А лично меня очень сильно напрягают совершенно не формализованные потроха компилятора. VD>Причем тут форматирование?
Где в моей цитате слово форматирование? Там есть немного похожее слово имеющее сильно другое значение.
Пожалуйста читай более одного раза если тебе кажется что я написал что-то не то.
VD>Макры — это программа которая очевидна. А вот код высших порядков — это еще то приключение. Хаскель замечательно демонстрирует, что об него можно хребет переломать. Или хаскель — это тоже не показатель? ОК. А что показатель?
Ну ты эта посмотри код на Ur/Web что-ли.
Причем я думаю что если поработать над синтаксисом его можно сделать еще проще.
VD>А это хорошо? Да и откуда это следует? Я вот с легкостью понимал, что происходит в примерах этого Ur-а, но когда дошел до метакода, то тихо поплыл и запутался. А я (межуд прочем) в потрахах компилятора таки разобрался (ну, типа не совсем ванька дурак).
Просто автор Ur'а как и большинство ученых страдает острой формой формализма.
Я уверен что там все можно переделать гораздо более человечески.
WH>>Но благодаря частичному выполнению весь оверхед связанный с обсчетом констант вообще и типов в частности исчезает. WH>>Те фактически раскруткой метакода у нас занимается оптимизатор. VD>Мне кажется от слов нужно перейти к примерам.
VD>Ну, структуры БД и время можно представить неизменяемой структурой данных. VD>Остается вопрос как из метакода получить эту информацию. Причем не из ресурсво, а из компьютера, сети и любого другого источника информации. Динамика и правда не нужна. Но данные нужны.
Я оставлю свою цитату (там ответ есть. пожалуйста отвечай не построчно.): WH>>Все что нужно это научить компилятор на этапе компиляции вызывать функции которые обращаются к внешним источникам данных, обрабатывают их выхлоп и возвращают некую неизменяемую структуру данных.
VD>В макрах, код макры и есть любая функция которая вольна делать все что ей угодно.
Это кстати далеко не всегда хорошо.
VD>Получается макры таки имеют преимущества и если их не воспроизвести, то грош-цена такому метааппарату.
Во первых полезность обращения к внешним ресурсам мягко говоря несколько преувеличена.
Во вторых мы можем во время компиляции обратиться к внешним ресурсам и запихнуть ответ в ресурсы модуля. Ресурсы модуля это по сути именованные и разумеется типизированные константы.
Короче возможности как минимум сравнимы с теми что есть у немерловых макросов.
VD>Это и есть куча? В прочем, согласен, что это не красиво. Вот только назвать это кучей приседаний у меня язык не поворачивается.
А оно тянет за собой весьма не мало.
В частности алгоритмы поиска решений подходящих под ограничения идут лесом почти со 100% вероятностью.
А они тут ИМХО весьма кстати.
VD>В прочем, ОК. Продемонстрируй как такой макрос будет выглядеть на типах высших порядков и сравним.
Это будет очень не честное сравнение...
А не честное по тому что все коллекции в таком языке будут реализовывать класс типов который умеет Fold или как минимум имеют метод Fold...
//имя и тип
syntax foreach : Expression
//правило для PEG
rule "foreach" "(" name : Identificator "in" collection : Expression ")" body : Expression
//переписываем
code
<[ _ = ($collection).Fold({}, ($name, _) => _ = $body; {}; end )]>
end
//{} это кортеж из 0 элементов. Универсальная заглушка вместо void.
Если же у нас тяжелый случай и ничего объединяющего нет то мы просто напишем набор перегруженных функций. И будет тоже самое.
И работать будет быстро ибо бекенд у нас заточен на оптимизацию ФВП и не только.
VD>Ты почитай с чего начинает автор. Он там в первых строках начинает разговор о невозможности гарантировать окончания компиляции в общем случае и о введении ограничений чтобы это обойти, говорит.
Это из-за зависимых типов. Для них вывод типов в общем случае задача не разрешимая. Но если ввести некоторые ограничения и эвристики то все получится вполне по человечески.
В немерле кстати тоже вывод типов далеко не полный.
VD>Прикрути его изыски к системе типов дотнета и может статься, что этого монстра уже никто никогда не сможет понять или реализовать.
Вот чего я не стану делать точно так это брать за основу систему типов .НЕТа. Ибо оно то еще убожество.
Все что нужно добавить в ту систему типов это сабклассинг для ООП и слово mutable для императивщены.
Ни то ни другое на выводе типов практически не отразится.
VD>Где там единообразие? Ты даже к ресурсам обратиться не можешь.
Это ты только что придумал.
Давай ты не будешь искать фатальные недостатки читая все по диагонали.
VD>В нем этот код можно материализовать (сгенерировать текст) и посмотреть. А что будем делать с сообщениями об ошибках при обработке "35-го" порядка?
Весь код у тебя уже есть.
Это исходник.
А ошибки там могут быть только из-за не правильного вывода типов в исходнике.
WH>>Так что это нужно всем компиляторам... VD>Ты пробовал ставить и использовать этот самый Ur?
Да при чем тут вообще ур?
Я говорю про подобные системы в принципе.
VD>>>ICE — это ошибка в компиляторе. Неверно предположение программиста писавшего часть кода компилятора, или изменения в другой части компилятора повлиявшее на ту часть в которой возникло ICE. Так что ICE может быть в любом компиляторе (и есть в любом). WH>>Ну да. WH>>Только если верификатор поймал ошибку в сгенерированном компилятором коде то это самое натуральное ICE. Ибо компилятор не должен генерировать неправильный код. VD>С макрами все просто.
Тут разговор идет про фронтенд. Фронтенд производит только простейшие переписывания типа того что я показал выше.
WH>>Считай это встроенным в компилятор PEVerify VD>Звучит хорошо... в теории.
Если платформу бутстрапить то это будет практикой.
VD>Что наоборот? Тебе ничего не придется делать и все чудесным образом интегрируется в IDE?
Все что нужно для IDE это выводить типы.
Про макросы ей знать не надо.
WH>>Я даже где то видел статью в которой зависимыми типами проверяли дерево в интерпретаторе. WH>>Тут ровно тоже самое. WH>>Так что это даже не подозрение, а почти 100% уверенность. VD>"почти 100% уверенность" — это надо запомнить!
И чего ты тут ехидничаешь?
Даже если я не смогу на 100% проверить результирующий AST при помощи ЗТ все равно верификатор будет очень сильно проще чем делать его без ЗТ.
VD>Смотрел. Он есть и работает в 10 раз лучше встроенного в шарп. А где посмотреть на аналог на ЗТ?
Выше...
VD>Пойми, я не спорю, что в этом что-то есть. Но так же я жопой чую, что в это есть куча проблем, а "правильное решение" (с) где-то по середине. Я так же как ты "почти 100% уверен", что без связи с внешним миром МП — это вещь в себе которая никому не нужна.
А давай ты будешь читать то что я пишу. Ладно?
VD>Знаешь сколько красивых идей я выбросил (за свою жизнь) только потому, что на практике в них оказалось очень много нюансов? R#-помнишь? И это только верхушка айсберга. Алгоритмов было намного больше.
Помню. А еще я помню что понял при первой попытке это использовать что это то еще унылое...
Немерловые макросы сильно лучше но из-за того что нужно постоянно дергать потроха компилятора тоже не фонтан.
VD>Дык я тоже не считаю его совершенством. Просто по совокупности факторов для реальной работы ничего лучше (для меня) нет. Мне не интересны проекты-игрушки. Мне интересна разработка для реального мира. В этом реальном мире есть тонны библиотек для того же дотнета и явя и плевать на них нельзя.
Я это все прекрасно понимаю.
Но если постоянно придерживаться данной логике то писали бы сейчас на ассемблере.
Так что если будет действительно мощный язык очень многие ему простят отсутствие мегафреймворка.
Посмотри на питон и руби хотя бы.
VD>Да и бэкэнд компилятора тоже не игрушка. Писать его только для того, чтобы создать более удобный ЯП — это маразм.
А тут просто выбора нет. Максимум что можно использовать это LLVM.
VD>Те же ЗТД — это интересная идея. Весьма перспективная. Но законченной концепции и тем более решения на них нет и не будет ближайшие 5 лет.
А я знаю. Но это не мешает мне вести исследования в этом направлении.
VD>Лично мне не нужен язык тольтко потому, что в нем реализованы некие ЗТД. Мне нужен язык решающий мои проблемы как программиста. Если ЗТД помогут мне в этом — замечательно. Если нет, ну и хрен бы с ними. В любом случае они должны решать те проблемы которые нужно решать мне, а не я должен подстраиваться под их ограничения. В общем, дизайн не должен вестись от возможностей. Он должен вестись от потребностей.
Это все понятно.
ЗТ нужны как минимум для того чтобы отловить очень большое количество ошибок.
А это реальное сокращение времени отладки программы.
Да и оптимизатору они помогут очень не слабо.
VD>Этого мало. Если ты хочешь чтобы нужный тебе язык появился, то единственное верное решение — это сделать его самому. Ну, или примкнуть к тем кто уже это делает.
Я в курсе.
Проблема в том что я пока не знаю какой конкретно язык я хочу.
У меня есть набор требований но в единую систему типов я их пока не укатал.
VD>Так можно всю жизнь прождать.
Я ничего не жду.
Я просто не знаю в каком конкретно направлении копать.
Немерле точно не то направление.
Ибо мне система типов нужна более мощная и формальная чтобы можно было рассуждать о программе.
Яркий пример IEnumeraor[T] реализующий IDisposable.
Пока дело ограничивается одним foreach все хорошо. А если появляются ФВП у меня крышу сносит от попытки понять кто Dispose делать будет.
VD>Вот простой вопрос. Если у нас есть макросы, то мы можем оформлять их синтаксис с использованием EBNF (как мы это обсуждали). При этом сложность распознавания синтаксиса перекладывается на механизмы автоматического построения парсеров (встроенного в язык). А как быть с метасистемой построенной на базе ЗТД?
Так я уже говорил.
Просто на уровне синтаксиса тупо переписываем при помощи PEG'а и все. См про foearch.
Пусть это будет просто:
просто, как только можно,
но не проще.
(C) А. Эйнштейн
Здравствуйте, VladD2, Вы писали:
VD>Здравствуйте, WolfHound, Вы писали:
WH>>А мне подход с системой типов нравится гораздо больше. WH>>1)Мы в очень широком смысле не можем написать метафункцию не правильно. VD>Опыт исползования МП в С++ убеждает меня в обратном. VD>Опять же достоаточно взглянуть на С++.
Посмотри на Agda2.
Yours truly, Serguey Zefirov (thesz NA mail TOCHKA ru)
Здравствуйте, thesz, Вы писали:
T>Сие позволяет мне заявить, что товарищи из Scala слегка поотстали от жизни в Хаскеле.
Если ты выносишь параметр монады в параметры класса, то open functions не нужны, MPTC достаточно:
class Monad m a b where
return :: a -> m a
(>>=) :: m a -> (a -> m b) -> m b
instance (Ord a, Ord b) => Monad Set a b where
return a = singleton a
g >>= q = bindSet g q
Здравствуйте, Andrei F., Вы писали:
N>>Насколько я понял, там поддерживается kind polymorphism, что довольно уникально.
AF>А можно объяснить идею вкратце?
kind — это как бы тип типа. Он включает себя количество типов-параметров, принимаемых данным типом, их kinds, а в некоторых языках (например, Scala) — их вариантность и констрейнты.
kind polymorphism — это возможность написать код, type variables в котором могут быть инстанциированы типами с различными kinds.
Здравствуйте, nikov, Вы писали:
VD>>Не...а. Отладчики пока что не умеют отлаживать вычисления в типах.
N>Кстати, Одерски планирует прикрутить к Scala отладчик типов. Пока ещё не совсем ясно, как это будет выглядеть.
А что, их система типов полна по Тьюрингу?
Есть логика намерений и логика обстоятельств, последняя всегда сильнее.
Здравствуйте, VladD2, Вы писали:
VD>А что, их система типов полна по Тьюрингу?
Насколько я знаю, система типов в стандартной Scala позволяет выразить примитивно-рекурсивные функции, а расширения языка (флаг компилятора -Yrecursion) — любые рекурсивные функции (соответственно, typechecker может зависать в этом режиме). Но я не берусь это продемострировать.
Здравствуйте, nikov, Вы писали:
N>Насколько я знаю, система типов в стандартной Scala позволяет выразить примитивно-рекурсивные функции, а расширения языка (флаг компилятора -Yrecursion) — любые рекурсивные функции (соответственно, typechecker может зависать в этом режиме). Но я не берусь это продемострировать.
При -Yrecursion ты должен явно задавать максимальную глубину рекурсии.
L>Здравствуйте, nikov, Вы писали:
N>>Насколько я знаю, система типов в стандартной Scala позволяет выразить примитивно-рекурсивные функции, а расширения языка (флаг компилятора -Yrecursion) — любые рекурсивные функции (соответственно, typechecker может зависать в этом режиме). Но я не берусь это продемострировать.
L>При -Yrecursion ты должен явно задавать максимальную глубину рекурсии.
L>А демонстрировать чего там L>
L>type T = { def foo(bar: T) }
L>
L>
Ну это не доказательство возможности представления любой рекурсивной функции.
Ты попробуй написать программу, на которой type checker останавливается только в том случае, если существует четное число, большее 2, не представимое в виде суммы двух простых чисел.
Здравствуйте, nikov, Вы писали:
N>Ты попробуй написать программу, на которой type checker останавливается только в том случае, если существует четное число, большее 2, не представимое в виде суммы двух простых чисел.
Кстати, интересно было бы посмотреть на это и на других языках (Haskell, C++).
Здравствуйте, nikov, Вы писали:
N>Ну это не доказательство возможности представления любой рекурсивной функции.
Конечно, не доказательство, оно же не компилируется!
N>Ты попробуй написать программу, на которой type checker останавливается только в том случае, если существует четное число, большее 2, не представимое в виде суммы двух простых чисел.
Ой-ой-ой... Сейчас вечер. Я и не на типах то такое не напишу.
На параллельный пост — на Haskell система типов является Тьюринг-полной. Достаточно включить UndecidableInstances.
Здравствуйте, Qbit86, Вы писали: Q>Например, в сочетании «это ваше Немерлo» Или: «закрой Немерлo!»
Всякому образованному человеку очевидно, что Немерло — это N'est Merlot, такое вино.
... << RSDN@Home 1.2.0 alpha rev. 677>>
Уйдемте отсюда, Румата! У вас слишком богатые погреба.
Здравствуйте, WolfHound, Вы писали:
WH>Пожалуйста сравни надежность обероновских программ с надежностью программ вот на этом языке WH>http://www.impredicative.com/ur/
Хм... отвал башки. Настолько очевидная концепция, что как впечатление остается лишь вопрос: "почему этого не было еще лет 10 назад?"
