Комментарии 102
Отличная статья (совсем малость опечаток). Напомнила мне, разъяснения о типах в scala Мартином Одерски (лекция 4.2 из progfun — «Objects Everywhere»).
«Strong typing» правильно переводить, как сильная типизация, если она сопоставляется слабой.
Сильная и слабая типизация на Вики
Сильная и слабая типизация на Вики
(Читать это определение стоит так: Bool может быть или True или False.) В принципе, можно было бы описать этот тип и в C++:
enum bool { true, false };
Только, наверно, лучше было бы
enum bool {
false,
true
};
:)
Перевод хороший, статья плохая — у автора узский взгляд на многие вещи.
Спасибо!
По поводу взглядов поделитесь, если можете, интересно было бы обсудить.
По поводу взглядов поделитесь, если можете, интересно было бы обсудить.
На мой взгляд, автор заметно преувеличивает полезность статической типизации. Или преуменьшает полезной динамической :-) как посмотреть.
В частности, не понравился пример с обезьянками. В нём просто не учтено, что человек — это не генератор рандомных последовательностей, а вполне себе сложный механизм с заложенными знаниями предметной области и умениями пользоваться инструментарием ЯП. Соответственно, выигрыш от статической типизации надо смотреть в сравнении с программистами, а не с /dev/random. А в этом случае получается что статический контроль сокращает работу таких «обезьянок» не так уж на много. Плюс, не учтены правила синтаксиса ЯП, которые будут резать неверный код куда лучше.
Чисто пропагандистский пример получается.
Также не согласен вот с этим положением
«Нагрузка» идёт не от необходимости помнить типы или выводить их. Чем больше формальных правил в ЯП, тем сложнее его модель вычислений, тем больше надо держать в голове мелких нюансов и особенностей. Каждое ограничение, по сути, усложняет процесс формирования алгоритма и его последующего анализа. Про это автор совсем не упоминает, хотя это куда более серьёзная проблема.
По общей интонации напоминило раговоры студентов в духе «моя технология самая крутая», а это не лучший стиль для пропагандисткой статьи, на мой взгляд.
В частности, не понравился пример с обезьянками. В нём просто не учтено, что человек — это не генератор рандомных последовательностей, а вполне себе сложный механизм с заложенными знаниями предметной области и умениями пользоваться инструментарием ЯП. Соответственно, выигрыш от статической типизации надо смотреть в сравнении с программистами, а не с /dev/random. А в этом случае получается что статический контроль сокращает работу таких «обезьянок» не так уж на много. Плюс, не учтены правила синтаксиса ЯП, которые будут резать неверный код куда лучше.
Чисто пропагандистский пример получается.
Также не согласен вот с этим положением
строгая типизация накладывает слишком много нагрузки на программиста. … только вот есть технология, вывод типов, которая позволяет компилятору вывести большинство типов из контекста …
«Нагрузка» идёт не от необходимости помнить типы или выводить их. Чем больше формальных правил в ЯП, тем сложнее его модель вычислений, тем больше надо держать в голове мелких нюансов и особенностей. Каждое ограничение, по сути, усложняет процесс формирования алгоритма и его последующего анализа. Про это автор совсем не упоминает, хотя это куда более серьёзная проблема.
По общей интонации напоминило раговоры студентов в духе «моя технология самая крутая», а это не лучший стиль для пропагандисткой статьи, на мой взгляд.
Во-первых, автор написал про синтаксическое отсечение.
Во-вторых, автор как раз сказал, что правила упрощают анализ алгоритмов, превращая этот анализ в доказательство теоремы.
В-третьих, в дополнение к упрощению типы придают еще и корректность, которую можно доказать. Не прикинуть в голове, а именно доказать.
В-четвертых, уже мое мнение: при написании программ на языках со слабой типизацией, в голове у меня все равно есть все типы. Только компилятор мне не помогает. По сути, разница только в этой помощи.
Во-вторых, автор как раз сказал, что правила упрощают анализ алгоритмов, превращая этот анализ в доказательство теоремы.
В-третьих, в дополнение к упрощению типы придают еще и корректность, которую можно доказать. Не прикинуть в голове, а именно доказать.
В-четвертых, уже мое мнение: при написании программ на языках со слабой типизацией, в голове у меня все равно есть все типы. Только компилятор мне не помогает. По сути, разница только в этой помощи.
Или преуменьшает полезной динамическойА в чем эта полезность состоит, кроме очевидного факта, что меньше писать не надо? У меня маленький опыт работы с динамически типизированными языками, но я часто видел, как на таких языках, например, перед определением функции в комментариях пишут типы её аргументов (скажем, аргумент с таким именем должен быть строкой, а с таким — числом) или первыми строками в теле функции проверяют, что аргументы того типа, что надо.
А «bottom» по-дурацки на русском — это «днище»? «Функция вернула днище»/ «Функция достигла днища (своей полезности)»?
«В языках программирования функции, которые всегда дают одинаковый результат на одинаковых аргументах и не имеют побочных эффектов, называются чистыми. В чистом функциональном языке наподобие Haskell все функции чисты.»
С этой точки зрения — в Хаскелле нет функции генерации псевдослучайного числа без аргументов? Есть. Какое-то противоречие.
С этой точки зрения — в Хаскелле нет функции генерации псевдослучайного числа без аргументов? Есть. Какое-то противоречие.
Конечно, есть! Просто эта функция принимает аргумент: состояние генератора, а возвращает два значения: новое состояние генератора и псевдослучайное число. В следующий раз вам следует вызвать ее с новым состоянием генератора и она вернет следующее.
В этом и прелесть монад состояния. Они очень простые — вы просто вместо обычного глобального состояния передаете обьект состояния в чистую функцию, и получаете новое.
В этом и прелесть монад состояния. Они очень простые — вы просто вместо обычного глобального состояния передаете обьект состояния в чистую функцию, и получаете новое.
Дополню свой ответ, в хаскелле действительно есть и функция генерации псевдослучайного числа без аргументов. Вернее, не уверен, что есть, но написать точно можно. Но дело в том, что эта функция будет типа :: IO Int и, в сущности это тот же State, только для внешнего мира: так как внешний мир — синглетон, то и аргумент состояния не нужен, монадическое состояние для IO передается внутри значения завернутого в оное IO. Не уверен, что я хорошо обьяснил, но лучше придумать не получается.
Функции внутри haskell (без IO) будут все принимать State.
Функции внутри haskell (без IO) будут все принимать State.
Просто на мой взгляд трудно будет назвать такую функцию чистой. Извините, я не силен в терминах монад. Я понял ваш ответ так, что вызов такой функции генерации случайного числа изменяет некое состояние (или проводит действие, эквивалентное изменению состояния). Мне кажется, что тогда можно утверждать, что функция будет иметь побочные эффекты, что делает ее грязной. Следовательно, утверждение «все функции в Хаскелле чистые» неверно.
Это как посмотреть. Она изменяет состояние компьютера — просто некий массив байт. IO a — это тоже, что и State RealWorld a, то есть, по сути тоже пара (мир, a). Мы принимаем мир, а возвращаем такую пару в виде IO a. Это точно то же самое, что и State RW a — что в точности (RW, a), так что c точки зрения хаскелля происходит тоже самое: мы принимаем какой-то мир и возвращаем результат и какой-то измененный мир. Побочные эффекты будут в железе, но это принято считать деталью реализации (ну не эффективно же хранить все-все состояния компьютера: по жесткому диску на каждое измемнение байта, и т.п.), с чистым интерфейсом. То есть, побочный эффект есть с точки зрения железячников, а с точки зрения программиста его как бы и нет.
Из вашей статьи:
В языках программирования функции, которые всегда дают одинаковый результат на одинаковых аргументах и не имеют побочных эффектов, называются чистыми.Отсюда напрямую следует, что чистая функция без аргументов обязана всегда возвращать один и тот же результат. Так что вы либо используете какое-то другое определение чистоты, либо не правы с точки зрения этого определения.
Функция-то монадическая, она только выглядит без аргументов, а на самом деле у нее есть аргумент-контекст, скрытый в монадическом значении, независимо от того, какая эта монада, но в монадах IO и State этот контекст — тот самый контекст, хорошо известный императивщикам — данные (о мире и структура соответственно).
Можно еще по-другому сказать: функция всегда возвращает одинаковый результат, но этот результат — сам по себе вычислимый обьект, и вот эти обьекты, когда вычисляются принимают контекст от предыдущего такого обьекта, изменяют его, и передают дальше измененным.
Я понимаю, что это все очень сложно звучит, но на самом деле это просто:
монадические «значения» (функции без аргументов) соединяются в одно монадическое значение посредством >>= (bind). И оператор >>= по сути «вычисляет» монадическое значение IO a, достает из него результат, выполняет функцию над результатом и возвращает новое монадическое значение с контекстом, которые вернуло исходное и значением, вычисленным функцией, вот пример:
Если мы захотим сумму двух случайных чисел, то будет:
То есть, формально аргументов нету и функция getRandomInt чистая, но оператор >>= работает так, что он забирает контекст у левого значения и создает значение с этим контекстом и функцией, которая должна будет вычислить значение справа. Кажется, у меня язык не подвешен такое обьяснять :)
Можно еще по-другому сказать: функция всегда возвращает одинаковый результат, но этот результат — сам по себе вычислимый обьект, и вот эти обьекты, когда вычисляются принимают контекст от предыдущего такого обьекта, изменяют его, и передают дальше измененным.
Я понимаю, что это все очень сложно звучит, но на самом деле это просто:
монадические «значения» (функции без аргументов) соединяются в одно монадическое значение посредством >>= (bind). И оператор >>= по сути «вычисляет» монадическое значение IO a, достает из него результат, выполняет функцию над результатом и возвращает новое монадическое значение с контекстом, которые вернуло исходное и значением, вычисленным функцией, вот пример:
getRandomInt :: IO Int
(getRandomInt >>= \x -> return (toFloat x)) :: IO Float.
Если мы захотим сумму двух случайных чисел, то будет:
(getRandomInt >>= (\x -> getRandomInt >>= (\y -> return (x + y)))) :: IO Int
То есть, формально аргументов нету и функция getRandomInt чистая, но оператор >>= работает так, что он забирает контекст у левого значения и создает значение с этим контекстом и функцией, которая должна будет вычислить значение справа. Кажется, у меня язык не подвешен такое обьяснять :)
Простите, я, как «прожженый объектно-ориентировенный» программист, уточню понятие:
правильно ли я понимаю, что точным аналогом «монадической функции» является функция-метод объекта, который изменяет только этот объект (и, возможно, вложенные в него сущности), но не изменяет внешний мир?
правильно ли я понимаю, что точным аналогом «монадической функции» является функция-метод объекта, который изменяет только этот объект (и, возможно, вложенные в него сущности), но не изменяет внешний мир?
Монадическая функция это функция которая возвращает функцию которая из одного состояния объекта и аргумента переводит в другое состояния объекта. Частный случай объекта — это весь мир.
Нет, монадическая функция, это функция оперирующая монадою. Она вовсе не обязана менять какое-то состояние или иметь к ним хоть какое-то отношение, так как монада — не о состояниях, это более общий случай. Например replicateM — монадическая функция, и, к примеру
или
однако
И никакого состояния в последнем случае нет, ибо монада тут списочная, а не монада состояния или IO, как в примерах выше.
ghci> replicateM 3 (putStrLn "Hello")
Hello
Hello
Hello
[(),(),()]
или
ghci> execState (replicateM 3 (modify (+1))) 0
3
однако
ghci> replicateM 3 [1,2]
[[1,1,1],[1,1,2],[1,2,1],[1,2,2],[2,1,1],[2,1,2],[2,2,1],[2,2,2]]
И никакого состояния в последнем случае нет, ибо монада тут списочная, а не монада состояния или IO, как в примерах выше.
Вернее наоборот
Тип IO a это функция, которая берет состояние RealWord и возвращает пару из нового состояния и значения.
So, 'main' just has type «IO ()», 'getChar' has type «IO Char» and so on. You can think of the type «IO Char» as meaning «take the current RealWorld, do something to it, and return a Char and a (possibly changed) RealWorld». Let's look at 'main' calling 'getChar' two times:
Это из www.haskell.org/haskellwiki/IO_inside#Welcome_to_the_RealWorld.2C_baby
Тип IO a это функция, которая берет состояние RealWord и возвращает пару из нового состояния и значения.
type IO a = RealWorld -> (a, RealWorld)
So, 'main' just has type «IO ()», 'getChar' has type «IO Char» and so on. You can think of the type «IO Char» as meaning «take the current RealWorld, do something to it, and return a Char and a (possibly changed) RealWorld». Let's look at 'main' calling 'getChar' two times:
getChar :: RealWorld -> (Char, RealWorld)
main :: RealWorld -> ((), RealWorld)
main world0 = let (a, world1) = getChar world0
(b, world2) = getChar world1
in ((), world2)
Это из www.haskell.org/haskellwiki/IO_inside#Welcome_to_the_RealWorld.2C_baby
Нет, состояние — частный случай монады, чуть выше я привел комментарий с примерами. Но если говорить конкретно о IO, то IO так и определён, как функция, принимающая старое состояние, и возвращающая новое + какой-то результат:
IO является при этом монадой, но не всякая монада — IO.
Чтобы быть монадою (в Haskell), для типа должны быть определены операции (также удовлетворяющие некоторым законам):
Что позволяет использовать в применении к этому типу синтаксический сахар do, например, или просто набор библиотечных монадических функций.
Например, в C# — LINQ — аналог монады, может быть реализован для разных типов. В Scala, насколько я знаю, это for с его for (x < — ...; y < — ...). Там тоже надо реализовать пару функций и можно использовать в for любой тип.
newtype IO a = IO (State# RealWorld -> (# State# RealWorld, a #))
IO является при этом монадой, но не всякая монада — IO.
Чтобы быть монадою (в Haskell), для типа должны быть определены операции (также удовлетворяющие некоторым законам):
return :: a -> m a --
(>>=) :: m a -> (a -> m b) -> m b
Что позволяет использовать в применении к этому типу синтаксический сахар do, например, или просто набор библиотечных монадических функций.
Например, в C# — LINQ — аналог монады, может быть реализован для разных типов. В Scala, насколько я знаю, это for с его for (x < — ...; y < — ...). Там тоже надо реализовать пару функций и можно использовать в for любой тип.
Аналогом монады состояний является переменные в императивных языках.
На самом деле состояние не изменяется, а создается новое :)
Внутри монады State, когда вы выполняете bind с другой чистой функцией(вне монады State) у вас создается новое окружение с уже новым значением State. Это чем-то напоминает как работает scope в Javascript. Scope в данном случае выступает в качестве State и мы не меняем scope у исходной функции, а создаем новую функцию с новым измененным scope.
Надеюсь хоть немного стало понятнее )
Внутри монады State, когда вы выполняете bind с другой чистой функцией(вне монады State) у вас создается новое окружение с уже новым значением State. Это чем-то напоминает как работает scope в Javascript. Scope в данном случае выступает в качестве State и мы не меняем scope у исходной функции, а создаем новую функцию с новым измененным scope.
Надеюсь хоть немного стало понятнее )
Попробую проиллюстрировать на примере javascript, как можно сохраняя чистоту «изменять» состояние, изобразив нечто схожее с монадами
Скрытый текст
//чистая функция
function random(state) {
//[значение, новое состояние]
return [state % 10, state + 1];
}
//обычная функция
function add4(v) {
return v + 4;
}
//fs - чистая функция наподобии random, state - начальное состояние
function makeMonad(fs, state) {
//функция не принимающая состояние, помещенная в "коробку"
return function () {
return fs(state);
};
}
//fs - функция наподобии random, f - обычная функция не принимающая состояние, наподобие add4
//возвращается функция, обернутая в монаду c другим состоянием.
function bind(fs, f) {
return function() {
var [value, state] = fs();
return [f(value), state];
};
}
//получить чистое значение из монады, без изменения состояния
function call(fs) {
return fs[0];
}
//тогда пример работы с генератором:
var generator = makeMonad(random, 0);
bind(generator, function(randomValue) {
//здесь работаем с псевдослучайным значением
});
Хорошая попытка, но немного не так.
//чистая функция
function random(state) {
//[значение, новое состояние]
return [state + 1, state % 10];
}
function runMonad(mval, state) {
return mval(state);
}
function makeMonad(val) {
return function(state) {
return [val, state];
}
}
function bind(mval, fn) {
return function(state) {
var [val, state1] = mval(state);
return runMonad(fn(val), state1);
}
}
[sum, _] = runMonad(
bind(random, function(x) { // x is a first random number (16)
return bind(random, function(y) { // y is a second random number (6)
return makeMonad(x+y); // sum of two random numbers (22)
});
}),
15 // random seed
);
// sum == 22
Тут, кстати, очень хорошо видно: random можно одновременно рассматривать и как чистую функцию и как монадическое значение (функция без аргументов): так он передается в bind.
Похоже, самым простым обьяснением было бы, что функция без аргументов в нотации хаскеля readRandomInt :: IO Int на самом деле в теории имеет аргумент типа RealWorld, это сразу понятно, если написать:
Похоже, самым простым обьяснением было бы, что функция без аргументов в нотации хаскеля readRandomInt :: IO Int на самом деле в теории имеет аргумент типа RealWorld, это сразу понятно, если написать:
data IO a = State a RealWorld
Нет, не так. В вашем случае bind вернет функцию, которая при вызове выдаст обычное число, а не пару [значение, новое сотояние]. Т.е. функция bind не возвратит монаду, а должна.
Смотрите. Какая-нибудь randomRIO (возьму функцию с явным аргументом, чтобы не конфликтовать по поводу терминологии и отличий значения от 0-арной функции) с типом :: Random a => (a, a) -> IO a абсолютно чистая, потому что для одного и того же аргумента с типом (а, а) она вернёт одно и то же значение типа IO a. В это значение завёрнута функция, которая принимает RealWorld (как тут уже объяснили в комментариях) и возвращает пару из значения типа a и нового RealWorld'а, и она тоже чистая, потому что для одинаковых состояний мира она вернула бы одну и ту же пару. Фича реализации типа IO в том, что эту копию состояния нельзя получить (в общем-то, как и в реальном мире :). И монада IO — не единственный вариант это обеспечить. Например, в Clean тоже все функции чистые, а невозможность копировать мир достигается при помощи уникальных типов. Похожий механизм, кажется, есть в Rust. А в старых, домонадических версиях хаскеля были явные функции, обрабатывавшие мир (точнее, приходящие от него события).
Насколько я понял в хзаскеле нет функции генерации псевдослучайного числа без аргументов
www.haskell.org/haskellwiki/IO_inside#Welcome_to_the_RealWorld.2C_baby
IO Int это функция без аргументов, которая возвращает функцию которая берет состояние мира и возвращает следующее состояие мира и число
www.haskell.org/haskellwiki/IO_inside#Welcome_to_the_RealWorld.2C_baby
IO Int это функция без аргументов, которая возвращает функцию которая берет состояние мира и возвращает следующее состояие мира и число
Я больше нахожу противоречие в том, что True и False не могут иметь тип Bool, потому как написаны с большой буквы…
Вот тут я не понял, что вы сказали. True и False — конструкторы типов, они, как и типы, записываются с большой буквы. Есть тип, у него есть конструкторы, вызов которых создает значения, и есть значения.
data Bool /* тип */ = True | False /* конструкторы без аргументов */
let a /* значение :: Bool */ = True /* вызов конструктора без аргументов */
Фактически True :: Bool — потому, что это вызов конструктора без аргументов, возвращающего Bool.
data Bool /* тип */ = True | False /* конструкторы без аргументов */
let a /* значение :: Bool */ = True /* вызов конструктора без аргументов */
Фактически True :: Bool — потому, что это вызов конструктора без аргументов, возвращающего Bool.
Только не конструкторы типов, а конструкторы значений (value constructors). Конструктор типов — это Bool
Ну, из статьи следует, что типы записываются с большой буквы, а значения этих типов — с маленькой. Также в статье сделан упор на строгую типизацию хаскеля, поэтому Присваивание типа True или типа False в тип Bool должно выдать ошибку.
Но тут всплывает еще одна сущность — некие конструкторы типов, о которых в статье ни слова. Поэтому и непонятно, как так: сначала автор говорит одно, а потом тут же показывает пример, нарушающий собственные же слова (нарушающий с точки зрения знаний, которые он дал в своей статье).
Но тут всплывает еще одна сущность — некие конструкторы типов, о которых в статье ни слова. Поэтому и непонятно, как так: сначала автор говорит одно, а потом тут же показывает пример, нарушающий собственные же слова (нарушающий с точки зрения знаний, которые он дал в своей статье).
Ну, как я понимаю, здесь Bool — это алгебраический тип данных, или тип-сумма, или перечисление типов. То есть, объекты типа Bool могут принимать значения только перечисленных в нем типов (либо True, либо False). А у этих типов в свою очередь может быть только одно значение у каждого, которое конструируется просто вызовом True или False — в таком случае эти имена будут выступать как конструкторы значений своих типов.
> в Хаскелле нет функции генерации псевдослучайного числа без аргументов?
Нету, если не считать unsafePerformIO, бо IO a таки принимает аргументы
Нету, если не считать unsafePerformIO, бо IO a таки принимает аргументы
Собственно hackage.haskell.org/package/ghc-prim-0.3.1.0/docs/src/GHC-Types.html#IO
newtype IO a = IO (State# RealWorld -> (# State# RealWorld, a #))
Спасибо за перевод. Надеюсь вы не остановитесь и продолжите перевод дальнейших статей.
Хотел уточнить вопрос насчет bottom, может кто-нибудь прояснит.
Как я понял, для того чтобы иметь возможность оперировать функциями, которые никогда не завершаться, как с математическими функциями мы расширяем множество типов значением bottom.
Значит ли это, что Bool = True | False на самом деле Bool = True | False | _|_?
И то, что () = _|_, т.е. у нас не существует типа, не содержащего ни одного элемента, т.к. любое множество типов должно содержать bottom?
Хотел уточнить вопрос насчет bottom, может кто-нибудь прояснит.
Как я понял, для того чтобы иметь возможность оперировать функциями, которые никогда не завершаться, как с математическими функциями мы расширяем множество типов значением bottom.
Значит ли это, что Bool = True | False на самом деле Bool = True | False | _|_?
И то, что () = _|_, т.е. у нас не существует типа, не содержащего ни одного элемента, т.к. любое множество типов должно содержать bottom?
Да, про Bool вы правы, а вот про () — нет. На самом деле () = () | _|_. А вот Void действительно = _|_.
Но про _|_ автор не беспокоится, и вот почему: дело в том, что в хаскелле _|_, оно же unedfined (на самом деле значение _|_ создается функцией raise#), так вот, это самое _|_ может возникнуть только в некорректной программе.
То есть, представляя, что программа корректная, можно не волноваться о _|_, как автор и поступил, и тогда все рассуждения верны. Некорректная же программа не выдаст результата, а выдаст _|_ — на этом можно закончить анализ этого значения с точки зрения программиста.
Но про _|_ автор не беспокоится, и вот почему: дело в том, что в хаскелле _|_, оно же unedfined (на самом деле значение _|_ создается функцией raise#), так вот, это самое _|_ может возникнуть только в некорректной программе.
То есть, представляя, что программа корректная, можно не волноваться о _|_, как автор и поступил, и тогда все рассуждения верны. Некорректная же программа не выдаст результата, а выдаст _|_ — на этом можно закончить анализ этого значения с точки зрения программиста.
Некорректная же программа не выдаст результата, а выдаст _|_ — на этом можно закончить анализ этого значения с точки зрения программиста.
Я только теперь заметил, как получилось символично!
Вот этот товарищ принимает участие в IFCFPC в составе команды «Lazy Bottoms» users.livejournal.com/_adept_/24049.html
del
… а теперь вспоминаем про функцию try, которая способна преобразовать bottom в строку — и понимаем, что все не так-то и просто :)
Это у автора статьи каша в голове. Дно (символ ⊥) нужно для того, чтобы вообще можно было дать формальное определение рекурсивным функциям. Он обозначает наименьшее значение в семантическом домене (это не множества, а верхние полурешётки), который соответствует некоторому типу. Хотя, очень распространено мнение, что вот мол теория категорий является решением для разных хитрых рекурсивных типов, на самом деле, это не так. Решением является теория семантических доменов Дана Скотта.
Так вот. Дно имеет следующее отношение к рекурсии. Когда некто пишет рекурсивное уравнение для функции, то этот некто, на самом деле, говорит: найдите мне функцию, которая является решением для этого уравнения. Факториал вот классический пример (я уж напишу на псеводязыке):
В этом уравнении искомая функция — это
А потом мы должны найти то, что называет обратным пределом для этой функции. Техника поиска обратного предела — это вычисление такого значения:
То есть, дно нужно как наименьший элемент для начала рекурсии. Формально, Вы правы, для Bool тоже есть своё дно. Оно просто не имеет смысла, потому что в домене Bool нельзя написать рекурсивных уравнений. Пустой тип состоит только из дна.
Так вот. Дно имеет следующее отношение к рекурсии. Когда некто пишет рекурсивное уравнение для функции, то этот некто, на самом деле, говорит: найдите мне функцию, которая является решением для этого уравнения. Факториал вот классический пример (я уж напишу на псеводязыке):
fact =λx. x == 0 ? 1 : x * fact(x-1)В этом уравнении искомая функция — это
fact. Для решения этих уравнений применяется оператор фиксированной точки. Применяется он к генерирующей функции, построенной по исходному выражению. В данном случае это будет простоgen = λfact. λx. x == 0 ? 1 : x * fact(x-1)А потом мы должны найти то, что называет обратным пределом для этой функции. Техника поиска обратного предела — это вычисление такого значения:
gen^n(⊥) при n идущем в бесконечность (крышка обозначает степень). Можно доказать, что для монотонных функций в верхних полурешётках этот предел всегда существует.То есть, дно нужно как наименьший элемент для начала рекурсии. Формально, Вы правы, для Bool тоже есть своё дно. Оно просто не имеет смысла, потому что в домене Bool нельзя написать рекурсивных уравнений. Пустой тип состоит только из дна.
Хорошее пояснение, но думаю, что автор сознательно упростил понятия, ведь и цикл называется ТК для программистов, а не теория типов для хардкорных маматематиков. Я тоже на некоторые вещи там морщусь, но не уверен, что стоит так резко про голову и кашу.
Он говорит, что это незавершающееся вычисление. Но это именно неопределённость. Среди незавершающихся вычислений могут быть вполне хорошо типизированные. Какой-нибудь сервер, например.
Я понял слово незнезавершающиеся не строго как вечные, а просто как те, которые могут не завершится успешно. То есть, банально некорректные. Видимо автор прежде всего думал о вечной зацикленной рекурсии, вот и сам зациклился. В любом случае, в посте есть ремарка о рантайм-ошибках.
Вы пишете кучу прекрасных вещей, но как-то слишком неоправданно строги, на мой вкус, особенно ввиду того, что автор сознательно с самого начала сказал, что цикл о идеях и строгость изложения будет низкая.
Вы пишете кучу прекрасных вещей, но как-то слишком неоправданно строги, на мой вкус, особенно ввиду того, что автор сознательно с самого начала сказал, что цикл о идеях и строгость изложения будет низкая.
Ну, нам же хотят привить строгость математического мышления в терминах теории категорий… Мне на самом деле просто очень хочется понять, каким боком она во всём этом присутствует. Либо это просто такой модный язык, либо в ней реально что-то такое есть. До сих пор не понял. Поэтому и пытаюсь докопаться до самых оснований.
Ох, давайте так — открываете коды программ на разных ML языках, и отдельно открываете коды программ на Хаскеле (Хаскель почти является языком ML).
Хоть типы данных (АТД) можно примерно одинаково составлять как в Хаскеле, так и в OCaml, F#, SML (со Scala немного по другому (тем более, что это не ML язык, хоть хочет быть на него похож), поэтому для чистоты эксперемента не рассматриваем).
Только Хаскель использует разнообразные АТД везде (примерно так же, как и классы в Яве или С#), а OCaml, F#, SML в основном используют «примитивы» и «простые» АТД, в основном для контейнерности. В OCaml почти допилили модули, и они стали хорошей заменой объектам и АТД.
Так вот, категории — это очень удобный интрументарий работы с АТД в Хаскеле.
Хоть типы данных (АТД) можно примерно одинаково составлять как в Хаскеле, так и в OCaml, F#, SML (со Scala немного по другому (тем более, что это не ML язык, хоть хочет быть на него похож), поэтому для чистоты эксперемента не рассматриваем).
Только Хаскель использует разнообразные АТД везде (примерно так же, как и классы в Яве или С#), а OCaml, F#, SML в основном используют «примитивы» и «простые» АТД, в основном для контейнерности. В OCaml почти допилили модули, и они стали хорошей заменой объектам и АТД.
Так вот, категории — это очень удобный интрументарий работы с АТД в Хаскеле.
Так вот, категории — это очень удобный интрументарий работы с АТД в Хаскеле.
Тык, блин… Я же пытаюсь ответить сам для себя на вопрос: почему? В чём удобство-то? Иначе, я могу точно так же заявить:
Так вот, гомотопии — это очень удобный инструментарий работы с АТД в Хаскеле.
или
Так вот, топология Скотта — это очень удобный инструментарий работы с АТД в Хаскеле.
В чём именно удобство-то проявляется. Вот этого я не вижу. Единственное, что пока смог сам для себя вычислить (с Вашей, кажется, помощью), это то, что различные типы пытаются вводить вместе с операторами композиции. Ну да, я согласен, обычно о таком не думают при программировании. Но, возникает вопрос: и всё!? Потому что, этого явно мало.
Потому что, на самом деле, любой алгебраист-программист знает о полугруппах и знает, что удобно вводить ассоциативные операторы для объектов, если это возможно. Что, например, ассоциативная композиция конечных автоматов — это хорошо, потому что позволяет их формально строить по алгебраическим выражениям (получаем regexp-ы). И не надо думать о ТК или ещё о чём-то. Просто полугруппы — это хорошо, а группы — ещё лучше, если получается обратные отображения строить.
Но зачем для этого ТК? Где её теоремы в Haskell? Где естественные преобразования? Где пределы? Не используются? А если используются, то как помогают программировать?
Тык, блин… Я же пытаюсь ответить сам для себя на вопрос: почему? В чём удобство-то? Иначе, я могу точно так же заявить:
Так вот, гомотопии — это очень удобный инструментарий работы с АТД в Хаскеле.
или
Так вот, топология Скотта — это очень удобный инструментарий работы с АТД в Хаскеле.
В чём именно удобство-то проявляется. Вот этого я не вижу. Единственное, что пока смог сам для себя вычислить (с Вашей, кажется, помощью), это то, что различные типы пытаются вводить вместе с операторами композиции. Ну да, я согласен, обычно о таком не думают при программировании. Но, возникает вопрос: и всё!? Потому что, этого явно мало.
Потому что, на самом деле, любой алгебраист-программист знает о полугруппах и знает, что удобно вводить ассоциативные операторы для объектов, если это возможно. Что, например, ассоциативная композиция конечных автоматов — это хорошо, потому что позволяет их формально строить по алгебраическим выражениям (получаем regexp-ы). И не надо думать о ТК или ещё о чём-то. Просто полугруппы — это хорошо, а группы — ещё лучше, если получается обратные отображения строить.
Но зачем для этого ТК? Где её теоремы в Haskell? Где естественные преобразования? Где пределы? Не используются? А если используются, то как помогают программировать?
Так вот, гомотопии — это очень удобный инструментарий работы с АТД в Хаскеле.
И будете совершенно правы! =)
Насчет «где» — не все сразу. Рано или поздно автор подберется к ответам на эти вопросы. Высокоуровневая мотивация же была в самой первой статье.
Нарпимер, вот моя старая статья по этому поводу: Зачем нужны все эти функторы и монады?
Так понимаете, она точно такая же, как и все прочие статьи этого сорта. Возьмём Haskell, найдём в нём проблему. Затем решим эту проблему очень неоптимальным образом. Затем решим её при помощи функторов и монад более элегантно и объявим их универсальными супер-инструментами для всех программистов.
Но это снова не выглядит как универсальное объяснение. Я понимаю, зачем это всё в рамках Haskell. При чём, не как универсальный принцип, а просто как удобный pattern. Но зачем мне это всё вне рамок Haskell?
Я лучше возьму CSP (или pi-исчисление, или гомотопную теорию типов, в которой ТК — одна из многих описываемых структур) и буду писать намного более гибкие программы, в которых можно порождать не только структуры из монад в виде стеков, но вообще произвольные деревья из процессов, без всякого синтаксического сахара, а на основном языке.
Может я и не прав, может ТК и Haskell намного круче. Но это не видно из таких примеров. Нужно показать, как это всё работает с реальной, относительно сложной программой (например, Хоар показал, как при помощи CSP описывается операционная система). Из тех очень примитивных примеров, которые обычно приводятся для демонстрации «мощи» ТК, общая картинка не собирается в голове. В этом моя проблема восприятия.
Но это снова не выглядит как универсальное объяснение. Я понимаю, зачем это всё в рамках Haskell. При чём, не как универсальный принцип, а просто как удобный pattern. Но зачем мне это всё вне рамок Haskell?
Я лучше возьму CSP (или pi-исчисление, или гомотопную теорию типов, в которой ТК — одна из многих описываемых структур) и буду писать намного более гибкие программы, в которых можно порождать не только структуры из монад в виде стеков, но вообще произвольные деревья из процессов, без всякого синтаксического сахара, а на основном языке.
Может я и не прав, может ТК и Haskell намного круче. Но это не видно из таких примеров. Нужно показать, как это всё работает с реальной, относительно сложной программой (например, Хоар показал, как при помощи CSP описывается операционная система). Из тех очень примитивных примеров, которые обычно приводятся для демонстрации «мощи» ТК, общая картинка не собирается в голове. В этом моя проблема восприятия.
и буду писать намного более гибкие программы, в которых можно порождать не только структуры из монад в виде стеков, но вообще произвольные деревья из процессов, без всякого синтаксического сахара, а на основном языке.
нет, принципиально не сможете.
Как язык узнает, как работать с вашим произольным деревом?
Ибо стоит приципиальный вопрос — как можно работать с типом данных, который ещё не описан (пользовательским).
И ещё более важное — как зашить в язык инструментарий работы с типами данных, которые ещё не описаны.
Об этом я писал ещё ранее — Развитие пользовательских типов данных в программировании.
Собственно, категории (вернее тип-классы) — как раз такой инструментарий. Самый мощный из всех существующих.
нет, принципиально не сможете.
Как язык узнает, как работать с вашим произольным деревом?
Ибо стоит приципиальный вопрос — как можно работать с типом данных, который ещё не описан (пользовательским).
И ещё более важное — как зашить в язык инструментарий работы с типами данных, которые ещё не описаны.
Об этом я писал ещё ранее — Развитие пользовательских типов данных в программировании.
Собственно, категории (вернее тип-классы) — как раз такой инструментарий. Самый мощный из всех существующих.
В языке просто будут необходимые для этой работы примитивы. Точно так же, как в Haskell есть необходимые примитивы для описания типов. Просто вместо конструктора -> для типов функций у меня будут другие конструкторы, скажем, для процессов. Аксиомы и правила вывода типов можно не только для lambda-выражений придумать.
Типизированные lambda-выражения это самый примитивный Тьюринг-полный из возможных языков. И да, он достаточно мощный. Но является ли он самым удобным? Вот в чём вопрос. Вы утверждаете, что является, но убедительных доказательств пока не приведено.
И нет, теория категорий — это не самый мощный из существующих инструментов. Самый мощный из конструктивных — это гомотопическая (по мне так лучше переводить как «гомотопная», но доверюсь википедии) теория типов. Вы же не описали в своей статье Coq или Agda. А стоило бы.
Типизированные lambda-выражения это самый примитивный Тьюринг-полный из возможных языков. И да, он достаточно мощный. Но является ли он самым удобным? Вот в чём вопрос. Вы утверждаете, что является, но убедительных доказательств пока не приведено.
И нет, теория категорий — это не самый мощный из существующих инструментов. Самый мощный из конструктивных — это гомотопическая (по мне так лучше переводить как «гомотопная», но доверюсь википедии) теория типов. Вы же не описали в своей статье Coq или Agda. А стоило бы.
Типизированные lambda-выражения это самый примитивный Тьюринг-полный из возможных языков.
А как же нетипизированные lambda-выражения? :)
Вы не совсем поняли.
Вы должны в языке иметь возможность писать новые типы данных.
Вы должны в языке иметь возможность описать, как с этими типами данных работать — инструментарий по работе с новым типом данных.
И вы должны в языке иметь возможность иметь работать с этим, ещё не написанным инструментарием.
Теперь посмотрим на функцию:
Как видим, эта функция позволяет отфильтровать любую коллекцию, если она является MonadPlus, а так же существует функция критерия отфильтровки для типа данных.
Ей всё равно, что фильтровать дерево обезьян, или список товаров, или коллекцию картин.
Причём неважно, когда описаны эти обезьяны, товары и картины.
Функции также всё равно, когда будут описаны коллекции, списки или деревья.
Вы должны в языке иметь возможность писать новые типы данных.
Вы должны в языке иметь возможность описать, как с этими типами данных работать — инструментарий по работе с новым типом данных.
И вы должны в языке иметь возможность иметь работать с этим, ещё не написанным инструментарием.
Теперь посмотрим на функцию:
mfilter :: (MonadPlus m) => (a -> Bool) -> m a -> m a
mfilter p ma = do
a <- ma
if p a then return a else mzero
Как видим, эта функция позволяет отфильтровать любую коллекцию, если она является MonadPlus, а так же существует функция критерия отфильтровки для типа данных.
Ей всё равно, что фильтровать дерево обезьян, или список товаров, или коллекцию картин.
Причём неважно, когда описаны эти обезьяны, товары и картины.
Функции также всё равно, когда будут описаны коллекции, списки или деревья.
И что? Любой более или менее современный язык позволяет писать такие вот процедуры. Такое ощущение складывается, что Вы ни на чём, кроме Haskell, принципиально не программируете :)
И я же не о том, что в Haskell нельзя что-то сделать. Можно сделать всё, и это математический факт. Я о том, что в Haskell реализована некоторая, довольно простая, система типов. Не очевидно, что для практики именно такая система типов является самой удобной из всех других возможных.
Её удобство не только не доказано (что, вполне может быть, невозможно), но даже и не продемонстрировано (это я к вопросу о примерах из реального мира, я же много раз предлагал достаточно простые актуальные задачи, и на Хабре тоже, и просил привести решения на Haskell, но никто так и не написал ничего в ответ; правда в этот мой заход хотя бы разобрались с вариантом подхода к реализации IO без внешних библиотек).
Поэтому я и утверждаю, может быть, другая система типов, может оказаться более полезной для практики и более выразительной. Лично мне кажется, что такая система типов может произрастать из CSP. Потому что композиция процессов не только ассоциативна, но и коммутативна (может быть, это важно, а может быть и нет; просто все исследования зациклены на ТК и Haskell и по сторонам никто не смотрит, что печально).
И я же не о том, что в Haskell нельзя что-то сделать. Можно сделать всё, и это математический факт. Я о том, что в Haskell реализована некоторая, довольно простая, система типов. Не очевидно, что для практики именно такая система типов является самой удобной из всех других возможных.
Её удобство не только не доказано (что, вполне может быть, невозможно), но даже и не продемонстрировано (это я к вопросу о примерах из реального мира, я же много раз предлагал достаточно простые актуальные задачи, и на Хабре тоже, и просил привести решения на Haskell, но никто так и не написал ничего в ответ; правда в этот мой заход хотя бы разобрались с вариантом подхода к реализации IO без внешних библиотек).
Поэтому я и утверждаю, может быть, другая система типов, может оказаться более полезной для практики и более выразительной. Лично мне кажется, что такая система типов может произрастать из CSP. Потому что композиция процессов не только ассоциативна, но и коммутативна (может быть, это важно, а может быть и нет; просто все исследования зациклены на ТК и Haskell и по сторонам никто не смотрит, что печально).
А почему система типов хаскеля «довольно простая»?
Какое отношение имеет система типов к теории категорий, которую вы пытаетесь понять?
Что же касается «простоты» системы типов.
Вот λ-куб.
Если не считать языки с зависимыми типами данных (Coq, Agda), система типов в Хаскеле — самая «сложная», поскольку уже поддерживает типы, зависящие от типов.
Что же касается зависимых типов
1) Хаскель уже поддерживает такие в качестве дополнения LiquidHaskell
2) Эти типы достаточно капризные, и для нужд программирования слишком «безопасные». Пока не докажешь что-то, программу не запустишь.
Что же касается «простоты» системы типов.
Вот λ-куб.
Если не считать языки с зависимыми типами данных (Coq, Agda), система типов в Хаскеле — самая «сложная», поскольку уже поддерживает типы, зависящие от типов.
Что же касается зависимых типов
1) Хаскель уже поддерживает такие в качестве дополнения LiquidHaskell
2) Эти типы достаточно капризные, и для нужд программирования слишком «безопасные». Пока не докажешь что-то, программу не запустишь.
Но lambda-куб — это о типизированном lambda-исчислении. А если взять типизированное pi-исчисление? Или типизированные ASM?
Если построят типизированное пи-исчисление, сомневаюсь, что будет сильно отличаться от λ-куба.
Strong Normalisation in the π-Calculus на 41 странице показывает возможный вариант типизации, похожий на лямбда-куб (как утверждается в линейном случае).
Там однако, вводятся дополнительные правила, вроде аннигиляции и смешивания (в том числе и поляризационного) при выводе типов.
Ну и конечно же, никуда не деваются категории и ТК для пи-исчисления. Они всё те же.
Что касается CSP — это язык описания конкурентных систем, а не универсальных систем. ТК к ним так же применим.
Потому что ТК — «язык» взаимодействия систем.
Пусть развиваются все исчисления!
Strong Normalisation in the π-Calculus на 41 странице показывает возможный вариант типизации, похожий на лямбда-куб (как утверждается в линейном случае).
Там однако, вводятся дополнительные правила, вроде аннигиляции и смешивания (в том числе и поляризационного) при выводе типов.
Ну и конечно же, никуда не деваются категории и ТК для пи-исчисления. Они всё те же.
Что касается CSP — это язык описания конкурентных систем, а не универсальных систем. ТК к ним так же применим.
Потому что ТК — «язык» взаимодействия систем.
Пусть развиваются все исчисления!
Для ТК важно, чтобы были стрелки. Стрелки — это сущности у которых есть одно начало и один конец. Эта единственность и эта полная определённость важны.
Когда мы говорим о взаимодействующих системах процессов, то одно событие может привести к потенциально произвольному числу изменений. То есть, шаг вычисления не ведёт к получению определённого нового значения применением функции к предыдущему значению. То есть, вроде как, там нет хорошо определённых стрелок. Может быть, их можно определить. Надо изучать вопрос. Но, я не встречал построений.
Ничем похожим на State эту проблему не решить, потому что речь именно о неопределённости, как о важном и необходимом элементе для описания взаимодействий.
ТК — это не язык взаимодействия систем. ТК — это способ конструирования математических абстракций. Всё же взаимодействия — это нечто иное.
А про категории для pi-исчисления было бы интересно почитать.
Когда мы говорим о взаимодействующих системах процессов, то одно событие может привести к потенциально произвольному числу изменений. То есть, шаг вычисления не ведёт к получению определённого нового значения применением функции к предыдущему значению. То есть, вроде как, там нет хорошо определённых стрелок. Может быть, их можно определить. Надо изучать вопрос. Но, я не встречал построений.
Ничем похожим на State эту проблему не решить, потому что речь именно о неопределённости, как о важном и необходимом элементе для описания взаимодействий.
ТК — это не язык взаимодействия систем. ТК — это способ конструирования математических абстракций. Всё же взаимодействия — это нечто иное.
А про категории для pi-исчисления было бы интересно почитать.
Когда вы говорите о процессах, вы не можете говорить о «неопределённости», поскольку вы говорите о… процессах. «Неопределённость» — это всего лишь такой вид/тип процесса.
Раз так, то ТК применима и к пи-исчислению.
Strong normalization in the π-calculus with intersection and union types
На странице 4 хорошо расписана композиция.
Там же, а так же Free-Algebra Models for the π-Calculus неплохо сказано про моноиды.
Cartesian closed double categories, their lambda-notation, and the pi-calculus
тут вообще про n-категории
Раз так, то ТК применима и к пи-исчислению.
Strong normalization in the π-calculus with intersection and union types
На странице 4 хорошо расписана композиция.
Там же, а так же Free-Algebra Models for the π-Calculus неплохо сказано про моноиды.
Cartesian closed double categories, their lambda-notation, and the pi-calculus
тут вообще про n-категории
Когда вы говорите о процессах, вы не можете говорить о «неопределённости», поскольку вы говорите о… процессах. «Неопределённость» — это всего лишь такой вид/тип процесса.
Нет. Для однозначного указания процесса, как показал Хоар, в рамках CSP нам необходимо говорить о его неопределённости (он называет это divergence). Собственно, процесс однозначно задаётся неопределённостью и определённостью.
Раз так, то ТК применима и к пи-исчислению.
Strong normalization in the π-calculus with intersection and union types
На странице 4 хорошо расписана композиция.
Эмс? А разве ТК не должна оперировать композицией стрелок? Где там написано, что процессы это стрелки? И каковы объекты этой категории? Наличие просто оператора композиции ещё не делает алгебраическую систему категорией.
Там же, а так же Free-Algebra Models for the π-Calculus неплохо сказано про моноиды.
Моноиды — это просто модное название для полугрупп. Они традиционно используются для описания и анализа трасс процессов. К процессам применима теория трасс (это фактор-моноиды, построенные по коммутативному отношению).
Cartesian closed double categories, their lambda-notation, and the pi-calculus
тут вообще про n-категории
Ничего не могу сказать. Бегло просмотреть не вышло. Слишком уж заумно. Но это и вызывает сомнения. Неужели вот это всё проще и полезнее для программирования, чем обычная алгебра процессов? В статье всё рассматривается над категориями-произведениями… А это явное усложнение. Разве нет? Изначально же процессы простые, как прямая линия. Видимо, их приходится поднимать в двумерные пространства, чтобы где-то там «незаметно» протаскивать состояние.
Надо будет почитать. Спасибо за ссылку.
Но ещё раз повторю свой тезис: 1. Теория Категорий позволяет построить модель (некоторые свойства) любой вычислимой сущности. 2. Но возникает вопрос, позволяет ли она выразить саму эту сущность (мой вопрос о параллельном программировании)? 3. И если она позволяет, то делается ли это самым оптимальным образом?
Нет. Для однозначного указания процесса, как показал Хоар, в рамках CSP нам необходимо говорить о его неопределённости (он называет это divergence). Собственно, процесс однозначно задаётся неопределённостью и определённостью.
Раз так, то ТК применима и к пи-исчислению.
Strong normalization in the π-calculus with intersection and union types
На странице 4 хорошо расписана композиция.
Эмс? А разве ТК не должна оперировать композицией стрелок? Где там написано, что процессы это стрелки? И каковы объекты этой категории? Наличие просто оператора композиции ещё не делает алгебраическую систему категорией.
Там же, а так же Free-Algebra Models for the π-Calculus неплохо сказано про моноиды.
Моноиды — это просто модное название для полугрупп. Они традиционно используются для описания и анализа трасс процессов. К процессам применима теория трасс (это фактор-моноиды, построенные по коммутативному отношению).
Cartesian closed double categories, their lambda-notation, and the pi-calculus
тут вообще про n-категории
Ничего не могу сказать. Бегло просмотреть не вышло. Слишком уж заумно. Но это и вызывает сомнения. Неужели вот это всё проще и полезнее для программирования, чем обычная алгебра процессов? В статье всё рассматривается над категориями-произведениями… А это явное усложнение. Разве нет? Изначально же процессы простые, как прямая линия. Видимо, их приходится поднимать в двумерные пространства, чтобы где-то там «незаметно» протаскивать состояние.
Надо будет почитать. Спасибо за ссылку.
Но ещё раз повторю свой тезис: 1. Теория Категорий позволяет построить модель (некоторые свойства) любой вычислимой сущности. 2. Но возникает вопрос, позволяет ли она выразить саму эту сущность (мой вопрос о параллельном программировании)? 3. И если она позволяет, то делается ли это самым оптимальным образом?
Ещё раз напомню:
Тео́рия катего́рий — раздел математики, изучающий свойства отношений между математическими объектами, не зависящие от внутренней структуры объектов.
ТК всё равно, моноиды ли это чисел, функций или процессов.
Наличие просто оператора композиции ещё не делает алгебраическую систему категорией.
Конечно же делает.
n-категори, кстати, говорит, что композиция — это слишком обще, и можно иметь ортогональную и линейную композиции (для дублирующих категорий).
На счёт ваших тезисов:
1) Не думаю, что можно любую модель. В конце-концов, из кубиков Ж, О, П и А никак слово СЧАСТЬЕ не сложишь, используя или не используя ТК ))
Попробуем сузить — если можно построить такую модель, то можно и с помощью ТК.
2) Не совсем понятно, что вы имели в виду. Если понимается, что можно ли с помощью категорий найти такие, с какими удобно человеку работать — то возможно.
В конце концов, люди увидели Линзы (объектоподобные структуры с едиными геттерами и сеттерами) в следующем
3) Когда вы спрашиваете, находит ли ТК путь оптимальным способом, вы имеете в виду, что ТК находит лишь 1 путь. Но нет, ТК может дать много путей к решению задач, в том числе и очень сложным путём.
Есть ли среди них оптимальный? Возможно да, но не гарантированно.
Тео́рия катего́рий — раздел математики, изучающий свойства отношений между математическими объектами, не зависящие от внутренней структуры объектов.
ТК всё равно, моноиды ли это чисел, функций или процессов.
Наличие просто оператора композиции ещё не делает алгебраическую систему категорией.
Конечно же делает.
n-категори, кстати, говорит, что композиция — это слишком обще, и можно иметь ортогональную и линейную композиции (для дублирующих категорий).
На счёт ваших тезисов:
1) Не думаю, что можно любую модель. В конце-концов, из кубиков Ж, О, П и А никак слово СЧАСТЬЕ не сложишь, используя или не используя ТК ))
Попробуем сузить — если можно построить такую модель, то можно и с помощью ТК.
2) Не совсем понятно, что вы имели в виду. Если понимается, что можно ли с помощью категорий найти такие, с какими удобно человеку работать — то возможно.
В конце концов, люди увидели Линзы (объектоподобные структуры с едиными геттерами и сеттерами) в следующем
type Lens' a b = forall f . (Functor f) => (b -> f b) -> (a -> f a)
3) Когда вы спрашиваете, находит ли ТК путь оптимальным способом, вы имеете в виду, что ТК находит лишь 1 путь. Но нет, ТК может дать много путей к решению задач, в том числе и очень сложным путём.
Есть ли среди них оптимальный? Возможно да, но не гарантированно.
Ещё раз напомню:
Тео́рия катего́рий — раздел математики, изучающий свойства отношений между математическими объектами, не зависящие от внутренней структуры объектов.
ТК всё равно, моноиды ли это чисел, функций или процессов.
Так это-то и смущает в первую очередь. С точки зрения ТК моноид — это один объект A и куча стрелок A → A. И что дальше может ТК сказать о таком объекте? Всё, что сказано, сказано без превличения ТК: автоматы, полугруппы, трассы, те же процессы. Совершенно не понятно, как ТК помогла бы вывести регулярные языки и автоматы из такого определения (кстати, было бы очень интересно и об этом почитать). То есть, более практические размышления проводятся совсем на другом уровне (мне так представляется).
Вы, конечно, скажете, что вот, можно рассматривать 2-категории, ..., n-категории и так далее. И это более интересные объекты. Но тогда возникнет вопрос, а чем это всё будет полезнее для практики? Какой метод ТК мы сможем применить к таким построениям над моноидами, чтобы, допустим, додуматься до тех же автоматов? Чем это лучше n-группоидов?
Наличие просто оператора композиции ещё не делает алгебраическую систему категорией.
Конечно же делает.
n-категори, кстати, говорит, что композиция — это слишком обще, и можно иметь ортогональную и линейную композиции (для дублирующих категорий).
Ну, собственно, у нас и получится моноид из такой композиции. А дальше? Что с этим делать?
1. Любую вычислительную сущность можно. Потому что ТК проникла в информатику именно как модель для типизированного lambda-исчисления. Если мы верим в тезис Чёрча-Тьюринга, то мы должны верить, что ТК позволяет смоделировать любую вычислимую сущность. Однако, вопрос в том, является модель самой этой сущностью, и не заложено ли в самой сущности больше возможностей, чем в модели.
2. То, что гордо называется Линзами в Haskell, давным давно применяют для реализации ООП в чистом ФП. Об этом даже в SICP написано. Было бы интересно не то, что Линзы есть, а то размышление в терминах ТК, которое привело к тому, что Линзы появились.
А то всё выглядит так: одни люди придумали, потом пришли другие люди, просто написали для этого всего красивую сигнатуру, объявили это всё категорией, и присвоили изобретение себе.
Вот Вы можете продемонстрировать как из задачи о необходимости иметь ООП с состояниями возникает такая вот формулировка для Линзы, при помощи рассуждений в терминах ТК? Было бы интересно.
3. Хм… Но нам же предлагают «программисты, учите ТК для обретения просветления и истины».
Тео́рия катего́рий — раздел математики, изучающий свойства отношений между математическими объектами, не зависящие от внутренней структуры объектов.
ТК всё равно, моноиды ли это чисел, функций или процессов.
Так это-то и смущает в первую очередь. С точки зрения ТК моноид — это один объект A и куча стрелок A → A. И что дальше может ТК сказать о таком объекте? Всё, что сказано, сказано без превличения ТК: автоматы, полугруппы, трассы, те же процессы. Совершенно не понятно, как ТК помогла бы вывести регулярные языки и автоматы из такого определения (кстати, было бы очень интересно и об этом почитать). То есть, более практические размышления проводятся совсем на другом уровне (мне так представляется).
Вы, конечно, скажете, что вот, можно рассматривать 2-категории, ..., n-категории и так далее. И это более интересные объекты. Но тогда возникнет вопрос, а чем это всё будет полезнее для практики? Какой метод ТК мы сможем применить к таким построениям над моноидами, чтобы, допустим, додуматься до тех же автоматов? Чем это лучше n-группоидов?
Наличие просто оператора композиции ещё не делает алгебраическую систему категорией.
Конечно же делает.
n-категори, кстати, говорит, что композиция — это слишком обще, и можно иметь ортогональную и линейную композиции (для дублирующих категорий).
Ну, собственно, у нас и получится моноид из такой композиции. А дальше? Что с этим делать?
1. Любую вычислительную сущность можно. Потому что ТК проникла в информатику именно как модель для типизированного lambda-исчисления. Если мы верим в тезис Чёрча-Тьюринга, то мы должны верить, что ТК позволяет смоделировать любую вычислимую сущность. Однако, вопрос в том, является модель самой этой сущностью, и не заложено ли в самой сущности больше возможностей, чем в модели.
2. То, что гордо называется Линзами в Haskell, давным давно применяют для реализации ООП в чистом ФП. Об этом даже в SICP написано. Было бы интересно не то, что Линзы есть, а то размышление в терминах ТК, которое привело к тому, что Линзы появились.
А то всё выглядит так: одни люди придумали, потом пришли другие люди, просто написали для этого всего красивую сигнатуру, объявили это всё категорией, и присвоили изобретение себе.
Вот Вы можете продемонстрировать как из задачи о необходимости иметь ООП с состояниями возникает такая вот формулировка для Линзы, при помощи рассуждений в терминах ТК? Было бы интересно.
3. Хм… Но нам же предлагают «программисты, учите ТК для обретения просветления и истины».
Потому что ТК проникла в информатику именно как модель для типизированного lambda-исчисления.
Эээ… Языки ML не используют ТК и при этом являются типизированными.
С точки зрения ТК моноид — это один объект A и куча стрелок A → A.
С точки зрения ТК, моноид — это такая вещь, которую можно ассоциативно соединять, и кроме того, существует «Ничего», такое, что при соединении с моноидом как справа, так и слева не меняет сам моноид.
Совершенно не понятно, как ТК помогла бы вывести регулярные языки и автоматы из такого определения
Если вас интересуют конечные автоматы — тогда вам необходимы комонады.
Собственно, язык комонад — это конечные автоматы.
Можете глянуть, например, Evaluating cellular automata is comonadic
Но тогда возникнет вопрос, а чем это всё [моноиды] будет полезнее для практики?
Возьмём, например, функцию свёртки:
И всем хороша, но вот второй параметр — начальное значение очень сильно нервирует.
Поэтому специально для них написали дополнительную функцию — по сути для ненулевых списков, в качестве начального значения берётся 1й этап свёртки.
но, стало небезопасно.
Ко всему прочему достаточно скучно каждый раз писать КАК сворачивать (то бишь первый аргумент).
В конце-концов, хаскелисты совсем обленились, и захотели свёртку не только списков, а чего угодно.
Вот и добавился новый тип-класс в библиотеку. Теперь свёртка — одно загляденье!
То есть если есть что-либо сворачиваемое (например, списки, массивы), и хранятся в них моноиды — функция их сворачивает до одного значения.
Правда, необходимо было дать большую свободу программистам, поэтому можно вначале преобразовать данные в моноиды, а далее — всё будет делаться само:
Как мы видим, если у нас есть функция foldr (в данном случае — это обобщённый foldr), и сворачивать надо моноиды — это делается самостоятельно, без помощи программиста.
Однако, вопрос в том, является модель самой этой сущностью, и не заложено ли в самой сущности больше возможностей, чем в модели.
Является ли система связей синапсов мозга самой сущностью, или в этой модели больше возможностей, чем заложено? )))
То, что гордо называется Линзами в Haskell, давным давно применяют для реализации ООП в чистом ФП.
Ссылку пожалуйста. В каких таких «чистых ФП» языках применяют?
Объект — это состояния + функции. Но в чистых ФП языках невозможно иметь состояния, ибо данные неизменны.
Вот Вы можете продемонстрировать как из задачи о необходимости иметь ООП с состояниями возникает такая вот формулировка для Линзы, при помощи рассуждений в терминах ТК? Было бы интересно.
В своё время были уже написаны библиотеки, где для записей были созданы удобные геттеры, сеттеры и модификаторы.
Гений линз в том, что нашёлся человек, который сказал, что геттеры, сеттеры и модифиакторы — это одно и то же — собственно, линза.
Эээ… Языки ML не используют ТК и при этом являются типизированными.
С точки зрения ТК моноид — это один объект A и куча стрелок A → A.
С точки зрения ТК, моноид — это такая вещь, которую можно ассоциативно соединять, и кроме того, существует «Ничего», такое, что при соединении с моноидом как справа, так и слева не меняет сам моноид.
Совершенно не понятно, как ТК помогла бы вывести регулярные языки и автоматы из такого определения
Если вас интересуют конечные автоматы — тогда вам необходимы комонады.
Собственно, язык комонад — это конечные автоматы.
Можете глянуть, например, Evaluating cellular automata is comonadic
Но тогда возникнет вопрос, а чем это всё [моноиды] будет полезнее для практики?
Возьмём, например, функцию свёртки:
foldr :: (a -> b -> b) -> b -> [a] -> b
foldr k z [] = z
foldr k z (y:ys) = y `k` foldr k z ys
И всем хороша, но вот второй параметр — начальное значение очень сильно нервирует.
Поэтому специально для них написали дополнительную функцию — по сути для ненулевых списков, в качестве начального значения берётся 1й этап свёртки.
foldr1 :: (a -> a -> a) -> [a] -> a
foldr1 f (x:xs) = foldr f (f x) xs
foldr1 _ [] = errorEmptyList "foldr1"
но, стало небезопасно.
Ко всему прочему достаточно скучно каждый раз писать КАК сворачивать (то бишь первый аргумент).
В конце-концов, хаскелисты совсем обленились, и захотели свёртку не только списков, а чего угодно.
Вот и добавился новый тип-класс в библиотеку. Теперь свёртка — одно загляденье!
fold :: (Foldable t, Monoid m) => t m -> m
То есть если есть что-либо сворачиваемое (например, списки, массивы), и хранятся в них моноиды — функция их сворачивает до одного значения.
Правда, необходимо было дать большую свободу программистам, поэтому можно вначале преобразовать данные в моноиды, а далее — всё будет делаться само:
fold :: (Foldable t, Monoid m) => t m -> m
fold = foldMap id
foldMap :: (Foldable t, Monoid m) => (a -> m) -> t a -> m
foldMap f = foldr (mappend . f) mempty
Как мы видим, если у нас есть функция foldr (в данном случае — это обобщённый foldr), и сворачивать надо моноиды — это делается самостоятельно, без помощи программиста.
Однако, вопрос в том, является модель самой этой сущностью, и не заложено ли в самой сущности больше возможностей, чем в модели.
Является ли система связей синапсов мозга самой сущностью, или в этой модели больше возможностей, чем заложено? )))
То, что гордо называется Линзами в Haskell, давным давно применяют для реализации ООП в чистом ФП.
Ссылку пожалуйста. В каких таких «чистых ФП» языках применяют?
Объект — это состояния + функции. Но в чистых ФП языках невозможно иметь состояния, ибо данные неизменны.
Вот Вы можете продемонстрировать как из задачи о необходимости иметь ООП с состояниями возникает такая вот формулировка для Линзы, при помощи рассуждений в терминах ТК? Было бы интересно.
В своё время были уже написаны библиотеки, где для записей были созданы удобные геттеры, сеттеры и модификаторы.
Гений линз в том, что нашёлся человек, который сказал, что геттеры, сеттеры и модифиакторы — это одно и то же — собственно, линза.
Эээ… Языки ML не используют ТК и при этом являются типизированными.
В каком смысле «не используют»? Любой тип в них можно описать той или иной категорией.
С точки зрения ТК, моноид — это такая вещь, которую можно ассоциативно соединять, и кроме того, существует «Ничего», такое, что при соединении с моноидом как справа, так и слева не меняет сам моноид.
Моноид? Соединять? С чем? Вот есть у меня обычный моноид строк. С чем его можно соединить?
Мой вопрос был не о пользе моноидов. Моноиды, несомненно, полезны, как абстракция для ассоциативных операций, которые позволяют рассуждать о многом, например, о параллельных алгоритмах для тех же конечных автоматов.
Мой вопрос был о пользе размышления над моноидами в терминах ТК. Какие выводы позволяет сделать ТК о свойствах моноидов? В частности, мне интересно, позволяет ли ТК своими формальными методами пройти к концепции конечного автомата для распознавания регулярных языков.
Если вас интересуют конечные автоматы — тогда вам необходимы комонады.
Собственно, язык комонад — это конечные автоматы.
Можете глянуть, например, Evaluating cellular automata is comonadic
Тут просто реализовано нечто в виде комонад (даже на самом деле не понятно, автоматы ли, единственное автоматное свойство: это возможность отыскать подходящую конечную подстроку в любой позиции). Интересно было почитать, спасибо.
Но, снова, это не то, что меня интересует. Я же спрашивал: хорошо, вот мы описали моноид в виде категории. Что нам дальше с этим делать? Как нам прийти к концепции вот этой автоматной комонады, рассуждая в терминах ТК? Ну, что-то типа такого: «сели мы, почесли репу, увидели, что у нас тут этакий морфизм и функтор, а вот там у нас такая хитрая стрелка, хопа! Так это же распознавание регулярных языков за линейное время!»
Ссылку пожалуйста. В каких таких «чистых ФП» языках применяют?
Объект — это состояния + функции. Но в чистых ФП языках невозможно иметь состояния, ибо данные неизменны.
Design Concepts in Programming Languages, Раздел 7.3. Ещё можно почитать Типы в Языках Программирования, раздел 20.1. В котором объекты описаны как расширения процессов :) Сколько авторов, столько и мнений.
Так, блин! Собственно же по этому и вопрос: почему ТК лучше других подходов-то? Что можно с ТК такого делать, чего нельзя делать в других подходах?
В каком смысле «не используют»? Любой тип в них можно описать той или иной категорией.
С точки зрения ТК, моноид — это такая вещь, которую можно ассоциативно соединять, и кроме того, существует «Ничего», такое, что при соединении с моноидом как справа, так и слева не меняет сам моноид.
Моноид? Соединять? С чем? Вот есть у меня обычный моноид строк. С чем его можно соединить?
Но тогда возникнет вопрос, а чем это всё [моноиды] будет полезнее для практики?
Возьмём, например, функцию свёртки:
Мой вопрос был не о пользе моноидов. Моноиды, несомненно, полезны, как абстракция для ассоциативных операций, которые позволяют рассуждать о многом, например, о параллельных алгоритмах для тех же конечных автоматов.
Мой вопрос был о пользе размышления над моноидами в терминах ТК. Какие выводы позволяет сделать ТК о свойствах моноидов? В частности, мне интересно, позволяет ли ТК своими формальными методами пройти к концепции конечного автомата для распознавания регулярных языков.
Если вас интересуют конечные автоматы — тогда вам необходимы комонады.
Собственно, язык комонад — это конечные автоматы.
Можете глянуть, например, Evaluating cellular automata is comonadic
Тут просто реализовано нечто в виде комонад (даже на самом деле не понятно, автоматы ли, единственное автоматное свойство: это возможность отыскать подходящую конечную подстроку в любой позиции). Интересно было почитать, спасибо.
Но, снова, это не то, что меня интересует. Я же спрашивал: хорошо, вот мы описали моноид в виде категории. Что нам дальше с этим делать? Как нам прийти к концепции вот этой автоматной комонады, рассуждая в терминах ТК? Ну, что-то типа такого: «сели мы, почесли репу, увидели, что у нас тут этакий морфизм и функтор, а вот там у нас такая хитрая стрелка, хопа! Так это же распознавание регулярных языков за линейное время!»
Ссылку пожалуйста. В каких таких «чистых ФП» языках применяют?
Объект — это состояния + функции. Но в чистых ФП языках невозможно иметь состояния, ибо данные неизменны.
Design Concepts in Programming Languages, Раздел 7.3. Ещё можно почитать Типы в Языках Программирования, раздел 20.1. В котором объекты описаны как расширения процессов :) Сколько авторов, столько и мнений.
Так, блин! Собственно же по этому и вопрос: почему ТК лучше других подходов-то? Что можно с ТК такого делать, чего нельзя делать в других подходах?
Я же спрашивал: хорошо, вот мы описали моноид в виде категории.
Вы почему-то путаете причину со следствием.
Это всё равно, что заявлять «пусть мы описали ноль в виде числа».
Моноид — это термин ТК. Вы не можете не расуждать о моноидах вне контекста ТК.
Если вы говорите «моноид», вы уже используете ТК. Если вы говорите «композиция», то вы уже используете ТК.
Пусть у нас есть строки и конкатенация — @
Если да, то строки — это моноид.
Пусть у нас списки и есть конкатенация — ++.
Если да, то списки — моноиды.
Так вот, в Хаскеле вы можете использовать эти свойства, в дальнешем работая только с моноидами, а не конкретными типами:
И после этого писать:
Где использовать? Например, я дал пример fold, которая сворачивает любые моноидо-содеращие данные в свёртываемых коллекциях.
Как нам прийти к концепции вот этой автоматной комонады, рассуждая в терминах ТК?
ТК не отменяет необходимость мышления. Так же рассуждать надо. Распознаёте паттерн — «да ведь это функтор/моноид/...!» и меняете на этот самый функтор/моноид/…
Что можно с ТК такого делать, чего нельзя делать в других подходах?
я уже говорил — его основной плюс в универальности подходов.
Если мы делаем аналогию с клеями — это универальные клеи, типа Момента. Можете пользоваться специализированными клеями, а можете Моментом.
Вы почему-то путаете причину со следствием.
Это всё равно, что заявлять «пусть мы описали ноль в виде числа».
Моноид — это термин ТК. Вы не можете не расуждать о моноидах вне контекста ТК.
Если вы говорите «моноид», вы уже используете ТК. Если вы говорите «композиция», то вы уже используете ТК.
Пусть у нас есть строки и конкатенация — @
("ABC" @ "DEF") @ "HIJ" ?== "ABC" @ ("DEF" @ "HIJ")
"ABC" @ "" ?== "ABC"
"" @ "ABC" ?== "ABC"
Если да, то строки — это моноид.
Пусть у нас списки и есть конкатенация — ++.
([1,2,3] ++ [4,5,6]) ++ [7,8,9] ?== [1,2,3] ++ ([4,5,6] ++ [7,8,9])
[1,2,3] ++ [] ?== [1,2,3]
[] ++ [1,2,3] ?== [1,2,3]
Если да, то списки — моноиды.
Так вот, в Хаскеле вы можете использовать эти свойства, в дальнешем работая только с моноидами, а не конкретными типами:
instance Monoid String where
mempty = ""
mconcat = (@)
instance Monoid [a] where
mempty = []
mconcat = (++)
И после этого писать:
("ABC" `mconcat` "DEF") `mconcat` "HIJ" ===
"ABC" `mconcat` ("DEF" `mconcat` "HIJ")
"ABC" `mconcat` mempty === "ABC"
mempty `mconcat` "ABC" === "ABC"
([1,2,3] `mconcat` [4,5,6]) `mconcat` [7,8,9] ===
[1,2,3] `mconcat` ([4,5,6] `mconcat` [7,8,9])
[1,2,3] `mconcat` mempty ?== [1,2,3]
mempty `mconcat` [1,2,3] ?== [1,2,3]
Где использовать? Например, я дал пример fold, которая сворачивает любые моноидо-содеращие данные в свёртываемых коллекциях.
Как нам прийти к концепции вот этой автоматной комонады, рассуждая в терминах ТК?
ТК не отменяет необходимость мышления. Так же рассуждать надо. Распознаёте паттерн — «да ведь это функтор/моноид/...!» и меняете на этот самый функтор/моноид/…
Что можно с ТК такого делать, чего нельзя делать в других подходах?
я уже говорил — его основной плюс в универальности подходов.
Если мы делаем аналогию с клеями — это универальные клеи, типа Момента. Можете пользоваться специализированными клеями, а можете Моментом.
А вот здесь не занимаются ли товарищи переизобретением моноидов?
Да, похоже трансдюсеры — это моноиды для свёрток (foldMap). Очень вероятно.
А редьюсеры — это точно свёртки Foldable.
А редьюсеры — это точно свёртки Foldable.
А в чём собственно изобретательство? Это давным давно известные паттерны. В том же параллельном программирование вовсю используются такие подходы уже лет 30. В Clojure просто реализация.
Пост в ЖЖ на эту тему
Вы почему-то путаете причину со следствием.
Это всё равно, что заявлять «пусть мы описали ноль в виде числа».
Моноид — это термин ТК. Вы не можете не расуждать о моноидах вне контекста ТК.
Если вы говорите «моноид», вы уже используете ТК. Если вы говорите «композиция», то вы уже используете ТК.
Но, позвольте, ноль — это не всегда число (и даже чаще в современных вычислениях совсем не число, как минимум матрица). Поэтому Ваша метафора не очень понятна. Ну да ладно…
Смущает другое. То есть, если я назову моноид полугруппой с 1, а вместо композиции стану употреблять термин «умножение», то я выйду из области рассуждений в рамках ТК? Так получается? Но, ведь, все свойства сохранятся. И я спокойно могу реализовать интерфейсы, которые называются Semigroup или, допустим Reduceable, или ещё какие-то, с другими названиями, но суть свою сохраняющими.
Получается, что ТК — это чисто номинальная вещь? Но это же странно. Потому что, вроде как, в самой ТК есть некие интересные теоремы. Или вот та же лемма Йонеды. Они никак не используются? Получается, что вся ТК в Haskell — это просто использование терминологии? Типам, мы такие элитные, что вместо «интерфейс» будем говорить «категория»? Но это пижонство. Вряд ли дело именно так обстоит.
я уже говорил — его основной плюс в универальности подходов.
Если мы делаем аналогию с клеями — это универальные клеи, типа Момента. Можете пользоваться специализированными клеями, а можете Моментом.
Эх… Мне кажется, Вы увлекаетесь метафорами. Давайте говорить не о клее, а о математических и информационных сущностях всё же. Просто, если делаются заявления об универсальности, то их надо как-то подкреплять. Потому что в этом месте возникает идея: а что может быть универсальнее подхода, используемого в Си (я о чистом Си) и Unix?
Типа, а давайте данные закатывать в буферы памяти и файлы, а потом все могут с ними делать всё, что угодно. Что угодно можно приклеить куда угодно, и это даже будет как-то работать благодаря аппаратной защите памяти. Разве это не наивысшее воплощение универсальности?
Но такой подход принято в сообществе Haskell критиковать. Значит, дело всё же, в чём то другом.
Я вот пока для себя такие выводы сделал.
1. ТК полезна тем, что заставляет Haskell-истов конструировать абстракции в монадном стиле. Типа, с монадой ты — крутой чувак, а без монады с тобой даже говорить не будут. И это позволяет накручивать функциональность определённой структуры достаточно легко. Но это не собственно сама ТК, из ТК тут название. Такое ощущение.
2. ТК полезна тем, что позволяет при описании объектов не закладываться на их внутреннюю структуру, а оперировать структурой внешней, выраженной через стрелки. Это, действительно, представляется важным. И воспалённый разум рисует картинку с точками, к которым постепенно навешиваются свойства, которые могли быть заранее в структуре этих точек не учтены. Это даёт гибкость.
Но опять же во многих языках примерно так и конструируются объекты. Концепция интерфейсов в чистом виде. Просто, получается, что в Haskell это сделано наиболее аккуратно и лаконично. Хорошо. Но… Собственно, чем тогда призыв изучать TK отличается от призыва проектировать «от интерфейса» и изучать pattern-ы?
Ладно. Так или иначе. Спасибо за пищу для размышлений.
Это всё равно, что заявлять «пусть мы описали ноль в виде числа».
Моноид — это термин ТК. Вы не можете не расуждать о моноидах вне контекста ТК.
Если вы говорите «моноид», вы уже используете ТК. Если вы говорите «композиция», то вы уже используете ТК.
Но, позвольте, ноль — это не всегда число (и даже чаще в современных вычислениях совсем не число, как минимум матрица). Поэтому Ваша метафора не очень понятна. Ну да ладно…
Смущает другое. То есть, если я назову моноид полугруппой с 1, а вместо композиции стану употреблять термин «умножение», то я выйду из области рассуждений в рамках ТК? Так получается? Но, ведь, все свойства сохранятся. И я спокойно могу реализовать интерфейсы, которые называются Semigroup или, допустим Reduceable, или ещё какие-то, с другими названиями, но суть свою сохраняющими.
Получается, что ТК — это чисто номинальная вещь? Но это же странно. Потому что, вроде как, в самой ТК есть некие интересные теоремы. Или вот та же лемма Йонеды. Они никак не используются? Получается, что вся ТК в Haskell — это просто использование терминологии? Типам, мы такие элитные, что вместо «интерфейс» будем говорить «категория»? Но это пижонство. Вряд ли дело именно так обстоит.
я уже говорил — его основной плюс в универальности подходов.
Если мы делаем аналогию с клеями — это универальные клеи, типа Момента. Можете пользоваться специализированными клеями, а можете Моментом.
Эх… Мне кажется, Вы увлекаетесь метафорами. Давайте говорить не о клее, а о математических и информационных сущностях всё же. Просто, если делаются заявления об универсальности, то их надо как-то подкреплять. Потому что в этом месте возникает идея: а что может быть универсальнее подхода, используемого в Си (я о чистом Си) и Unix?
Типа, а давайте данные закатывать в буферы памяти и файлы, а потом все могут с ними делать всё, что угодно. Что угодно можно приклеить куда угодно, и это даже будет как-то работать благодаря аппаратной защите памяти. Разве это не наивысшее воплощение универсальности?
Но такой подход принято в сообществе Haskell критиковать. Значит, дело всё же, в чём то другом.
Я вот пока для себя такие выводы сделал.
1. ТК полезна тем, что заставляет Haskell-истов конструировать абстракции в монадном стиле. Типа, с монадой ты — крутой чувак, а без монады с тобой даже говорить не будут. И это позволяет накручивать функциональность определённой структуры достаточно легко. Но это не собственно сама ТК, из ТК тут название. Такое ощущение.
2. ТК полезна тем, что позволяет при описании объектов не закладываться на их внутреннюю структуру, а оперировать структурой внешней, выраженной через стрелки. Это, действительно, представляется важным. И воспалённый разум рисует картинку с точками, к которым постепенно навешиваются свойства, которые могли быть заранее в структуре этих точек не учтены. Это даёт гибкость.
Но опять же во многих языках примерно так и конструируются объекты. Концепция интерфейсов в чистом виде. Просто, получается, что в Haskell это сделано наиболее аккуратно и лаконично. Хорошо. Но… Собственно, чем тогда призыв изучать TK отличается от призыва проектировать «от интерфейса» и изучать pattern-ы?
Ладно. Так или иначе. Спасибо за пищу для размышлений.
Получается, что ТК — это чисто номинальная вещь?
Не стоит передёргивать. Я сказал, что если вы неандерталец с топором, то вы просто не увидите чисел.
Но они есть и их свойства остаются в силе.
Моноиды, полугруппы,… — это всё термины ТК.
Давайте говорить не о клее, а о математических и информационных сущностях всё же. Просто, если делаются заявления об универсальности, то их надо как-то подкреплять.
Это не я говорю, а математика, а именно ТК.
Универсальнее Си только Ассемблер )))
2. ТК полезна тем, что позволяет при описании объектов не закладываться на их внутреннюю структуру, а оперировать структурой внешней, выраженной через стрелки.
Да, совершенно точно.
Собственно, чем тогда призыв изучать TK отличается от призыва проектировать «от интерфейса» и изучать pattern-ы?
1) Паттерны проектирования никто не отменял. Правда, много этих паттернов не имеют смысла в Хаскеле. Тем не менее, такой паттерн как MCV никто не отменял там.
3) Паттерны построены на основе постоянного опыта и специфике лёгкости изменений. Паттерны всегда отлично смотрятся для больших проектов. Даже, если они на Хаскеле.
Не стоит передёргивать. Я сказал, что если вы неандерталец с топором, то вы просто не увидите чисел.
Но они есть и их свойства остаются в силе.
Моноиды, полугруппы,… — это всё термины ТК.
Давайте говорить не о клее, а о математических и информационных сущностях всё же. Просто, если делаются заявления об универсальности, то их надо как-то подкреплять.
Это не я говорю, а математика, а именно ТК.
Универсальнее Си только Ассемблер )))
2. ТК полезна тем, что позволяет при описании объектов не закладываться на их внутреннюю структуру, а оперировать структурой внешней, выраженной через стрелки.
Да, совершенно точно.
Собственно, чем тогда призыв изучать TK отличается от призыва проектировать «от интерфейса» и изучать pattern-ы?
1) Паттерны проектирования никто не отменял. Правда, много этих паттернов не имеют смысла в Хаскеле. Тем не менее, такой паттерн как MCV никто не отменял там.
3) Паттерны построены на основе постоянного опыта и специфике лёгкости изменений. Паттерны всегда отлично смотрятся для больших проектов. Даже, если они на Хаскеле.
Справедливости ради, простое типизированное лямбда-исчисление в общем случае не полно по Тьюрингу.
Чистая функция, которая возвращает блок
Это, кажется, опечатка.
О, я просто напишу несколько строк кода и посмотрю, что происходитИменно так зачастую и бывает. Особенно, если в программе ошибка, а где именно — непонятно.
По поводу примера с факториалом.
Могу утверждать, что PHP не хуже:
Хотя пример от переводчика уже поинтереснее.
А в целом, автор обещал рассказать о теории категорий, а рассказывает о Haskell и как он крут по сравнению с c++.
Могу утверждать, что PHP не хуже:
function fact(n) { return gmp_fact(n) }
Хотя пример от переводчика уже поинтереснее.
А в целом, автор обещал рассказать о теории категорий, а рассказывает о Haskell и как он крут по сравнению с c++.
Зарегистрируйтесь на Хабре, чтобы оставить комментарий
Типы и функции