Человеческое метапрограммирование

Во-первых, то, что ты определил - не подтипирование. Во-вторых, Num - не тип. Закончим на этом до тех пор, пока не ознакомишься с основной литературой по теме (хотя бы тот же тапл (чтобы знать основы), потом необходимую любому базу - дифтоп, алгебраическая геометрия, теория гомологий и теория пучков. потом (НЕ РАНЬШЕ!) можешь попытаться осилить Маклейна (категории для работающего математика)). Когда завершишь - возвращайся.

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

Там используется строка (String) для которой определено конкретное приведение к конкретному типу Data. То есть String -> Data, никаких Data -> к нужному типу.

сперва мы имеем НАБЛЮДАЕМЫЕ типы. Это нам дано.

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

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

TK это междисциплинарная штука, поэтому и результаты должны быть междисциплинарные. Например, оба результата Voevodsky (motivic cohomology и HoTT).

человек просто себе даже и представить не может, что что-то может быть НЕ ТАК КАК В ХАЦКИЛЕ

А где-то, представь себе, не так как в Racket.

Int - это не подтип «forall (a:: *) a»

Можно безопасно использовать элемент типа Int вместо элемента типа «forall (a:: *) a» и прочих перечисленных без каких-либо приведений? Можно.

хотя бы тот же тапл (чтобы знать основы), потом необходимую любому базу - дифтоп, алгебраическая геометрия, теория гомологий и теория пучков. потом (НЕ РАНЬШЕ!) можешь попытаться осилить Маклейна (категории для работающего математика)

Это такая игра в перечисление ряда random topics? Как-то не интересно.

Кем дано?

Откуда я знаю? Это неважно.

Машины и языки - не явления природы, это рукотворные вещи

И что?

В том числе я могу выбрать язык.

Ну да. А систему типов - выбрать не можешь. Она тебе дана. Если у тебя есть язык - то ты как не извернись, а система типов с ним уже будет вполне конкретная и определенная - естественно, под системой типов мы понимаем не ее модель (правила типизации), а реальную систему типов - то есть наблюдаемые типы значений термов.

TK это междисциплинарная штука

Неверно.

и результаты должны быть междисциплинарные.

А их нет. Ни междисциплинарных, ни каких-либо еще. Такая вот незадача :(

Можно безопасно использовать элемент типа Int вместо элемента типа «forall (a:: *) a» и прочих перечисленных без каких-либо приведений? Можно.

Нет, нельзя. Иди и почитай, что такое подтипирование уже. Хватит позориться. Домашнее задание тебе - сказать, почему f: (forall (a: Num) a) (forall (a: Num) a) -> (forall (a: Num) a), f = x + y, f 1 1.0 не чекнется (hint: если бы Int и Float были подтипами (forall (a: Num) a), то все бы прекрасно чекалось).

Это такая игра в перечисление ряда random topics?

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

А где-то, представь себе, не так как в Racket.

Я это прекрасно пониманию и именно по-этому не начинаю, например, при виде high-order-полиморфных типов вопить «это не имеет смысла! ведь в Racket это невыразимо!!1!» - и привести пример, в котором в Racket не чекается монадический код. Кстати, типы variable-arity полиморфных ф-й в Racket это вообще функция из множества натуральных чисел в множество типов. Здесь ты должен опять закричать «НИВАЗМОЖНА!! НИИМЕЕТ СМЫСЛА!!!! БРЕД НОНСЕНС! Я В ДОМИКЕ!».

И что?

А систему типов - выбрать не можешь. Она тебе дана.

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

Неверно.

А их нет. Ни междисциплинарных, ни каких-либо еще. Такая вот незадача :(

Что ты думаешь о двух упомянутых работах Воеводского? Там ТК используется именно как междисциплинарная связка (пусть и как чисто технический «гаджет»).

Иди и почитай, что такое подтипирование уже.

Ты сейчас сам ограничиваешь понятие подтипирования до того что описано в TAPL.

не чекнется

Конечно, (1 :: Int) + (1.1 :: Float) не чекнется. Ты говоришь в сигнатуре «хочу чтобы был тип-инстанс Num и чтобы он совпадал у обоих аргументов и у результата», но передаёшь разные типы. Если хочешь разные, делай разные:

f :: (Real a, Real b, Fractional c) => a -> b -> c
f x y = realToFrac x + realToFrac y

или

class Plus a b c | a b -> c where (+.) :: a -> b -> c
instance Plus Float Int Float where x +. y = x + fromIntegral y
-- ...

Нет, это необходимый нминимум, которым нужно владеть, чтобы не быть попугаем.

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

не начинаю, например, при виде high-order-полиморфных типов вопить «это не имеет смысла! ведь в Racket это невыразимо!!1!» - и привести пример, в котором в Racket не чекается монадический код

Вопить я не начинаю, я просто говорю своё «не нужно».

Кстати, типы variable-arity полиморфных ф-й в Racket это вообще функция из множества натуральных чисел в множество типов.

Это как раз ерунда (codes в agdе, то есть (A : Set) -> Set), так что тут я спокоен :)

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

Масло масленное. Если фиксирован язык, то фиксирована модель вычисления. Если фиксирована модель вычисления, то фиксирована система типов. Так что достаточно «выбрал язык». Все остальное будет дано.

Это как раз ерунда (codes в agdе, то есть (A : Set) -> Set), так что тут я спокоен :)

Так ведь типы «1» или «2» - это подмножество такого подхода. Если у тебя в агде кодируется variable-arity полиморфизм, то и это тоже кодируется.

Ты говоришь так, как будто тебе все три на голову свалились

Именно так все и происходит на практике. Когда ты уже это поймешь?

Я смотрю на все три как на предмет сознательного выбора, на предмет сознательной разработки именно в _соответствии_ с моделями.

Еще раз - твоя модель должна отражать реальнотсь. Сперва есть реальность - потом модель. Модель, которая не отражает реальность никому нахуй не нужна. Так работает наука. А подгонять реальность под модель - это религия, это не наука.

Что ты думаешь о двух упомянутых работах Воеводского? Там ТК используется именно как междисциплинарная связка (пусть и как чисто технический «гаджет»).

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

Ты сейчас сам ограничиваешь понятие подтипирования до того что описано в TAPL.

У понятий есть общепринятые определения. Если я гвоорю «подтипирование» - то это «подтипирование» в рамках общепринятого определения. Если ты полагаешь под «подтипированием» что-то другое - то тебе следует указывать на это и не использовать слово «подтипирование».

Да, кстати, определение «подтипирования» нам тоже _дано_. То есть сперва у нас появились системы типов с подтипированием и только потом это понятие было формализовазно. формализовано затем, чтобы инкапсулировать в себе сущность и особенности таких систем (виртуальный полиморфизм). Любое определение «подтипирования» которое не отражает эти «особенности» (то есть не формализует виртуальный полиморфизм) - не будет иметь смысла.

Ты говоришь в сигнатуре «хочу чтобы был тип-инстанс Num и чтобы он совпадал у обоих аргументов и у результата»

Нет, я такого не говорил. Я сказал «хочу чтобы был тайп-инстанс Num, свой для любого аргумента».

делай разные:

Ты не то сделал. Квантификация по типу долджна быть _внутри_, а не _снаружи_, Ты определил f как полиморфную ф-ю, которая будет обычной ф-й для каждой тройки типов. Задача же была сделать обычную моно-функцию, которая в качестве аргументов будет принимать произвольные инстансы Num.

Алгебраическая геометрия и теория гомологий - интересно, конечно, но не релевантно. Дифтоп - тем более.

Теория гомологий - это вообще the most relevant часть математики для теорката, т.к. теоркат - это изначально и есть инструмент для теории гомологий. Если ты не знаешь теории гомологий - ты не можешь знать теорката. топология и дифференциальная топология нужна затем, чтобы понимать теорию гомологий (не знаешь топологии - не знаешь теории гомологий, и не поймешь никогда, что такое гомологии и зачем они нужны и почему они такие, какие есть). А алгебраическая геометрия - затем, чтобы понимать теорию пучков (потому что пучки оттуда и пришли, так же как гомологии из топологии).

Вопить я не начинаю, я просто говорю своё «не нужно».

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

ТК, категорные логики, теория пучков - может быть.

Хорошо, кстати, что релеватность пучков для ТК хоть не оспаривается. Может, не все потеряно для пациента.

Масло масленное.

Заданием языка (заданием голого абстрактного синтаксиса = множества синтаксически корректных термов) задаётся также система типов? И вычислитель?

Так ведь типы «1» или «2» - это подмножество такого подхода.

Да, когда ты пишешь «1» на месте типа в сигнатуре ты на самом деле подразумеваешь некий 1_the_type : U(0), а когда пишешь «1» типа «1» на месте значения - некий (и единственный для этого типа) 1_the_term : 1_the_type. Дальше можно ввести f : 1_the_type -> Nat; f 1_the_term = 1, ввести коды c : Nat -> Set; c 1 = 1_the_type; ... В твоих примерах на Rackete нет ничего плохого. Просто ещё до того как их привести ты начал говорить про существование неких ? : 1_the_term, что не имеет смысла и по отношению к чему я говорил «не нужно». Если изначально подразумевалось, что 1 в сигнатуре это одно (множество {1}), в значениях - другое (элемент 1), тогда вопросов нет, это нормально.

Так работает наука.

Как ни странно, так работает _естественная_ наука.

А подгонять реальность под модель - это религия, это не наука.

А это любая инженерия, когда ты создаёшь («подгоняешь реальность под модель») что-либо по готовому проекту (чертежу, шаблону, модели, стандарту языка, ТЗ и т.д.).

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

Нет такого понятия «виртуальный полиморфизм». Если речь про разные формы subtype polymorphism, то чего именно не хватает в хаскеле, чтобы утверждать, что его нет и что он не настраивается?

хочу чтобы был тайп-инстанс Num, свой для любого аргумента

Это записывается не как (Num a => a) -> (Num a => a) -> (Num a => a) (так нельзя), а как (Num a, Num b, Num c) => a -> b -> c.

теоркат - это изначально и есть инструмент для теории гомологий. Если ты не знаешь теории гомологий - ты не можешь знать теорката

Я знаю эту историю. Но любой современный учебник ТК (Аводея, например, там как раз «Маклейн - математикам, а мы пишем для всех остальных») даёт ТК саму по себе, с примерами из тех областей в которых она применима, причём обычно примеры по-проще, потому что предполагается знакомство с ТК в том числе тех кто не специализируется и не будет (то есть не обязательно) специализироваться в перечисленных тобой областях. Считаешь, что это неправильно и бурбакизм, что ТК нужно изучать исключительно следуя по её генетической цепочке (почему-то вспомнился Ленг грузящий категориями с самого начала своей Алгебры, а про теорию Галуа рассказывающий где-то к середине)?

Заданием языка (заданием голого абстрактного синтаксиса = множества синтаксически корректных термов) задаётся также система типов? И вычислитель?

Я не знаю ни одного языка программирования, который бы задавался голым абстрактным синтаксисом, без вычислителя. А ты?

Просто ещё до того как их привести ты начал говорить про существование неких ? : 1_the_term, что не имеет смысла

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

Если изначально подразумевалось, что 1 в сигнатуре это одно (множество {1}), в значениях - другое (элемент 1)

По-моему, это было очевидно.

Нет такого понятия «виртуальный полиморфизм».

Конечно, есть - имеется ввиду тот самый полиморфизм из ООП.

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

Подтипов не хватает.

Это записывается не как (Num a => a) -> (Num a => a) -> (Num a => a) (так нельзя), а как (Num a, Num b, Num c) => a -> b -> c.

Еще раз - квантор должен быть ВНУТРИ, иначе это не подтипы. А если квантор внутри, то имя переменной уже не имеет значения, т.к. она локальная для квантора. То есть на вопрос «почему в хаскеле нет подтипов?» ответ именно такой - потому что в хаскеле нельзя (Num a => a) -> (Num a => a) -> (Num a => a)

Я знаю эту историю. Но любой современный учебник ТК (Аводея, например, там как раз «Маклейн - математикам, а мы пишем для всех остальных») даёт ТК саму по себе

Так же как и любой современный учебник по алгебре начинает с аксиом групп, вместо того, чтобы начать с групп преобразований, их приложений и _вывести_ соответствующие аксиомы. И это плохо, очень плохо, потмоу что в результате получается попугай, который запросто тебе эти аксиомы расскажет, но не ответит в чем их смысл и почему они такие, а не какие-либо другие. В худшем случае вообще определение группы дается как частный случай более базовых структур (магм, моноидов, полугрупп).

Считаешь, что это неправильно и бурбакизм, что ТК нужно изучать исключительно следуя по её генетической цепочке

Это верно не только для ТК - это верно для всего. Изучение алгебры/тк/гомологий/чего угодно без «генетической цепочки» - это как изучать устройство микроскопа без изучения задач, из которых это устройство следует. В результате изучавший подобным образом микроскоп человек будет колоть им орехи. А если его попросят такой микроскоп доработать - сделает из него молоток. Конечно, теоретически, все может быть и иначе - но это будет _вопреки_ подобной схеме изучения.

(почему-то вспомнился Ленг грузящий категориями с самого начала своей Алгебры, а про теорию Галуа рассказывающий где-то к середине)?

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

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

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

Я не знаю ни одного языка программирования, который бы задавался голым абстрактным синтаксисом, без вычислителя. А ты?

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

только что абзацем выше ты обосновал корректнотсь этого подхода, а теперь - «не имеет смысла».

Нет ничего странного в записи 1_the_term : 1_the_type или 1 \in {1} (в теории множеств) и в том чтобы позволить себе вольность обзывать элемент и соответствующий синглтон одним именем (если можно их различить исходя из контекста). Есть странность в принятии термов как типов чего-то ещё (не термов и не типов), то есть в ? : 1_the_term и в том чтобы отождествлять \in с отношением типизации. Например, в ZF у нас может быть 0 \in 1, но не может быть ? \in 0, если мы разрешим термам 0, 1, ... быть типами чему-то и отождествим \in с отношением типизации, то мы получим 0 как тип без термов (аналог _|_). Если у нас TT, то принято _начинать_ с термов и формул, задавая далее типы для термов и утверждений вместе с определением отношения типизации, раз мы начинаем с термов, то мы просто не можем использовать их как типы для чего-то другого - это не определено.

Подтипов не хватает.

Чем не подходит 2-параметричный класс (:>) инстансы которого задают иерархию подтипирования?

Конечно, есть - имеется ввиду тот самый полиморфизм из ООП.

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

Еще раз - квантор должен быть ВНУТРИ, иначе это не подтипы.

И что это даст? Оба ведут себя одинаково - принимают разные инстансы одного класса.

Метапрограммирование — это просто!

Если речь про ЯП, то всё так.

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

Есть странность в принятии термов как типов чего-то ещё (не термов и не типов)

Чего-то еще - это чего? Не понял что-то.

Чем не подходит 2-параметричный класс (:>) инстансы которого задают иерархию подтипирования?

Тем, что они не задают иерархию подтипирования. Сколько можно уже один и тот же вопрос задавать?

И что это даст? Оба ведут себя одинаково - принимают разные инстансы одного класса.

Они НЕ ведут себя одинаково. В случае сабтайпинга вообще типы одинаковые: type T = (Num a) => (forall a . a), f: T -> T -> T, f = x + y. Естественно, чтобы это работало, нам надо в рантайме уметь определять, какой конкретный подтип стоит на месте терма (Int или Float, например?).

Это сабтайп полиморфизм, оно может быть и просто про вызов не виртуальных методов предка на объектах классов потомков

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

Метапрограммирование с тайпчеком

fxd

Чего-то еще - это чего?

В том и дело, что ничего. Поэтому нельзя написать 5 foo(5 x); нигде начиная с си и далее. В Racket 5 на месте типа это совсем не терм 5, это другая вещь (отдельный тип с единственным элементом 5 эквивалентным элементу 5 множества целых чисел).

Тем, что они не задают иерархию подтипирования.

Задают, только не автоматически.

type T = (Num a) => (forall a . a), f: T -> T -> T, f = x + y

type T = Num a => a это Rank2Types, равно как и (Num a => a) в сигнатурах (тут я ошибся сказав что так нельзя). Но они не помогут делать рантайм диспетчеризацию, для этого нужны ExistentialQuantification с data или сразу GADTs:

{-# LANGUAGE Rank2Types, KindSignatures, GADTs, ConstraintKinds, FlexibleInstances, UndecidableInstances #-}

import GHC.Prim ( Constraint )

data Any :: (* -> Constraint) -> * where
  Any :: forall cls a. cls a => a -> Any cls

class (Show t, Fractional t) => ShowFractional t
instance (Show t, Fractional t) => ShowFractional t

type RealT = Any Real
type ShowFractionalT = Any ShowFractional

(+.) :: RealT -> RealT -> ShowFractionalT
Any x +. Any y = Any $ realToFrac x + realToFrac y

выбор типа тут происходит именно в рантайме.

В том и дело, что ничего. Поэтому нельзя написать 5 foo(5 x); нигде начиная с си и далее. В Racket 5 на месте типа это совсем не терм 5, это другая вещь (отдельный тип с единственным элементом 5 эквивалентным элементу 5 множества целых чисел).

Так чего ты вопил «нельзя не имеет смысла»?

Задают, только не автоматически.

Вообще никак не задают. Подтип - это если тип разрешается в рантайме.

type T = Num a => a это Rank2Types, равно как и (Num a => a) в сигнатурах (тут я ошибся сказав что так нельзя). Но они не помогут делать рантайм диспетчеризацию, для этого нужны ExistentialQuantification с data или сразу GADTs:

И опять ты сделал не то. У тебя Any Int и Any Real вместо Int и Real. Ну нету подтипов в хаскеле, сколько можно уже? Подтипирование - это вполне определенный формализм и система типов хаскеля этому формализму НЕ УДОВЛЕТВОРЯЕТ. Сколько примеров не приводи - а не удовлетворяет и все. И если вдруг тебе кажется, что какой-то пример это опровергает - ищи ошибку в примере.

(+.) :: RealT -> RealT -> ShowFractionalT
Any x +. Any y = Any $ realToFrac x + realToFrac y

Прекрасно. Теперь не переписывая эту функцию и ее тип определи какой-нибудь подтип RealT который можно будет передать в +.

Кстати:

http://hackage.haskell.org/trac/ghc/wiki/TypeNats

И вот:

http://hackage.haskell.org/trac/ghc/wiki/DeferErrorsToRuntime

так что безопасные объединения теперь можно и в хаскиле сделать - все ранво ошибки в рантайме чекаются :)

У тебя Any Int и Any Real вместо Int и Real

У меня Any _Real_ и Any _ShowFractional_, где Real и ShowFractional - классы. И сделано это исключительно чтобы инкапсулировать квантифицируемую переменную, как ты просил. Вместо GADTs + ConstraintKinds можно сделать просто с ExistentialQuantification:

data RealT = forall a. Real a => RealT a
data ShowFractionalT = forall a. (Show a, Fractional a) => ShowFractionalT

но это менее удобно.

Теперь не переписывая эту функцию и ее тип определи какой-нибудь подтип RealT который можно будет передать в +.

В (+.) уже можно передавать всё что угодно, достаточно написать этому инстанс Real и обернуть в Any.

http://hackage.haskell.org/trac/ghc/wiki/TypeNats

Там нет объединений, просто типы параметризированные числами, например, Vec : Nat -> Set -> Set и потом Vec 5 Int, то есть совсем не то что было в примерах с Racket. 5 как был термом, так и есть, тут ни он ни нечто вспомогательное не используется как тип. С пакетом type-level так можно делать, только вместо 5 будет D5, где D5 :: * и не имеет нормальных термов.

http://hackage.haskell.org/trac/ghc/wiki/DeferErrorsToRuntime

А это про расставление (достаточно полиморфного) error на месте плохого кода вместо генерации ошибок во время компиляции.

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

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

А есть генетически правильные учебники или популярная литература? Лучше на русском.

Вместо GADTs + ConstraintKinds можно сделать просто с ExistentialQuantification:

data RealT = forall a. Real a => RealT a

у тебя RealT a, а надо а...

В (+.) уже можно передавать всё что угодно, достаточно написать этому инстанс Real

И какое же это подтипирование? Подтипирование работает безо всяких инстансов, искаробки.

Там нет объединений

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

А это про расставление (достаточно полиморфного) error на месте плохого кода вместо генерации ошибок во время компиляции.

Ну правильный код же в том месте не дает эррора? Или я неверно понял?

А есть генетически правильные учебники или популярная литература?

Нет, не в курсе.

• Лекции и задачи по топологии. Вербицкий М.
• Теорема Абеля в задачах и решениях.
• Теоремы и задачи функционального анализа.

у тебя RealT a, а надо а...

Можно

type RealT = Real a => a

c Rank2Types, но оно в итоге не будет полностью работать как надо, потому что type это просто compile-time синоним (нельзя сделать инстансов таким типам, будут жёсткие (rigid) переменные типов и невыводимость конкретных a ~ Float и т.п. из контекста Real a), а data, вместе с конструктором RealT, добавляет объектам runtime различимость (тэг), так что можно делать позднюю диспетчеризацию.

Подтипирование работает безо всяких инстансов, искаробки.

Ну ладно. Тогда в си нет ООП потому что нет наследования искоробки и нужно возиться с агрегацией и ручным составлением интерфейсных структур с функциями для структур с данными.

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

Там нет термов в качестве типов. Natural number literals are a family of types, all of which belong to the kind Nat. То есть each natural number literal is an empty type. То есть 5 как _тип_ с kind-ом Nat это пустой тип без термов. Отличие от того что уже было (например, hackage://type-level) чисто сахарное. Лучше бы, конечно, были термо-зависимые типы с kind-ами * -> ... -> КакойТоТипНапримерInt -> ... -> *.

Ну правильный код же в том месте не дает эррора?

goodA :: TypeA
goodA = termOfTypeA
-- ^
-- Всё хорошо с точки зрения тайпчекера, нечего заменять.

badA :: TypeA
badA = termOfTypeB
-- ^
-- Will be replaced with
-- 
--   = error "... Expected type `TypeA' but found `termOfTypeB' of type `TypeB' in `badA' ..."
-- 
-- at compile time, but thrown an error at runtime. The error can be handled with `catch'-like functions.

у error тип forall a. String -> a, поэтому его можно подставить на место выражения любого типа (как и throw или undefined).

Лекции и задачи по топологии. Вербицкий М.

А это точно алгебра?

Теоремы и задачи функционального анализа.

Кириллов и Гвишиани?

А это точно алгебра?

нет, как видно из названия.

Кириллов и Гвишиани?

да

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

собственно, это решает вопрос — внутри existential надо сделать поле данных и поле функции, которая работает именно с этими данными; снаружи разрешить вызывать только эту функцию

ниже прога (правда, требует с++0х из-за unrestricted union); вопрос к читателям — что *опасного* можно сделать с объектом типа A1_or_A2 *после* того, как он инициализирован? по-моему, без нарушения типов с помощью reinterpret_cast и юнионов, отличных от А1_or_A2 ничего опасного не сделать

тут очевидно, что типизация в виде тайптега или че-то подобного нигде не хранится, но, как подсказал анонимус, въедливым читателям придется это доказывать; скажем, если бы в качестве аргумента вместо repeat_head1/repeat_head_twice2 использовался бы print1/print2, то можно было бы спорить на эту тему, т.к. в рантайме, имея указатель u.a1.function и доступ к сегменту кода, можно было бы проанализировать код function и определить количество разыменований (1 или 2 штуки) и так сделать вывод о его типе данных

именно поэтому function инициализируется не принтами, а параметрически полиморфной фигней, из кода которой тип данных не вытащищь — она прекрасно работает со всеми

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

#include <iostream>
#include <assert.h>
#include <stdlib.h>

typedef double  dbl;
typedef double* dbl_ptr;

int*  new1(int x) { return new int(x); }
dbl** new2(dbl x) { return new dbl_ptr( new dbl(x) ); }

struct Node1 { int*  element;  Node1* next;  Node1( int e, Node1* n ): element(new1(e)), next(n) {} };
struct Node2 { dbl** element;  Node2* next;  Node2( dbl e, Node2* n ): element(new2(e)), next(n) {} };
///               ^^ существенная разница

/// данные 2 функции не изменяют список, если он пустой, и повторяют голову списка, если он не пустой
/// пример: [1,2,3] преобразуется в [1,1,2,3]
/// кроме того, у данных 2 функций полностью одинаков бинарный код
Node1* repeat_head1(Node1* arg) { if(!arg) return arg;  Node1* node=new Node1(*arg);  node->next=arg; return node; }
Node2* repeat_head2(Node2* arg) { if(!arg) return arg;  Node2* node=new Node2(*arg);  node->next=arg; return node; }

Node1* repeat_head_twice1(Node1* arg) { return repeat_head1(repeat_head1(arg)); }
Node2* repeat_head_twice2(Node2* arg) { return repeat_head2(repeat_head2(arg)); }

/// возвращаемое значение, а не void, сделано для того, чтобы можно было заюзать эти функции вместо repeat_head
Node1* print1(Node1* node) {    if(!node) { std::cout << '\n'; }else{ std::cout <<  *(node->element) << ' ';   print1(node->next); }    return node; }
Node2* print2(Node2* node) {    if(!node) { std::cout << '\n'; }else{ std::cout << **(node->element) << ' ';   print2(node->next); }    return node; }
///                                                                                ^^ существенная разница

Node1* a1_d;  Node1* (*a1_f)(Node1*);
Node2* a2_d;  Node2* (*a2_f)(Node2*);

class A1 { Node1* data;  Node1* (*function)(Node1*);  public:  void init(){ data=a1_d; function=a1_f; }   void do_something(){ if(data && function) data=function(data); }  };
class A2 { Node2* data;  Node2* (*function)(Node2*);  public:  void init(){ data=a2_d; function=a2_f; }   void do_something(){ if(data && function) data=function(data); }  };

union A1_or_A2 {
  A1 a1;
  A2 a2;
};

void typesafe( A1_or_A2& a1_or_a2 ) {
      a1_or_a2.a1.do_something();
  /// a1_or_a2.a2.do_something(); <--- так тоже можно, и результат будет тот же
}

int main()
{
  /// проверяем, что в А1 и А2 нет скрытых полей с тайптегом
  assert( sizeof(A1)==2*sizeof(void*) );
  assert( sizeof(A2)==2*sizeof(void*) );

  assert( sizeof(int*)==sizeof(int) );
  assert( sizeof(dbl*)==sizeof(int) );

  Node1* ptr1 = new Node1( 1, new Node1( 11, NULL ) );
  Node2* ptr2 = new Node2( 2, new Node2( 22, new Node2( 222, NULL ) ) );

  A1 a1; a1_d=ptr1; a1_f = repeat_head1       ; a1.init();
  A2 a2; a2_d=ptr2; a2_f = repeat_head_twice2 ; a2.init();

  print1( *reinterpret_cast<Node1**>(&a1) );
  print2( *reinterpret_cast<Node2**>(&a2) );
  
  A1_or_A2 u; /// тут оно пока что не инициализировано

  u.a1=a1;
  typesafe(u);
  print1( *reinterpret_cast<Node1**>(&u) );

  u.a2=a2;
  typesafe(u);
  print2( *reinterpret_cast<Node2**>(&u) );

#ifdef AA1
  /// для тех, кто будет утверждать, что А1 и А2 это один и тот же тип -- расскомментируйте следующую строку и получите сегфолт:
  u.a1=a1;
  print2( *reinterpret_cast<Node2**>(&u) );
#endif
#ifdef AA2
  /// при этом следующие строки хотя и выдают бред, но сегфолт не вызывают:
  u.a2=a2;
  print1( *reinterpret_cast<Node1**>(&u) );
#endif
  return 0;
}

sizeof(int*) == sizeof(int) и sizeof(double*) == sizeof(int) - кстати, не факт (x86_64/Linux, например).

Попробуй добавить отладочную печать в оба метода do_something, тогда станет видно, что оба раза вызывается только один из них, в зависимости от того какой вариант выбран в typesafe.

Это случай если не одинаковых типов, то типов с одинаковым sizeof и memory layout - тут просто везёт. Возьмём действительно разные типы:

struct A1 {
    Node1* data;
    Node1* data2;
    Node1*(*fn)(Node1*);
    void do_something() { puts("A1 case"); if (data && fn) data = fn(data); if (data2 && fn) data2 = fn(data2); } };

struct A2 {
    Node2* data;
    Node2*(*fn)(Node2*);
    void do_something() { puts("A2 case"); if (data && fn) data = fn(data); }
};

union A1_or_A2 { A1 a1; A2 a2; };

безопасными будут все (типично) безопасные использования объединений:

    printf("%lu, %lu\n", sizeof(A1), sizeof(A2));

    A1 a1 = { new Node1(1, new Node1(11, NULL)), new Node1(3, new Node1(33, NULL)), repeat_head1 };
    A2 a2 = { new Node2(2, new Node2(22, new Node2(222, NULL))), repeat_head_twice2 };

    A1_or_A2 u;

    u.a1 = a1;
    u.a1.do_something(); // A1 case
    print1(u.a1.data);
    print1(u.a1.data2);

    u.a2 = a2;
    u.a2.do_something(); // A2 case
    print2(u.a2.data);

теперь если инициализировать u одним значением (a1 или a2), но вызвать метод по другому полю (u.a2.do_something() или u.a1.do_something(), соответственно), то что произойдет - метод класса A2 (или A1) будет вызван на объекте класса A1 (или A2), то есть он будет искать значения полей по смещениям одного класса в совсем другом классе:

    u.a1 = a1;
    u.a2.do_something(); // A2 case + segfault!
    print1(u.a1.data);
    print1(u.a1.data2);

    u.a2 = a2;
    u.a1.do_something(); // A1 case
    print2(u.a2.data);

в первом случае вполне может быть сегфолт, во втором, опять, просто везёт.

То есть, тот typesafe можно написать двумя вариантами и разницы между ними нет только при A == B в смысле memory layout. Что касается

    u.a1 = a1;
    print2(u.a2.data);

    u.a2 = a2;
    print1(u.a1.data);

то в первом случае мы лезем в объект класса A1 используя смещение из класса A2 и нам везёт (для data), но потом print2 пытается печатать список указателей на int как список указателей на указатели на double, то есть получается лишнее разыменование и всё падает. Во втором случае нам опять везёт с data, а print1 успешно печатает список **double как список *int, то есть разыменовывая как (int)(*(*int)((**double)x)), _если_ sizeof(**double) <= sizeof(*int) <= sizeof(int) (или для малых адресов), то мы увидим не сами doublы а те адреса по которым они лежат.

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

лавсан?

Нет. Просто анон, искренне непонимающий, нахрена делать слаботипизированный юнион строготипизированным. И твёрдо уверенный, что если это вообще можно сделать, то только с помощью динамического тайп-тега. Только сделать нормально, без UB при любом составе юниона (включая шаблонные классы) и любом обращении с ним (за исключением прямого засирания памяти).

напомню, что разговор шел о том, можно ли сделать какое-то *конкретное* объединение неразмеченным; и квазимото писал Человеческое метапрограммирование (комментарий)

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

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

Только сделать нормально, без UB при любом составе юниона (включая шаблонные классы) и любом обращении с ним (за исключением прямого засирания памяти).

такой вопрос, по-моему, там не стоял, но это интересный, хотя наверно и непрактичный вопрос — примерно сколько типовой информации можно стереть из рантайма

sizeof(int*) == sizeof(int) и sizeof(double*) == sizeof(int) - кстати, не факт

спасибо, К.О. — именно потому, что не факт, я и поставил ассерты

void do_something() { puts(«A1 case»); if (data && fn) data = fn(data); }
void do_something() { puts(«A2 case»); if (data && fn) data = fn(data); }

зря стараешься

испортить код так, чтобы все сломалось, можно еще проще:

struct A1 { int   x; void do_something() { .... } };
struct A2 { float x; void do_something() { .... } };

код void do_something() в обоих случаях один и тот же по той причине, что классы А1 и А2 являются двумя конкретизациями (или специализациями, х.з. как оно там правильно называется) одного и того же экзистенциального класса

напрямую и типобезопасно это на с++ не выразить, приходится дуплицировать код

код void do_something() в обоих случаях один и тот же

Теперь понял. То есть мы берём _разные_ типы (Node1 и Node2, например), обворачиваем их в шаблонный класс с набором методов которые обращаются с этими типами _как с одинаковыми_. Тогда на объединении из специализаций этого шаблонного класса можно вызывать методы этого класса, и так как они не видят разницы в типах по которым проводится специализация и никак от этой разницы не зависят, то всё будет хорошо. Если начать вызывать на таком объединении какие-то другие функции не предусмотренные шаблонным классом (например print1 и print2), тогда разница может проявиться, поэтому лучше скрыть соответствующие поля в private области.

#include <iostream>

Сударь, неужели Вы не поняли?

Сия дискуссия — об анафорических лямбдах, пандорических захватах, рекурсивных схемах, аппликативных функторах, ленивых продолжениях, зигохистоморфных препроморфизмах, метациклических суперкомпиляторах, монадических трансформерах, алгебре и коалгебре Калвина Элгота наконец. А Вы влезаете в неё со своей императивной пошлятиной. Фи, как это низко, сударь! Я Вам сейчас лицо набью!

Трансформеры - это нам понятно...

Трансформеры - это нам понятно...

А что не понятно? «Монадический»?

Но ведь это же элементарно! Монада — всего-навсего моноид в категории эндофункторов!

Это типа как модули в руби?

Это типа как модули в руби?

Нет, не типа.

методы и классы определяются отдельно и в произвольном порядке

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

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

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

Для определения свойства node-thickness для объектов некоего класса shape-node я пишу:

(defaccessor node-thickness ((node shape-node))
  (:slot 'thickness)
  (:test #'=)
  (:changing-trigger trigger-node-thickness-changing)
  (:changed-trigger trigger-node-thickness-changed)
  (:op-class 'node-thickness-changed-operation)
  (:op-initargs '(:node :value0 :value))
  (:postform 
   (progn
     (trigger-connectable-entry-changed node)
     (reallocate-geometry node)))
  (:documentation "The node thickness."))

Здесь defaccessor является макросом, а его текущее применение определяет два метода node-thickness и сетер (setf node-thickness) для аргумента класса shape-node. То есть, мы добавляем два метода, ничего не предполагая заранее о классе. Методы сами по себе, класс shape-node сам по себе. Всю фактическую привязку к классу мы определяем на месте: используем слот thickness, предикат = для сравнения, перед изменением вызываем тригер trigger-node-thickness-changing, после изменения свойства - тригер trigger-node-thickness-changed, сам факт изменения заносим в лог операций Redo/Undo с помощью операции node-thickness-changed-operation. После окончания операции выполняем последействия из формы :post-form.

Похожим образом я определяю тригеры событий через макрос deftrigger, который опять же за меня создает нужные мне методы, специализируемые на объектах класса shape-node. Именно они вызываются в сетере (setf node-thickness). Все очень декларативно.

(deftrigger trigger-node-thickness-changing :before ((node shape-node))
  (:slot 'thickness-changing-source)
  (:documentation "Raised when the thickness is changing."))

(deftrigger trigger-node-thickness-changed :after ((node shape-node))
  (:slot 'thickness-changed-source)
  (:documentation "Raised when the thickness has changed."))

Сами внешние события тоже определяются через макрос defevent, который также ничего не знает о классе, для которого он определяет методы. Как и в F#, событие - это метод или функция, возвращающая некий объект, у которого можно подписать обработчики сообщений. Вот, node-thickness-changing и node-thickness-changed - это методы для shape-node, и они возвращают такие объекты:

(defevent node-thickness-changing ((node shape-node))
  (:slot 'thickness-changing-source)
  (:documentation "Raised when the thickness is changing."))

(defevent node-thickness-changed ((node shape-node))
  (:slot 'thickness-changed-source)
  (:documentation "Raised when the thickness has changed."))

В завершение мы должны определить соответствующую операцию для Redo/Undo:

(defoperation node-thickness-changed-operation
  (:initargs '(:node :value0 :value))
  (:writer node-thickness)
  (:documentation "The operation when the node thickness changes."))

Операция запоминает узел, прежнее и следующее значения свойства node-thickness. При вызове Redo или Undo операция меняет значение свойства через сетер (setf node-thickness), который передается в форме :writer.

Я привел примеры нескольких макросов, которые ничего не знают о классе shape-node и которые создают новые методы для него. Здесь я даже не приводил определение самого класса (а оно очень простое). И что примечательно, мои примеры не содержат кода вообще, а задают некоторое декларативное описание того, что мы хотим получить.

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

class A
  def a
    puts 'a'
  end
end

class A
  def b
    puts 'b'
  end
end

class A
  def c
    puts 'c'
  end
end

a = A.new
a.a #a
a.b #b
a.c #c

class A
  def d
    puts 'd'
  end
end


a.d #d

А вот что похоже (если я правильно понимаю) на макрос в данном случае.

module M
  def e
    puts 'e'
  end
  def f
    puts 'f'
  end
end

class A
  include M
end

class B
  include M
end

a.e #e
a.f #f

b = B.new

b.e #e
b.f #f

Класс в руби это тот же объект, следовательно у него есть методы, в т.ч. специальные методы для метапрограммирования.

module N
  def g
    puts 'g'
  end
end

A.class_eval{
  include N
}

a.g #g

A.class_eval{
  extend N
}
A.g #g

макрос defevent, который также ничего не знает о классе

А вот модули кое-что знают о классе

module O
  def self.included klass
    puts klass
  end
  def h
    puts 'h'
  end
end

A.class_eval{
  include O
} #A
a.h #h

p A.included_modules #//[O, N, M, Kernel]

И что примечательно, мои примеры не содержат кода вообще

Ну где-то же код всеравно есть) - напоминает паттерн «композитный метод».

Как-то так..

дообределить

... спать что ли лечь...

Любопытно. Все же надо бы мне как-нибудь выделить время на изучение Руби :)

http://share.xmarks.com/folder/bookmarks/SFFZKaSIM4

Спасибо, занес в закладки.

А как быть с множественной диспетчеризацией?

макрос определяет методы для произвольного класса
То есть, мы добавляем два метода, ничего не предполагая заранее о классе. Методы сами по себе, класс shape-node сам по себе.

...а в результате код класса оказывается размазанным по всему проекту. Лепота!

И понятия «low coupling» и «high cohesion», надо полагать, выдумали яйцеголовые теоретики, ничего не понимающие в архитектуре и программировании, ага.

Например, в одном своем (незавершенном) проекте
незавершенном
незавершенном

Попутного ветра, чо.

И понятия «low coupling» и «high cohesion», надо полагать, выдумали яйцеголовые теоретики, ничего не понимающие в архитектуре и программировании, ага.

Напиши жалобу в комитет по стандартизации ANSI CL. Можно коллективную.

Напиши жалобу в комитет по стандартизации ANSI CL. Можно коллективную.

Что ещё предложишь? В штаб-квартиру сайентологов написать? Или Петрику с Фоменкой?

...а в результате код класса оказывается размазанным по всему проекту. Лепота!

А там и нет кода классов, там классы это вроде как struct в С++, а методы - любые перегруженные (с рантайм диспетчеризацией, то есть мультиметоды) функции которые могут спокойно дописываться и оперировать слотами struct (так как они все в public). То есть нет ситуации с классами с private данными которым никак нельзя дописать некоторых методов не поправив сам класс (чтобы тот соизволил принять метод) или не унаследовал производный класс. Разрешая свободно расширять интерфейс класса мы также даём возможность новым частям интерфейса сломать все остальные части, нарушив необходимые инварианты, но это плата за гибкость. Потом, никто не мешает запилить «своё ООП» на макросах (даже поверх CLOS).

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