Homoiconic C

Ну, тип еще определяет результат операции. const все таки не тип, а модификатор типа, ЕМНИП;-)

Смотри, висит два тэга - int и double (я утрирую). Что с результатом то?;-)

Или еще хуже, int и str - как будем умножение производить?

Ну модификатор типа, один черт. Суть-то в том, что const int * и int * - это разные типы. Вот и у нас после введения этой системы появятся два разных типа функций.

Обсуждаем вундервафлю geekless? Тогда не ловит (ну или я не понимаю, каким образом ловит).

Что именно тебе не понятно? При объявлении указателя на функцию тебе придётся использовать nomalloc, если ты хочешь вызывать этот указатель из nomalloc-функции. А присвоить nomalloc-указателю можно только nomalloc-функцию.

Обсуждаем вундервафлю geekless? Тогда не ловит (ну или я не понимаю, каким образом ловит).

Ну чекер то рекурсивный. И он как бы понимает, что речь идет о вызове ф-ии (и он знает kmalloc).

В обсуждаемой вундервафле это будет как то так ИМНО выглядеть:

foo = kmalloc #тип выводится автоматом, про kmalloc мы знаем априори

Какую проблему(ы) ты хочешь решить, как она решается сейчас и чем тебя эти решения не устраивают?

Т.е. перед каждой сборкой сложной программы надо будет собрать её компилятор?

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

надо проверять не только тело функции, но и все функции, которые из неё вызываются

Для этого достаточно писать handler и kmalloc в разных монадах (или любых других подобных структурах), без возможности сделать lift из второй в первую. То есть достигать выполнения инвариантов не дедуктивно (написали нечто и насилуем это проверками), а индуктивно, то есть так, что сами вещи композицонно (согласно type rules) не смогут образовать expressions которые нам не нужны (содержат kmalloc в handler), по аналогии с тем как

template <typename T> struct List ...

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

Ну например - в хаскеле есть STM :: * -> * и IO :: * -> * и atomically :: STM a -> IO a - в монаде STM я не могу делать IO операций (точнее, могу, но это особая GHC-зависимая unsafe фича с которой нужна осторожность и за которой легко следить), могу только составить сложную транзакцию (любой чистый код, любое чтение/запись разных STM контейнеров) и кинуть её в IO. Ну и так же - я могу кинуть чистое значение в IO, но не могу вытащить обратно (опять же, без unsafe фич).

Поэтому все таки я про тип привык думать как про значение поля + возможно пачка модификаторов

Ну это от выбранной системы типов зависит. Для таких языков как C++, Java или вот эта вундервафля, это вполне справедливо.

Ну чекер то рекурсивный. И он как бы понимает, что речь идет о вызове ф-ии (и он знает kmalloc).

Если чекер рекурсивный, ему не нужен макрос.

Что именно тебе не понятно?

Зачем ты использовал макрос для обработчика прерывания.

Ну осталось синхронизивать наши понятия макроса, и выясниться что мы об одном и том же, но разными словами;-)

Я совершенно уверен, что не все присуствующие тебя поняли %)

Ну осталось синхронизивать наши понятия макроса, и выясниться что мы об одном и том же, но разными словами;-)

Мы с тобой вроде вообще не говорили о макросах. Еще раз: то, что предлагает geekless - это effect system, она реализуется без макросов.

Я, к сожалению, нихрена не понимаю в монадах, так что не смогу содержательно прокомментировать. Но сущностно мы имеем то же самое: nomalloc-выражение может состоять только из nomalloc-выражений; а «просто выражение» может состоять из «просто выражений» и nomalloc-выражений.

Насчёт насиловать проверками — главное, что результат-то достигается: мы придумываем разделение данных на типы, которые нам нужны, и можем объяснить транслятору эти типы так, чтобы «до него дошло». Хаскель точно так же будет выполнять проверки типов. В конечном счёте, на то статическая типизация и нужна.

Ну почему же... я не знаю хаскеля, а монады это шо то филофофское навроде? Но основную идею мне кажется я понял, и прмяо аж дух перехватило - «открылась бездна, байт полна», как то так... красиво;-)

Зачем ты использовал макрос для обработчика прерывания.

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

Макрос то можно куда угодно прикрутить, м.б. ему так больше нравиться...

Мне кажется, он под макросом понимает некоторую доп работу над кодом. То, что совсем настоящие программисты называют это эффект систем - ну так наука знает много гитик.

ЧТо то мне подсказывает, что в итоге в хацкеле реализуется это именно так, через насилование проверками, просто хацкелисты этого не видят.

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

Я правильно понимаю, что ты должен будешь с той же целью переопределить еще и макрос, объявляющий указатель на функцию?

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

Суть в том, для достижения этой конкретной цели тебе нужны не макросы.

Но основную идею мне кажется я понял,

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

и прмяо аж дух перехватило

Ты перед этим по лестнице не поднимался?

Макрос то можно куда угодно прикрутить, м.б. ему так больше нравиться...

Объясни, что такое макрос в твоем понимании.

Еще раз: то, что предлагает geekless - это effect system, она реализуется без макросов.

Это отлично, что я теперь знаю, как это называется, и могу это потом загуглить. Но, если я правильно понял, ты упускаешь, что я говорю про более широкую вещь. Речь идёт о метапрограммировании как таковом, а не только о частных проявлениях, таких как реализация системы для формального описания side-эффектов.

Не, ты мне скажи - переопределять макрос определения указателя на функцию надо или нет? %)

Если предположить, что он является отдельным символом, то надо.

Ты перед этим по лестнице не поднимался?

Я вообще лежу, страдаю, колено вчера на горных лыжах потянул;-(

Объясни, что такое макрос в твоем понимании.

Ну вот я для своей БД запилил «макросы». В выражении (запросе) можно юзать индентификаторы из некоторой таблицы. По индентификатору берется код из таблицы, вычисляется (при этом аналогично обрабатываются макросы во взятом коде), результат испольщуется вместо индентификатора. В общем похоже на вызов ф-ии, но без скобочек;-) Это макросы (или как это можно назвать)?

Есть ище макросы с параметрами, в С.

ИМНО макрос - это некоторое средство заменить один участок кода на другой участок кода. Вопрос в том, куда именно попадает замененный участок. В С-ях он идет в тот же исходный код. В обсуждаемой вундервафле - он может проваливаться на следующий уровень обработки, т.е. в исходный код не попадать, а влиять на формирование AST. Это существенная разница?

Если предположить, что он является отдельным символом, то надо.

А если не является, то как объявление и инициализация указателя на функцию учитывает атрибут nomalloc?

ИМНО макрос - это некоторое средство заменить один участок кода на другой участок кода.

Ок.

Это макросы (или как это можно назвать)?

С учетом того, что код хранится в БД, я бы назвал это ужасом на крыльях ночи %)

В обсуждаемой вундервафле - он может проваливаться на следующий уровень обработки, т.е. в исходный код не попадать, а влиять на формирование AST

В обсуждаемой вундервафле замена одного участка кода влияет на замену другого; это значит, что нужно менять процедуры-«заменятели» синхронно - например, введение nomalloc потребует замены макроса определения функции _и_ макроса определения указателя на функцию (и указателя на указатель %). В общем, геморрой. У www_linux_org_ru была другая идея - компилятор позволяет определять предикаты над данными и следит за их соблюдением.

А если не является, то как объявление и инициализация указателя на функцию учитывает атрибут nomalloc?

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

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

Ну это на тему того что называется phantom types в ML/Haskell и traits в C++. Например, «сделать trait в С++ для биндинга с контролем доступа только-чтение или чтение-и-запись в виде параметра типа, а не квалификатором const»:

namespace ref {

    // Вот тут даже лучше чем в ML/Haskell, потому что тип будет зависим от терма.
    enum access_t { r, rw };

    template <typename T, access_t a>
    class ref_t {};

    template <typename T>
    class ref_t<T, r> {
      protected:
        T x;
      public:
        explicit ref_t(T x_) : x(x_) {}
        T operator()() { return x; }
    };

    template <typename T>
    struct ref_t<T, rw> : ref_t<T, r> {
        explicit ref_t(T x_) : ref_t<T, r>(x_) {}
        void operator=(T x_) { ref_t<T, r>::x = x_; }
    };
}

int main()
{
    ref::ref_t<int, ref::r> x(2);
    // x = 3;

    ref::ref_t<int, ref::rw> y(3);
    y = 5;

    return x() + y();
}

на уровне системы типов разделили доступ, в рантайме - ничего нет (поэтому «фантомные» типы). Теперь представим, что ";", то что делает lexical bindings / shadowing и прочие вещи перегружаются, пишутся и нормально типизируются - мы можем constness / pure / referential transparency принять по умолчанию, а весь код с эффектами типизировать, например, как

io<int> main()
{

где перечисленные вещи - методы монады io. Или оставить как есть, но всё равно сделать

irq_handler_layer<irqreturn_t> handler(int irq, void *p);
mm_layer<void*> kmalloc(...);

и определить те вещи в монадах irq_handler_layer и mm_layer (или унаследовать их от абстрактной монады layer). Если нет функции mm_layer -> irq_handler_layer, то плохой код никак не напишется. Опять на уровне системы типов разделили слои выполнения - на рантайме это не должно (в идеале) отражаться.

Вообще, в хаскеле это часто практикуется - называется «монадический стек», код на разных уровнях не смешивается - чистый код, IO, STM, многочисленные монадические трансформеры (сюда ещё можно дописать уровень на котором все программы завершаются за конечное время, но это пока не реализовано именно в хаскеле).

http://web.cecs.pdx.edu/~apt/icfp05.pdf - тут аналогично вводится слой «hardware monad».

я изначально отвечал на вопрос, как это встроить, чтобы это работало. Если сделать некоторые предположения о этом нашем ЯП, то очевидные такие точки встраивания - макрос, который срабатывает при определении функции или указателя на функцию

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

С учетом того, что код хранится в БД, я бы назвал это ужасом на крыльях ночи %)

Код не хранится в БД, это не БД-шная таблица (там вообще таблиц нету, она нереляционная), таблица макросов хранится в конфиге и может менятся/дополнятся в процессе работы с БД юзером.

В обсуждаемой вундервафле замена одного участка кода влияет на замену другого; это значит, что нужно менять процедуры-«заменятели» синхронно - например, введение nomalloc потребует замены макроса определения функции _и_ макроса определения указателя на функцию (и указателя на указатель %).

ИМНО указатель можно не менять (с учетом рекурсивности), но да, некоторые проверки должны вводится синхронно в разных местах и это гемор.

У www_linux_org_ru была другая идея - компилятор позволяет определять предикаты над данными и следит за их соблюдением.

Ну все же все равно к проверкам сведется?

и вообще у тебя всё будет из макросов и точек втраивания, даже небо, даже аллах

Да. В рамках этого подхода, так и есть.

Shen

Спасибо, гляну.

ты таки напиши в лчику. ПРоэкт о генерации кода для числодробилок, на входе питон, на выходе плюсы.

У www_linux_org_ru была другая идея - компилятор позволяет определять предикаты над данными и следит за их соблюдением.

Ну все же все равно к проверкам сведется?

Там атрибуты вводятся и их совместимость задается формулами в исходном коде программы, а не кодируется руками для каждого нового атрибута.

Си с препроцессором, который сам был Си.

В си уже есть фопен и варианты на тему сканф и принтф, дерзай.

А что мешает сделать набор правил по проверке совместимости атрибутов расширяемым? Ну или ввести такие высокоинтеллектуальные общие правила, что бы новые атрибуты как то сами в них нужным образом вписывались и давали искомый эффект;-)

а не кодируется руками для каждого нового атрибута.

И что мешает реализовать систему формального описания этих предикатов в рамках метаязыка? Речь про malloc шла исключительно в виде примера а ля «и вот такое можно сделать тоже». Очевидно, что можно сделать не только частный случай, но и решение в общем виде.

И что мешает реализовать систему формального описания этих предикатов в рамках метаязыка?

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

Alv, это и тебе ответ %) Вы с geekless один человек?

синтаксис должен быть удобен и для человека.

покажи мне блин этот эталон_человека.

по факту человек пластичное животное.

а разнаобразие синтаксисов части следствие экономии усилий - зачем переучивать англоговорящего с его SVO(вроде) на что-то иное - проще бэйсик слепить.

чёт мне понравилось рекомнедовать эту статью http://goodarticles.narod.ru/mccarthy.html

пора её наверно на цитаты разбирать - обнаружить что в М-синтаксисе(случаи когда символ функции заранее известен ) синтезировать проще(ибо привычней ) чем в чистом S полезное наблюдение(само).

обнаружить что биекция (hd tl |lft rgt) тобиш просто наложение хоть какой то структуры на возможный не_атом есть реально МЫСЛЬ - а запись однородного набора в виде открывающий_разделитель ноль_либо_более_раз_элемент разделёные разделителем( по началу запятой ибо пробел удобен для именования символов именуемыми словосочетаниями_предложениями) закрывающий_разделитель - это по факту сиюминутный компромис ставший ритуалом. - замечательное

Это интересная техника, но, насколько я понимаю, это чистая инкапсуляция значений. Ок, изменять и создавать их может только соответствующий слой, но какая польза от этого в задаче «запретить вызов kmalloc из прерывания»?

не только и не столько .

чаще(в случае наступления прекраснного будущего с желаемым ТС языком) среда (эклипсы и прочии идеи) будет точнее давать информативный выбор человеку при синтезе кода.

т.е мечта синтаксически рулируемого формирования мысли наконецто станет реальностью.

покажи мне блин этот эталон_человека.

Эталона нет, есть статистика. Она не в пользу лиспа. Кроме того, есть здравый смысл, который подсказывает, что человеку приходится иметь дело чаще с линейными сущностями, а не с рекурсивными.

по факту человек пластичное животное.

И поэтому можно кормить его говном?

А к лиспу как к синтаксису у меня есть претензии, да. Вычисления строятся как _действие_, применяемое к _объектам_ (аргументам). Однако проблема в том, что человек не мыслит вложенными действиями. Человек чаще мыслит трансформациями объекта применением к нему нескольких действий. И поэтому оптимальный порядок записи аргументов не «действие аргумент1 аргумент2 аргумент3 ...», а «аргумент1 действие аргумент2 аргумент3». А потом к результату выражения применяется новое действие, и получаются цепочки: «аргумент1 действие аргумент2 аргумент3 действие2 аргумент4 действие3 аргумент5...».

Это именно тот способ, который наиболее естественнен человеку, прост для чтения и для записи. И именно это мы видим в Io. somelist select(greater(10)) reduce(+) — «из somelist выбрать все, что больше 10-ти и сложить».

При том, что это ровно те же самые рекурсивные списки, что и в лиспе, просто записанные по-человечески.

Си с препроцессором, который сам был Си.

В си уже есть фопен и варианты на тему сканф и принтф, дерзай.

Иногда лучше жевать.

ЧТо то мне подсказывает, что в итоге в хацкеле реализуется это именно так, через насилование проверками, просто хацкелисты этого не видят

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

Ну а различить два newtypa (типа IO и STM) это вообще не сложнее чем отличить Int от String (как типы, то есть ~ сравнение чисел-представлений на равенство).

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

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

какая польза от этого в задаче «запретить вызов kmalloc из прерывания»?

Вот:

nomalloc-выражение может состоять только из nomalloc-выражений; а «просто выражение» может состоять из «просто выражений» и nomalloc-выражений.

malloc работает в io, например:

malloc :: Size -> IO (Ptr CChar)

useMalloc :: Size -> IO ()
useMalloc bytes = do
  ptr <- malloc bytes
  write / read prt
  other io

если сделать производную обвёртку от IO:

-- IRQ <: IO
-- up-cast fromIRQ :: IRQ -> IO is safe
-- down-cast IRQ :: IO -> IRQ is unsafe
newtype IRQ a = IRQ { fromIRQ :: IO a } deriving ( Functor, Monad )

и _не_ экспортировать из соответствующего модуля конструктор IRQ :: IO a -> IRQ a, оставив только минимальный нужный интерфейс, то можно будет писать:

handler :: __ -> (__ -> IRQ some) -> IRQ IRQRetType
handler _ fn = do
  -- valid irq computations ...
  some <- fn __
  case some of
    _ -> return IRQ_HANDLED
    -- etc ...

но ни

foo = malloc

ни любое другое IO нельзя:

handler _ fn = do
  foo 100500 -- Couldn't match type `IO' with `IRQ'

вместо конструктора IRQ можно оставить unsafeIO2IRQ для желающих. Аналогично можно разбросать вычисления на большее количество уровней - IO :> Log только для логов, IO :> MM для памяти, IO :> Log :> IRQ (но не MM :> IRQ). Работает за счёт разных вещей - zero-cost newtype, возможность писать императивный код исключительно как монадические комбинаторы обеспечивающие некую форму последовательного выполнения и биндингов в IO, do-нотация, соответственно, rank-1 параметрический полиморфизм и соответствующие проверки типов, сокрытие имён в модулях.

система верификации типов будет написана на том же самом языке, который она верифицирует.

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

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

Ну если так... То есть, «лисп, только как си» :) Если есть core язык с набором примитивных специальных форм пригодный для трансляции в си + макросистема + любые библиотечные макросы реализующие произвольные специальные формы + кто-то должен рассказать почему макросистемы достаточно для того чтобы делать проверки и вывод для действительно богатых систем типов. Последнее обычно делается в трансляторе, иногда на самом хост-языке, для заведомо изученной системы типов. Например, http://lampwww.epfl.ch/~odersky/papers/mfcs06.pdf — и представим как это делать на макросах. Тут можно вспомнить yale haskell в котором было CL <- Scheme <- Haskell — работало же, чисто как транслятор.

Получится что-то вроде BitC/ACL2, наверно.

А на Си++ это не переводится?

В C++ всегда в слое IRQ можно будет найти безобидный тип T и населить его избегаемым эффектом, хотя бы someT : T => ([]() -> T { malloc(100); return someT; })() : T, так что нет. Точно так же наличие constness у operator+ не говорит что он pure (и про ассоциативность с коммутативностью тем более ничего не говорит).