[@] о трансляции

ИМХО ослаблять проще, ибо если при усилении вылезет ошибка типизации, которой не было в исходном языке, как ее решать?

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

> и, в общем случае, как системы типов исходного/результирующего языка влияют на трансляцию?

влияет на то, проще будет сделать кодогенератор или сложней. Например, был пример фракталы/мозаика на лиспе -- написал человек скринсейвер на Си, потом переделал на лиспе, откомпилировал sbcl/Lispworks/clisp/etc и померял -- разница в 10..30 раз Си/лисп. Запостил в comp.*.lisp, его пример там пооптимизировали, свели в итоге разницу к 2-3 раза. Из дизассемблированного sbcl конечного варианта было видно, что назначение регистров sbcl проводит не оптимально.
Поэтому для такого конкретного примера проще не заморачиваться с эффективным кодогенератором и писать руками часть на Си, часть на лиспе, встраивать Си в лисп или наоборот. Например, взять что-то вроде Lush или ECL, отпрофилировать и переписать узкие места на встроенном Си или компилируемом CLush. CLush в каком-то смысле можно посмотреть как пример "усиления типизации" -- переводится наоборот, лисповый код в си, и компилируется си компилятором, но он немного нечестный по сравнению с Haskell+C++(sweeny.pdf) , там была нормальная выводимая система типов, а тут предполагается ручная расстановка типов.
Упрощать проще, но какая цель трансляции, получить более эффективный код или более гибкую, расширяемую модель исполнения? Если более эффективный для компиляции, то тут надо как-то сохранять целостность семантики модели. Можно посмотреть проект Harmony в Беркли, http://www.seas.upenn.edu/~harmony/ , на тему "линз" . Ещё был какой-то Harmony где делали плагин к Хемаксу, что-то вроде семантического представления на разных языках -- можно было написать кусок на яве, кусок на Common Lisp, а плагин показывал исходник в унифицированном виде. Ссылку не помню.

> если желаемым результатом является эквивалентная исходной программа?

а в чём цель перевести программу из одного языка/парадигмы в другую? Почему нельзя работать в одном языке целиком или "встраивать руками"?

> есть ли такое же для каких-нибудь не-Чёрчевских языков (того же C, или BASIC, или кто там у нас попроще)?

то есть, свести императивный алгоритм на Си к эквивалентной "функциональной" программе? или просто свести к каким-то базовым "императивным" операциям, по аналогии с "функциональными" комбинаторами (вроде Дейкстра ещё писал про ветвление, цикл, переходы/рекурсию?)

> есть ли такое же для каких-нибудь не-Чёрчевских языков (того же C, или BASIC, или кто там у нас попроще)?

можно посмотреть "компилятор схемы за 90 минут" (из схемы в си) или MBase лисп (из паскаля/бейсика/DSL в лисп и из него в стековый .NET-байткод, JVM или регистровый)

> а в чём цель перевести программу из одного языка/парадигмы в другую?

В том, что для более простой и строго определённой модели проще делать выводы относительно свойств кода. Так же, в несколько этапов проще компилировать.

> ибо если при усилении вылезет ошибка типизации, которой не было в исходном языке, как ее решать?

расширением без потери точности (int->long->double) или выводимой системой типов в общем случае

Угу. То есть, трансляция/трансформация как формализация метамодели относительно свойств "системы". Общая метамодель в целом задаёт поведение системы в целом, частные модели/спецификации метамодели решают конкретную задачу оптимальным для неё способом.
Просто интересно, можно ли из одного и того же кода генерировать или правильную, но медленную универсальную, лучше распараллеливающуюся формальную модель на чем-то универсальном вроде лиспа, (и не иметь проблем с параллельным исполнением -- вместо нитей и блокировок передача continuations и чистые функции без побочных эффектов), или эффективный императивный С-код. И переключаться между представлениями по ходу дела (набросали прототип, посмотрели под профилировщиком hotspot'ы, перевели только их в другой, более эффективный вид, а остальное оставили в универсальном виде).

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

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

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

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

цель - объединить первое и второе, получить эффективную трансляцию высокоуровневого, domain-specific языка в низкоуровневое, возможно платформо-зависимое представление

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

проект Harmony посмотрю, спасибо - вроде весьма близко к тому что надо

>а в чём цель перевести программу из одного языка/парадигмы в другую? Почему нельзя работать в одном языке целиком или "встраивать руками"?

возможность локальных оптимизаций, невозможных на текущем "языковом уровне"

>то есть, свести императивный алгоритм на Си к эквивалентной "функциональной" программе? или просто свести к каким-то базовым "императивным" операциям, по аналогии с "функциональными" комбинаторами (вроде Дейкстра ещё писал про ветвление, цикл, переходы/рекурсию?)

второе

>можно посмотреть "компилятор схемы за 90 минут" (из схемы в си) или MBase лисп (из паскаля/бейсика/DSL в лисп и из него в стековый .NET-байткод, JVM или регистровый)

не совсем то...хотя спасибо за напоминание, "схему за 90 минут" прочитаю

http://www.cambridge.org/uk/catalogue/catalogue.asp?isbn=0521314232

> цель - объединить первое и второе, получить эффективную трансляцию высокоуровневого, domain-specific языка в низкоуровневое, возможно платформо-зависимое представление

Посмотри на C--

Ещё интересная идея была реализована в Helium, там типизированная VM, с доказательством тождественности всех шагов преобразования от Haskell к VM.

>как пример - задача развёртывания циклов в C++ посредством шаблонног

http://lush.sourceforge.net/lush-manual/47ae76ea.html#6 -- описание CLush, компилируемого лиспа.

Lush правда, не CL ни разу, больше на встраиваемый PicoLisp похож: Lisp интерпретатор с возможностью подключения отдельных методов скомпилированных на Си. Или лиспе.

One of Lush's most interesting features is its Lisp-to-C compiler and the ability to freely intermix Lisp and C code in a single function. Unlike many other interpreted/compiled languages , and contrary to many well established principles of language design , the two dialects that the Lush interpreter and the Lush compiler implement are two very different languages , though they share the same syntax. The compiled dialect is strongly typed , lexically bound , and has no garbage collector , while the interpreted dialect has loose typing , is dynamically bound , and is garbage collected.

In fact , the Lush compiler is not designed to replace the interpreter , but rather to complement it. <..>

sweeny.pdf: www.st.cs.uni-saarland.de/edu/seminare/2005/advanced-fp/docs/sweeny.pdf -- про то, как в Gears of War опасный С++ обернули Хаскеллем и получили что-то вроде контрактов на систему типов.

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

Меня это тоже интересует, но в обратном варианте: пишем на чем-то похожем на С, а некоторые куски транслируем в continuations (как это по русски? континуации?) чтобы потом можно быть распараллеливать.

"продолжения"? в теории множеств/алгебра, классы и поля вроде есть термин
closure -- замыкание, continuation -- продолжение

> возможность локальных оптимизаций, невозможных на текущем "языковом уровне"

нечто вроде LTO в gcc, оптимизации на уровне "всей" программы?
а то "локальные opt." смахивают на предварительную оптимизацию, которая is a root of all evil.

>нечто вроде LTO в gcc, оптимизации на уровне "всей" программы? а то "локальные opt." смахивают на предварительную оптимизацию, которая is a root of all evil.

вроде матричных вычислений в Blitz++. не преждевременная оптимизация, а декларативное описание локальных оптимизаций, известных для данной предметной области. отказ от преждевременно пессимизации, если хочешь :)

то есть - да, на уровне всей программы, но для каждого конкретного случая. как GHC RULES Pragma для Haskell: встретили паттерн - соптимизировали по наиболее подходящему правилу

>Ещё интересная идея была реализована в Helium, там типизированная VM, с доказательством тождественности всех шагов преобразования от Haskell к VM.

Спасибо, интересно.

Ещё было (есть?) нечто под названием HLVM:

http://lambda-the-ultimate.org/node/1562
http://www.coyotos.org/pipermail/bitc-dev/2006-August/000759.html

сайт http://hlvm.org не работает, но какой-то код есть в SVN LLVM:
http://llvm.org/svn/llvm-project/hlvm/trunk/

интересно, что в итоге случилось с проектом, бобик сдох?

мда, кое-кто "ниасилил" s-выражения:
http://nekovm.org/doc/nxml

http://en.wikipedia.org/wiki/Type_classes
http://www.coyotos.org/pipermail/bitc-dev/2008-November/001299.html