Какашки в Common Lisp

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

Функции - элементы, макросы - множества. Функции - люди, макросы - страны. Плохая аналогия :)

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

Даже в лиспе есть type-of который имеет в качестве значения type expression.

Если определять язык как индуктивный тип = Expression (тип-сумма по типам-произведениям), то любой конкретный АСТ (объект) будет иметь тип Expression, любые формы (стрелки) с помощью которых можно конструировать ACT будут иметь вид (_ -> Expression), т.е. это будет выглядеть как диаграмма из разных типов к Expression. В самом простом Тьюринг-полном языке (безтиповое лямбда-исчисление):

  Symbol * Expr
       |
      Lam
       |
       v
      Expr <--Var-- Symbol
       ^
       |
      App
       |
  Expr * Expr

или

      Expr
       |
      Lam
       |
       v
      Expr <--Var-- Nat
       ^
       |
      App
       |
  Expr * Expr

любые функции имеют тип Expression -> Expression (т.е. AST -> AST, или ([Symbol], AST) -> AST в другом предсталении). В этом смысле (типа) между функциями и макросами нет разницы - наличие макросов продиктовано только стратегией вычисления. Значения и типы - отдельно (это язык и его система типов), функции рантайма и функции компайл-тайма (макросы) - отдельно (это про стратегию редукций, про фазы). Безусловно, удобно разделить фазы, а смешивать нехорошо, но если из рантайма нет интерфейса к компилятору (и наоборот), то это тоже нехорошо.

Первые - существуют только в компайлтайме и их нету при запуске программы.

Как это нет, а type-of? А предикаты типов? А тайп-теги у объектов в куче и на стеке?

Вторых - не существует до того, как программа будет запущена.

Т.е. в написанной программе нет значений? Вроде (let ((a ...)) ...), или в том смысле что они не аллоцированны? Вообще-то до того как программа написана/скомпилирована вообще кроме идей ничего нет. А когда она скомпилирована значения уже есть в сегмента данных.

(if (integer? x) (...) (...)) знаем, что в первой ветке х - integer, во второй - соответственно он integer быть не может.

А чем может? Чем угодно? Дополнение до чего - до универсума (множество всех множеств, ага :))? Тем самым происходит апелляция к универсальному типу U, т.е. integer или вообще что угодно - дедуктвные типы в крайней степени.

(if (< (length x) 10) (...) (...)) соответственно в первой ветке х имеет тип списка с количеством элементов < 10, во второй - дополнение к этому типу.

Зависимые дедуктивные типы в крайней степени :)

А ещё (let ((a 1)) (set! a «hi!»)) - можно конечно вывести (Either Integer String).

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

Системы типов это больше про индуктивные типы - в таких системах дедуктивные типы это нечто более высокоуровневое.

В хаскеле сейчас SystemF, более слабая чем исчисление конструкций система, она позволяет оперировать как конечными так и бесконечными гетерогенными структурами (если делать через GADTs а не через экзистенциальные типы). Конечные or-квантификации по типам это Either. Что касается всего остального что позволяет статике (типы в рантайме + типы у переменных) приблизится к динамике (типы только в рантайме), то это уже бесконечные типы данных, о которых мало что известно, в том числе где они вообще нужны.

Про Main в Haskell.

Haskell исходит из наблюдения о том, что хоть потоки данных в реальном мире индетерминированны (т.е. случайны, стохастичны, сложнопредстказуемы и т.п.) процессы которые ими управляют в современных машинах детерминистичны (у нас ведь не квантовые компьютеры, а индетерминированные программы противоречат тезису Чёрча-Россера). До этого были ML-и которые достаточно внимательно относились к хорошим типам (к well-typed свойству), но ничего не могли сказать про детерминистичность программ и не принимали во внимание это наблюдение. Потом была Miranda которая уже очень внимательно относилась к этому наблюдению, а именно - там все программы были детерминированны, а нормальных средств для индетерминированных вычислений вообще не было. Haskell как язык сформировался уже к концу 80-ых и началу 90-ых и он почти не отличался от Miranda, отличался только тем что был открытым, а не собственностью некой компании как Miranda. Например, в книжке Peyton Jones-а про реализацию компиляторов функциональных языков (1987-ого года издания) весь код детерминирован, а рядом с программами к книжке есть простой скрипт который превращает прогаммы на Haskell в программы на Miranda и наоборот. Вобщем тогда в Хаскеле не было IO но было очень много о том как писать хорошо-типизированные детерминированные программы. И хаскель был в глубокой... академической среде :)

Что-то изменилось только с появлением публикаций про монадические интерфейсы, state transform-еры и IO. (Launchbury [1993], Peyton Jones & Wadler [1993], Launchbury & Peyton Jones [1994]). Суть в том, что с помощью state transformer мы можем расщеплять вычисление на две части. В основном расщепляя детерминированное вычисление мы получаем два детерминированных вычисления. Но если ввести тип-примитив про «мы тут ничего не знаем, это всё идёт в VM», то state transformer от такого типа расщепляет детерминированное вычисление на детерминированное вычисление и вычисление которое уходит в VM, а там с ним происходит что угодно. Такой state transformer и есть IO a = ST VM a, так IO Int это индетерменированный поток чисел, если Flow a = IO (Maybe a), то Flow Int это нечёткий недетерминированный поток чисел, IO () (= ST VM () или как пишут в GHC - ST RealWorld# ()) читается просто - индетерминированность (о которой вообще ничего нельзя сказать). Так в хаскеле реализуется управление индетерминированными потоками данных с помощью детерменнированых программ. При этом в концепцию монадических интерфейсов укладывается и смешивание того и другого (lifting).

Сейчас это развитие продолжается в singularity и прототипах операционных систем на haskell-е («A Principled Approach to Operating System Construction in Haskell»). Есть несколько таких систем (все они основаны на halvm - порт GHC под Xen, в galois недавно вышел стабильный релиз - они тоже используют её для прототипирования ОС). Там делается следующее - так как большая часть машины (RAM, CPU, FPGA, GPU) детерминированна вся машина рассматривается как обычный ADT и может участвовать в чистом state transformere. При этом граница IO оказывается там где она должна быть - в интерфейсе к недетрменированному миру (mouse, keyboard, аудиокарта и т.п.). Т.е. вместо «мы тут ничего не знаем, это всё идёт в VM» там «мы тут ничего не знаем, это всё идёт в мир за пределами нашей детерминистичной машины». В таких системах уже нет unsafe* функций, а тот факт, что сужение ST на mouse, keyboard и тому подобное нельзя запустить (run) абсолютно естественный факт (о том что нельзя назвать непредсказуемое предсказуемым) - вместо этого эти потоки можно направлять, фильтровать - с помощью liftingа с ними можно что угодно делать в плане «чистых» вычислений вокруг «нечистых» данных.

Далее, в ОС на си любая функция си может быть программой (функция создания треда принимает функцию). В Inferno любая функция на limbo может быть программой. В лисп-ОСах тоже самое. В тех системах на хаскеле тоже самое - «программа» это суть запуск обычной родной функцию через forkIO. Т.е. в естесвенной ситуации тип программы это просто тип функции.

В текущей же архитектуре есть ОС на си которая не интересуется ничем кроме кода возврата. Haskell работает (как виртуальная ОС) поверх этой хост ОСи - рантайм должен что-то вернуть и можно вернуть этот код с помощью System.Exit, но в типологическом плане тип программы IO (). Это только отражает тот факт что хаскелю с его концепцией разделения дет. и индет. процессов абсолютно нечего сказать хост-оси (даже если бы та поинтересовалась) кроме как просто «индетерминированность» (что хост-ось бы устроило, так как ничего про детерминированность она не знает).

У нас в Racket такого бреда нет - вместо него няшные фазы.

В рэкете можно в макросе запустить рантайм (eval) или в рантайме, скажем, прочесть файл, разобрать его, скомпилировать и запустить получившуюся функцию?

> В рэкете можно в макросе запустить рантайм (eval) или в рантайме, скажем, прочесть файл, разобрать его, скомпилировать и запустить получившуюся функцию?

Можно, но все это будет происходить в конкретной фазе. Более того, если мы, например, произвели некоторое вычисление в 1 фазе («компайлтайм»), потом скомпилировали модуль с этим вычислением (соответственно вычисление будет произведено во время компиляции), а потом сделали require в -1 фазу (т.о. первая фаза стала нулевой), то это вычисление опять будет произведено при запуске программы (мы его как бы перенесли из рантайма в компайлтайм, а значит оно должно выполниться именно там), а вот если делать require в ту же фазу - не будет (оно остается в фазе компайлтайма, которой во время исполнения программы не существует).

> что «значение» это объект (в смысле теории категорий), а «тип» это стрелка (в том же смысле)

Это херня какая-то. Типы - объекты, функции (не типы функций, типы функций - это тоже объекты, а конкретные функции - стрелки). То есть обратно - стрелки это значения (т.к. функция является именно значением), а объекты - это типы.

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

Нет, нельзя. Не надо путать тип и метаинформацию о типе, которая приклеена к значению.

тогда стрелки будут «классами» (как в haskell) т.е. типами типов.

«классы» - это функторы. Точнее недофункторы, чтобы класс стал функтором надо добавить к нему операцию fmap.

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

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

А чем может? Чем угодно?

скажем так, вместо «он не может иметь тип integer» следует лучше сказать, что он имеет тип (not integer). В такой системе первичны именно предикаты. Каждый предикат - тип, соответственно и отрицание предиката - тоже тип. Теоретико-множественная семантика не нужна :) В данном случае «тип» - это не множество значений, а некоторый набор свойств, которым характеризуется объект (и этот набор представляется совокупностью предикатов, которым объект удовлетворяет).

Зависимые дедуктивные типы в крайней степени :)

Ага. Но это единственная адекватная система типов. Вот кстати, то же Typed Racket изначально было спец. тулзой, которая примерно это и делала - занималась выводом типов выражений при помощи data-flow анализа, чтобы элиминировать чеки операций на тип аргумента. Конечно (< n 10) оно не делало - все ограничивалось «стандартными» типами + мелкие фичи вроде доказательства непустоты списка (тогда можно эиминировать проверку на пустой список в cdr) и т.п.

В хаскеле сейчас SystemF

Ну хаскель - вообще примитивное говно. Список произвольной вложенности оно хоть умеет типизировать? :)

Зачем множить сущности и придумывать какие-то «потоки», «детерменированности», «недетерменированности»?

Это херня какая-то.

Да, ты считаешь что вся теория индуктивных типов на основе теории категорий это херня :)

Типы - объекты

Всё что угодно может быть объектом, если это имеет смысл. Тип объекта это всегда стрелка (тип константы это стрелка (1 -> _)), объект с его стрелкой-типом это отношение типизации.

Так в мире значений (U = 1,2,3,...; знаки; строки; ...; функции; и т.п.) значения - объекты, их типы - стрелки, которые объекты уже в мире типов (U' = 1 -> Integers, 1 -> Characters, 1 -> String (или более сложно - индуктивно); A (/= 1) -> B (функции); и т.п.), их классы - стрелки, которые объекты в мире классов (U" = Functor, Applicative, Monad, Arrow - не расписываю чтобы не тратить место, мы просто собираем объекты из U', также как в U' собирали объекты из U).

Но понятно конечно, что аксиоматика на которую я ссылаю (то есть «тип это - ...» и так далее) «немного» не совпадает с той на которую ссылаешься ты. Кстати, что на эту тему есть на почитать? А то тут у категорщиков целая секта - даже в квантовую теорию поля залезли :)

Нет, нельзя. Не надо путать тип и метаинформацию о типе, которая приклеена к значению.

А не надо ожидать того к чему привыкли - в статике у переменной приписанный тип это «тип навсегда». Так что нет разницы. Опять же, всё не так как в той схеме которая тебе ближе.

«классы» - это функторы. Точнее недофункторы, чтобы класс стал функтором надо добавить к нему операцию fmap.

Я чего-то фундаментального не знаю, не иначе :) Это утверждение выглядит прямо как трансляция с марса. Можно подробнее?

Наличие макросов продиктовано их семантикой. Которая _ничего_ общего с семантикой функции не имеет.

Функций достаточно (как 640 килобайт :)).

(not integer)

Ну так конкретно - что это. А то такая система типов это как наивная теория множеств.

Список произвольной вложенности оно хоть умеет типизировать? :)

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

Зачем множить сущности и придумывать какие-то «потоки», «детерменированности», «недетерменированности»?

Писать PhD тезисы -> получать гранты -> заниматься их попилом :)

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

Так в мире значений (U = 1,2,3,...; знаки; строки; ...; функции; и т.п.) значения - объекты, их типы - стрелки

Функция как объект и её стрелка как объект той же категории это в смысле CCC.

> Да, ты считаешь что вся теория индуктивных типов на основе теории категорий это херня :)

Нет, конкретно твоя попытка построить категорию так, как ты ее строишь - херня.

(тип константы это стрелка (1 -> _))

Тебя не смущает этот костыль в виде черточки? Я уж не говорю о том, что если у тебя типы - стрелки, то как быть с тем фактом, что, вообще говоря, тот же Integer - это КУЧА стрелок? То есть 1 -> _, 2 -> _, 3 -> _ - это все разные типы, как ты собираешься делать Integer из них?

Кстати, что на эту тему есть на почитать?

«Сategories for working matematician» а дальше - публикации в интересующей тебя области.

Я чего-то фундаментального не знаю, не иначе :) Это утверждение выглядит прямо как трансляция с марса. Можно подробнее?

Рассмотрим на примере тайпкласса List. У нас объекты - типы, стрелки - функции. С точки зрения теорката функтор - это такая штука, которая отображает объекты/стрелки одной категории в объекты/стрелки другой (в частном случае, которым и является наш, «другая» категория может быть той же самой). + это отображение должно удовлетворять определенным свойствам, которые общеизвестны :) Теперь переводим на язык нашей категории. Значит, функтор - отображение, которое каждому типу ставит в соответствие некоторый другой тип, а функции - некоторую другую функцию. Рассмотрим List. Сам этот тайпкласс - это отображение, которое типу ставит тип. Действительно, типу А он ставит в соответствие тип списка с элементами типа А. Теперь ф-я fmap ( = map для List) - у нее тип (a -> b) -> [a] -> [b], то есть она каждой ф-и ставит в соответствие некоторую ф-ю. объединяя List с fmap мы в совокупности получаем нужное нам отображение целиком. Осталось только проверить, удовлетворяет ли оно общеизвестным свойствам - а это уже гарантируется условиями, накладываемыми на ф-ю fmap. Т.о. мы получаем функтор List. Теперь можно делать другие интересные вещи, как-то. Добавим ко всему этому делу полиморфную функцию return x = [x] (кстати, полиморфная функция в теоркате - это естественное преобразование. Действительно, естественное преобразование ставит в соответствие каждому объекту некоторую стрелку, то есть каждому типу - функцию, на нашем языке. А полиморфная функция это и делает - подставляя некоторый тип в полиморфную функцию, мы получаем функцию обычную.). Теперь у нас есть выбор - либо можно доавить полиморфную ф-ю Join - и мы сделаем наш функтор монадой, либо добавить <*> - и мы сделаем наш функтор аппликативным (да, аппликативный функтор - полностью аналогичная по сложности и абстракции монаде конструкция. Но почему-то туториалы про них не пишут :))

Функций достаточно

Иногда хочется излишеств.

Ну так конкретно - что это.

Это тип (not integer). Я же говорю тут тип - не множество, а предикат. Естественно, большинству таких типов можно поставить в соответствие множества, но некоторым - нельзя, и тут нет ничего такого. То есть (not integer) - это просто тип, совокупность значений которого (возможно) множеством не является. Никаких противоречий. Вот кстати можно заглянуть в соседний тред про «тип = интерфейс», там тип опять же не некое множество, а набор операций, которые можно производить с объектами. Быть множеством ему не требуется.

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

Можно определение такого типа? Пусть только элементы не произвольные, а конкретного типа, то есть что-то типа RecList a. Например [1, [[2]], [3, 4, 5]] - RecList Integer.

> Но вообще, затем же, зачем отделять фазы трансляции в Racket - чтобы отделить мух от котлет.

Нет, просто, по-моему, ИО можно придать семантику безо всяких «недетерменированностей». Как-то эти «недетерменированности» отдают кухонной философией, на мой взгляд.

императивный язык может в том же самом смысле быть «сам по себе макроязык» — компилятору достаточно доказать, что *данные* преобразования не изменяют результата выполнения *данной* императивной программы, и дальше вперед ровно как на хаскеле

>> типы соответствуют произвольном предикатам языка и единственная информация компилятору о типе переменной - это в какой ветке вычислений эта переменная стоит

Эээ... это что-то похожее на dependent types?

он скорее про это:

The key feature of occurrence typing is the ability of the type system to assign distinct types to distinct occurrences of a variable based on control flow criteria. You can think of it as a generalization of the way pattern matching on algebraic datatypes works.

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

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

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

допустим, у нас есть класс

class BankAccount {
  public:
    BankAccount( password ) { 
      this->amount=0;
      this->password=password; 
    }
    // тот, кто знает пароль от аккаунта, может снять деньги с этого аккаунта
    // и послать их на другой аккаунт
    send_to(receiver, sum, password) {
      if( password != this->password ) 
        return false;
      if( sum > amount ) 
        return false;
      amount-=sum;
      receiver.receive(sum);
      return true;
    }
    receive(sum, password) {
      if( password == "пароль отделения банка, принимающего наличку" )  
        receive(sum);
    }
  private:
    password="";
    amount=0;    
    receive(sum) {
      amount+=sum;
    }
};

как компилятору догадаться, что в обоих случаях sum должна быть неотрицательной? ведь по операциям над ней этого *не скажешь*

я уж не говорю про то, что sum должна быть точным десятичным числом с например четырьмя знаками после запятой

и кстати — ведь декларация private это тоже предикат? как ты думаешь компилятор должен его выводить, а?

возможно, однако, что чем меньше ручных деклараций предикатов ( = ручных аннотаций типа ) — тем лучше; если интересно обсудить возникающие проблемы — стучись ко мне в жаббер (в профиле)

З.Ы. кстати ты пробовал ту схему? http://lambda-the-ultimate.org/node/2622

> Ну (cons 1 (lambda ...))

Если речь про хацкель, то я так понимаю, что имеется в виду enumFrom 1 вычисленный до WHNF, которая в данном случае равна (1 : enumFrom 2).

В данном случае ф-я - это значение, ее дальше вызывать не надо.

Почему не надо? А если после f = [1..] мы где-нибудь в main напишем print f?

Все равно не понимаю, что конкретно имеется в виду в фразе:

Так ведь кроме main мы можем в компайлтайме вообще выполнить все не-ИО функции.

Ну да и фиг с ней, забей.

> императивный язык может в том же самом смысле быть «сам по себе макроязык» — компилятору достаточно доказать, что *данные* преобразования не изменяют результата выполнения *данной* императивной программы, и дальше вперед ровно как на хаскеле

Императивный язык в данном случае ничем не будет отличаться от функционального, т.к. все императивные конструкции будут только внутри ИО.

> наивно думать, что так можно избавиться от ручных деклараций предикатов ( = ручных аннотаций типа )

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

и кстати — ведь декларация private это тоже предикат? как ты думаешь компилятор должен его выводить, а?

Компилятор предикаты не выводит, он смотрит на те, которые прямо наличествуют в коде.

З.Ы. кстати ты пробовал ту схему? http://lambda-the-ultimate.org/node/2622

Ага. Она на уровне прототипа - просто для обкатки тех или иных фич. Я уверен, там глобально дизайн еще меняться будет.

> Ну, предположим, добавили эти expression-oriented и AST-макросы, что получаем в итоге? НедоЛисп? так почему бы сразу лисп не использовать?

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

> Вроде как у CL программистов в среднем квалификация выше.

Не «квалификация» выше, а ЧСВ и небыдлость. Вплоть до полной нирваны от осознания собственной небыдлости. Квалификация же обратно пропорциональна небыдлости, и это закон.

Ага и за эти 10 лет понять, что С++ никакого отношения к ООП не имеет ;)

Отношение к ООП имеет даже ассемблер. Так что гуляй, кури.

> Назовите 5 существенных отличий бзд от линукса для обычной программы?

Нет клевенького /proc, а есть какое-то унылое говно.

> Ну, когда Страус создавал свой C++, никакого ООП и не было. Он появился в начале 90-х стараниями маректологов. Так что Страус несовременен.

А Симула мне приснилась? Smalltalk под веществами привидился?

WTF, во что тред превратили? :) Чо-то парсер сломался на последней странице.

> и кстати — ведь декларация private это тоже предикат? как ты думаешь компилятор должен его выводить, а?

Если это и предикат, то к типу он точно не относится.

Но, наверное, все предикаты компилятор вывести не сможет.

> и кстати — ведь декларация private это тоже предикат?

Это, строго говоря, qualifier.

как ты думаешь компилятор должен его выводить, а?

Он его форсить должен. Чтоб неповадно было.

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

Если это и предикат, то к типу он точно не относится.

в моем понимании относится (и думаю в понимании страуструпа тоже)

рассмотрим класс

class CC {
  public: 
    CC(): value(1) {}
    CC* inc2(int n) { return this->inc1(n)->inc1(n); }
    int get() { return value; }
  private:
    CC* inc1(int n) { value*=n; return this; }
    int value;
};

сейчас get может возвращать только точные квадраты, а если inc1 вытащить в публичную часть (и получить класс С) — то все целые числа; так что С и СС это разные типы (С это класс всех целых чисел, СС это класс квадратов — для СС например *всегда* определена операция извлечения квадратного корня, дающая целое)

инкапсуляция для поддержания инвариантов — это общее место (про которое где-то в инете писал страуструп), соответственно отсюда вылезает простое как репа определение «тип это предикат»

>> Если это и предикат, то к типу он точно не относится.

в моем понимании относится (и думаю в понимании страуструпа тоже)

Серьезно?

class foo { int a; }

struct bar { int b; }

И что, по твоему и Страуструпа мнению, a и b имеют разные типы?

Ты сам с корчевателем спелся, никто за язык не тянул :)

Дядь, ты случайно тайпклассы с полиморфными типами не путаешь?

А кто такой «корчеватель»?

Ну что изначально такое корчеватель, легко ищется в инете.

А в текущем контексте как-то одно из твоих воплощений http://www.linux.org.ru/jump-message.jsp?msgid=5034750&cid=5066370 так назвало quasimoto, мне очень приглянулось.

:))

>А кто такой «корчеватель»?

http://www.linux.org.ru/forum/talks/3797897

P.S. Ппц, вы тут наговорили. :) Придание парадигмам излишней «научности» — злоЪ (и скукота по совместительству). :)

они и по твоему устаревшему классическому определению имеют разные типы, т.к. в bar можно че-то записать, а потом прочитать, а вот с foo ничего такого невозможно

твой вопрос видимо равноценен вопросу:

имеют ли разные типы

1. class foo { };

2. struct bar { int b; }

> твой вопрос видимо равноценен вопросу:

Нет. Я же вроде прямо спросил о полях a и b.

а я прямо ответил;

в дополнение к этому я имел в виду, что

class foo { int a; };

и

class foo { };

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

а вот некоторые программы, компилировавшиеся и работавшие с твоим bar, откажутся работать (и даже компилироваться) с foo

З.Ы. ты о таких очевидных вещах спрашивешь, что я уж опасаться начал, а нет ли тут подвоха

> наши самолёты как летали лучше ихних так и летают

Будте добры, расскажите, какой самолет летает лучше F-22?

Ну, тайпкласс - это полимофрный тип с добавкой, нет?

> с самого начала 80-ых пошло резко сокращение финансирования и сворачивания большинства исследовательских программ - в стране тупо кончились деньги.

Потому что цены на нефть резко упали как раз в начале 80-х.

И по поводу ракет: подскажите, сколько КА Советский Союз/Россия запустили хотя бы дальше орбиты Марса?

Будте добры, расскажите, какой самолет летает лучше F-22?

да много какой, Вы не представляете что декларируется для самолёта 5-го поколения, зачем тогда спорить ввязываетсь?

И по поводу ракет: подскажите, сколько КА Советский Союз/Россия запустили хотя бы дальше орбиты Марса?

в эту игру можно играть вдвоём: сколько космических орбитальных станций было создано и запущено США? :)

//давайте с оффтопом в другую ветку

> а я прямо ответил;

Твой ответ сильно удивил бы страуструпа.

>>> наши самолёты как летали лучше ихних так и летают

Будте добры, расскажите, какой самолет летает лучше F-22?

да много какой

Слив защитан? Или все-таки назовете, какой конкретно «наш самолет летает лучше ихних»?

>> И по поводу ракет: подскажите, сколько КА Советский Союз/Россия запустили хотя бы дальше орбиты Марса?

в эту игру можно играть вдвоём: сколько космических орбитальных станций было создано и запущено США? :)

Полторы: Skylab и половина (± немного) ISS.

Так сколько КА дальше Марса?

> сколько космических орбитальных станций было создано

и запущено США? :)

Да нах мы их вообще запускали?

Давайте по другому, я не знаю как на данный момент, но 5 лет назад у американцев было 400 спутников, а у нас 100. При этом, один американский идёт за 5 наших. А может и больше. Для примера: на геостационарных спутниках связи при схожей массе и мощности батарей на наши ставили 2 ретранслятора, а американцы ставили 15. При этом, стандартный САС для буржуйский спутников уже давно 15 лет. А наши начали делать такие только несколько лет назад (и неизвестно, до летает ли кто-нибудь эти самые 15 лет). До этого запускали хорошо если на 5 лет. А большинство советских спутников имели САС меньше 3 лет. При этом, хоть какую-то телеметрию (по которой хрен что разберёшь) стали снимать только в этом веке, а буржуины снимают и анализируют все подробности.

Я видел образцы солнечных батарей, которые вернули с «Мира». Вернули потому, что там была потеря мощности до 80% и хотели понять в чём дело (только эти образцы потом много лет никому не показывали, держали в сейфе, наверное стыдно было). Мля, кто их делал как будто вообще не понимал куда летит, как будто и не было десятилетий освоения космоса: толстенные стёлка (нахрена? на высоке 400 км то), а между ними всё залито каким-то (бытовым?) лаком, который в вакууме активно испаряется и тут же оседает на те самые стёлка.

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

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

Нет, конкретно твоя попытка построить категорию так, как ты ее строишь - херня.

Да, действительно - ерунда получилась. Но вот тут картинки правильные - типы как объекты и значения как стрелки (константы как стрелки 1 -> _, где 1 это терминальный объект категории). Но тогда непонятно что такое классы тиипов - ранее было сказано, что класс это недофунктор без fmap. Как это понимитиь? Например, с чего классу Arrow быть недофунктором без fmap или какому-нибудь произвольному классу с произвольными методами (который штук десять, например) быть недофунктор без fmap?

Но почему-то туториалы про них не пишут :))

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

«Сategories for working matematician» а дальше - публикации в интересующей тебя области.

Я имел ввиду не про вообще, а конкретно по этой концепции типов как предикатов, отслеживания предикатов в data-flow и т.п.

Рассмотрим на примере тайпкласса List.

А что это за тайпкласс?

Можно определение такого типа?

{-# LANGUAGE GADTs, TypeOperators #-}

data a :| b = L a | R b

infixr 5 :>

data List a where
  E    :: List a
  (:>) :: a :| List a -> List a -> List a

любой список будет иметь тип List a, где а это тип атомов списка. (:|) это or-квантификатор для типов (то же самое что Either из Prelude). Если нужно не накладывать никаких ограничений, то просто не or-квантифицировать, а forall-квантифицировать:

{-# LANGUAGE GADTs #-}

infixr 5 :>

data List where
  E    :: List
  (:>) :: a -> List -> List -- в GADTs forall по-умолчанию.

тогда любой список будет иметь тип List. Или даже так:

{-# LANGUAGE GADTs #-}

infixr 5 :>

data List where
  E    :: List
  (:>) :: a -> b -> List

Это уже как лисповые конс-ы, можно ими представлять ещё и графы.

Если делать с помощью обычных типов, то:

data Nil      = Nil
data Cons a b = Cons a b

class List l
instance List Nil
instance List b => List (Cons a b)

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

> наши самолёты как летали лучше ихних так и летают

А, да, вот еще: я не уверен, входит ли это в понятие «летать лучше», но рекорды SR-71 так до сих пор и не побиты. :-P

> Но вот тут картинки правильные - типы как объекты и значения как стрелки

У тебя из терминального объекта может быть только одна стрелка в каждый тип => одна единственная константа каждого типа. Алсо, у тебя каждой ф-и будет соответствовать пара стрелок - собственно, стрелка A -> B и стрелка из терминального объекта в этот функциональный тип. Какую выбирать?

ранее было сказано, что класс это недофунктор без fmap. Как это понимитиь?

Там чуть выше верно заметили - имелись в виду типы с кондом * -> *, а не тайпклассы :)

Ну почему, в typeclassopedia всё есть

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

любой список будет иметь тип List a, где а это тип атомов списка. (:|) это or-квантификатор для типов (то же самое что Either из Prelude). Если нужно не накладывать никаких ограничений, то просто не or-квантифицировать, а forall-квантифицировать:

То есть если я теперь напишу x = [1,[[[2]]],[3,4],5], то мне х правилньо протипизирует?

> А, да, вот еще: я не уверен, входит ли это в понятие «летать лучше», но рекорды SR-71 так до сих пор и не побиты. :-P

Рекордный самолет, чо. Как разведчик, правда, почти полный фейл.

>> А, да, вот еще: я не уверен, входит ли это в понятие «летать лучше», но рекорды SR-71 так до сих пор и не побиты. :-P

Рекордный самолет, чо. Как разведчик, правда, почти полный фейл.

Ну это смотря по каким критериям оценивать.

У тебя из терминального объекта может быть только одна стрелка в каждый тип => одна единственная константа каждого типа.

Да, индуктивный тип (а нам, в теории, вообще не нужны примитивные типы - достаточно индуктивных) как сумма по произведениям других типов, в смысле начальной алгебры у нас все константы (пустые конструкторы) индуктивного типа A это стрелки (1 -> A), все остальные конструкторы это стрелки (_ -> A), где чёрточка это не 1, а любые другие типы (в том числе сам A) и их произведения.

Алсо, у тебя каждой ф-и будет соответствовать пара стрелок - собственно, стрелка A -> B и стрелка из терминального объекта в этот функциональный тип. Какую выбирать?

А это уже нет, 1 -> A это константы, функции это только A -> B, без участия 1. Например, для data Nat = Zero | Succ Nat коммутативна диаграмма:

1 --zero--> N <-succ--- N
 \          |           |
  \         f           f
   \        |           |
    \       v           v
     с----> C <---h---- C

zero = inl
succ = inr
f    = join

Теперь, я надеюсь, всё правильно? :)

То есть если я теперь напишу x = [1,[[[2]]],[3,4],5], то мне х правилньо протипизирует?

Да. [a, b, c] это сахар для правоаасоциативного инфиксного оператора (:) - a : b : c : [], там я определил такой же оператор (:>). Чтобы прямо так писать <1,<<<2>>>,<3,4>,5> в хаскеле нужно чтобы был способ задавать новый вид скобок - этого нет в стандарте, но у GHCi есть препроцессор.