Комментарии 70
типы появились, как минимальная абстракция, позволяющая формализовать процесс вычислений
Не стоит забывать об очень мощном влиянии практиков на развитие информационных технологий. В частности, именно практики сочинили ассемблер, потом фортран, потом си. В ассемблере были просто регистры, а в регистрах - байты, биты, слова. И все эти единицы хранения информации уже являлись типизированными. Просто жизнь заставила - например, в машине регистры принимают только семибитные значения, и хоть ты тресни, данные другого типа туда не засунешь.
С другой стороны, автор понимает сложность объяснений, связанную с излишне завышенным уровнем абстракции:
Типичный математический текст начинается со знакомства со "взятой с
потолка" абстракцией, и потом рассматриваются её "удивительной красоты"
свойства
Но он поставил себе цель донести до общества очередную "удивительную красоту", только теперь выражающуюся в использовании в разработке софта так называемого "функционального" подхода. Да, функциональные языки в своей основе имеют реально много математики, и потому для полноценного понимания действительно необходимо как-то свести вместе высокие абстракции и прикладные повседневные задачи (то есть практику).
К сожалению, в статье присутствует несколько завышенное внимание к абстракциям, своим введением отталкивающее практиков, а так же искажающее реальность в части удовлетворения потребностей практиков. Практика отодвинула функциональные языки на задний план эволюционного развития, освободив место более простым процедурным подходам. Это не значит, что функциональный подход бесперспективен, даже наоборот, математически мыслящее сообщество функциональных разработчиков вносит гораздо больший вклад в развитие языков именно гораздо более тщательной проработкой теории. Только в статье для практиков (каковых здесь большинство, как и во всех остальных слоях общества), было бы неплохо учитывать их интересы более явным образом.
Например - можно приводить практически полезные решения на процедурных языках, сравнивая их с аналогами из функционального множества. Да и примеры стоит вводить гораздо раньше, и именно с упором на их полезность для практики.
Хотя сама возможность вполне простого отображения алгоритма, записанного на функциональном языке, на алгоритм, записанный процедурно, говорит нам о большой сложности задачи популяризации функционального подхода из-за неочевидности его преимуществ. Поэтому не возьмусь как-то умалять труд автора, хотя замечу, что до идеала ему ещё совсем неблизко.
регистрах - байты, биты, слова. И все эти единицы хранения информации уже являлись типизированными
Не являлись. Если я по-невнимательности положу в регистр AX сумму в рублях, а в BX другую сумму в долларах, то ассемблер не помешает мне их сложить друг с другом и получить бредовый результат.
Первыми практиками были выдающиеся математики, спроектировавшие языки Ассемблера, Фортран и прочие. На ранних этапах типизация байтов была весьма условной - там скорее речь шла именно о множествах возможных значений а не о возможностях, которые предоставляет тип. Представление чисел с плавающей запятой появилось позднее. Понятие о типах, в появилось в математике задолго до первых ЭВМ.
Мотивом статьи было не столько снижение "сложности объяснения завышенного уровня абстракций", сколько объяснение неизбежности появления этих абстракций. Проблема в том, что обычно математики предоставляют уже готовую "красоту", не особо утруждаясь обоснованием. А потом практики смотрят на это с мыслями вроде "красиво, но нафига, а главное, зачем это мне?". Не считаю, что с поставленной перед собой задачей справился "на отлично", но всё же постарался донести, что в следствие неизбежности появления, эти абстракции являются фундаментом в том числе и в области обеспечения корректности компьютерных программ любых алгоритмов (да, теорию множеств и сейчас развивают в этом плане, но это дальше от программирования и там всё оказывается намного сложнее).
Популярность императивного (процедурного, если угодно) программирования обуславливается в первую очередь историей развития электронно-вычислительной техники. Первые языки программирования строились вокруг архитектуры процессоров. Тогдашние компиляторы просто не тянули абстракции, далёкие от железа. Для популярных тогда языков писалось множество книг, курсов обучения семинаров. Разрабатывались и популяризировались императивно-ориентированные техники программирования. Позднее появилось ООП, в пропаганду которого также влиты гигантские деньги... Но популярность, на самом деле, слабо коррелирует с качеством этих методов. Сейчас компьютеры и компиляторы сильно поумнели, функциональная парадигма стала весьма актуальной, но преодолевать огромную инерцию общественного мнения всё тяжело. Тем не менее, тенденции на изменение мира к лучшему прослеживается везде - в публикациях, в развитии языков программирования и т.п. Без относительно того, замечают ли это сами программисты))
Вообще, такую холиварную тему, как преимущества ФП, наверное, имеет смысл осветить в отдельной статье (угу, ещё одной на эту тему...). Если подумать, то фундаментальный набор абстракций, необходимых для качественного программирования гораздо меньше, чем всё то, чему сейчас традиционно учат в школах/вузах. А научить человека писать качественные программы в традиционной парадигме сложнее, чем в функциональной. Впрочем, данная статья не столько про ФП, сколько про фундаментальность фундамента ФП)))
Безусловно, автору есть многое, над чем нужно поработать. Прошу не судить слишком строго - это мой первый опыт публикации статьи. Большое спасибо за отзыв!
Вы, наверное на scala пишите, если выбрали её для демонстрации примеров. Сколько раз не пытался, так и не смог писать на Скале в функциональном стиле, такое ощущение, словно язык сопротивляется тому, чтобы код был функциональным и пытается вынудить писать в императивно-оопшном стиле. Когда пишу на Хаскеле или Racket(типизированный Лисп) такого не возникает.
Возможно это связано с тем, что в скале постоянно используются джавовые либы, и при использовании их API неизбежно приходится городить ООП.
Да, последнее время больше пишу на Scala. У языка не мало проблем, по большей части из-за "беттерджавного" наследства. Но в нём сочетаются как традиционные для большинства популярных языков решения, так местами весьма глубокие ФП-шные вкусности. Так что несмотря не некоторые недоработки в плане ФП, мне кажется, он здорово подходит для демонстрации кода в подобных статьях.
Какое-то время назад попробовал в реальном проекте Tagless Final в экосистеме cats и остался доволен - ООП вынесена куда-то на периферию, а про опасную "нечистую" императивность вообще практически можно было забыть))
На всяких Haskel мало кто хочет писать продуктовый софт, а Scala приносит не только боль))
Довольно голословное утверждение.
Ну так это чисто субъективный взгляд автора. Как по мне, таких как вы таки на сегодня мало. И даже скорее не потому, что никто не хочет, а вот представим, что я хочу — но это автоматически означает, что мне нужно не просто самому научиться, но и научить команду, а это уже совсем другие требования. И экспертов-то мало, а экспертов готовых научить (и умеющих) — еще меньше. Их и по скале-то кот наплакал.
если в ваших приложениях это полезно, то и на скале писать, конечно, выгоднее, а иначе… ну хз :]
Ну да, у нас во все API — это JVM, ну или по большей части они, и что получается, когда Scala или даже Java заменяют хотя бы на Python — я прекрасно вижу каждый день. Если в том же спарке для питона сделали специальную обертку — то еще как-то можно жить, если забыли — то это тоже боль. Потому что совместимости нету. Ну вот авторы спарка в очередной версии 3.4 обещали, что переделают весь API, так чтобы его можно было дергать из Go, например — то есть, не из JVM языков, может у нас что-то и изменится (когда оная 3.4 до нас доедет).
Первыми практиками были выдающиеся математики, спроектировавшие языки Ассемблера, Фортран и прочие.
Например, в википедии авторство ассемблера приписывают двум авторам, выпустившим книгу с описанием раннего прототипа ассемблера в 1947 году. Один из авторов по образованию математик, но второй - инженер электрик. Кто из них двигал идею упрощения работы при кодировании программ? Как вы думаете?
Сама по себе идея сделать так, что бы писать было проще, становится очевидной любому, кто должен был писать что-то сложное, особенно в машинных кодах. Напрашивающаяся мысль о замене цифровых кодов буквенными обозначениями, хоть немного похожими на слова, просnо обязана была прийти в голову в первую очередь именно практикам. Ну а отсутствие в такой подстановке каких-либо существенных математических идей подсказывает нам, что математикам такая идея в голову просто не должна попасть, ибо зачем вносить в математику "изобретения" уровня 2+2=4?
Аналогичная история была и с фортраном, и с си, и со многими другими языками.
Хотя функциональный подход, соглашусь, был заимствован прямо из математики. И здесь авторство легко доказуемо, если мы сравним даты появления лямбда-исчисления с датами появления функциональных языков. Но какие даты вы бы предложили сравнить в случае с ассемблером и тому подобными малыми (но вносящими много удобств) изменениями теории языков программирования?
Мотивом статьи было не столько снижение "сложности объяснения завышенного уровня абстракций", сколько объяснение неизбежности появления этих абстракций.
Вообще, стоит указывать конкретику. Если речь идёт о типах, то это один подход, идущий своими корнями в древнюю грецию, а может и много дальше, то есть в те времена, когда люди впервые пришли к понятию классификации, то есть разделения наблюдаемых явлений на группы по сходству тех или иных признаков. Соответственно, "неизбежность" здесь несколько натянутая - разве можно подумать, что кто-то осмысленно (то есть мы не говорим об откровенных идиотах) отказался бы от накопленных тысячелетиями примеров полезного применения инструмента с названием "классификация"?
Если же речь идёт о функциональном подходе, то неизбежность пока что не случилась. Как было упомянуто ранее, лёгкость отображения алгоритмов на много способов их формальной записи, не предполагает лёгкой победы одного из подходов, даже если за ним стоит авторитет математиков. Для победы нужно нечто большее - реальное и заметное без микроскопа облегчение работы по созданию программ.
Ассемблер создавался, чтобы была возможность записать программу не в виде дырок на перфокарте, а текстом. С прицелом на кроссплатформенность. Семантика языка целиком определялась архитектурой тогдашних процессоров, которые проектировались ведущими учёными. Впрочем, это был по-прежнему язык для пенетрации перфокарт, а не для консольного ввода.
Фортран, Алгол уже создавались по заказу целыми комитетами, куда входили так же самые достойные учёные. Все остальные языки уже шли по их стопам и не особо отступали от первоначальных конструктов.
Деление людей на практиков и "тех, других" вообще кажется не совсем корректным))
Типы - это вполне конкретная абстракция)) Не так важно, кто их придумал, как то, что начиная с определённого периода они начинают изучаться и использоваться повсеместно. Те определения которые лежат в основе теории типов появились вследствие накопившегося объёма проблем, для решения которого старые абстракции не работали, или были неудобны. Именно это я и называю "неизбежностью".
И ещё одна ремарка))
Эволюция ФП следует за математикой. А вот традиционное императивное (процедурное, объектно-ориентированное...) программирование - это уже законченные идеи. Они очень вяло мутируют исключительно за счёт впитывания ФП-шных техник.
Императивное программирование выросло из железа и следует за ним. Базовые концепции присутствуют со времен первых компьютеров: вычисления на последовательных шагах (тактах) и изменяемые переменные (регистры, ячейки памяти). Более близкий пример: в семантике языка C запечатлены свойства PDP-11 (C Is Not a Low-Level Language). Объектно-ориентированное, процедурное и даже фундаментальное структурное программирование — это просто способы ограниченным человеческим мозгам ворочать все большим количеством тех же самых элементарных инструкций. Новые подходы в теории типов позволяют выразить в коде более сложные утверждения, инварианты решаемой задачи. ООП и даже элементы ФП в императивных языках не позволяют выразить больше, чем уже можно было выразить машинным кодом — лишь помогают человеку не сделать ошибку при записи. Новых базовых концепций долго не было, соответственно, не было эволюции в том же смысле, что у теории типов, то есть, чтобы стало можно решать принципиально больше задач. Настоящее развитие императивного программирования — квантовые вычисления, поскольку элементная база не позволяет иметь, как минимум, классические переменные. Глядя в обратную сторону, до появления компьютеров "железом" была голова, которой тяжело делать шаги не последовательно, и записи, которые можно править.
Пример - расширяемые типы. Они введены в ряд процедурных языков под названием generics. Назовите аналог в лямбда-исчислении.
Это всё к тому, что разделение на концепции (типы и функциональный подход, то есть два разных направления) показывает нам, что практики не во всём были дурнее паровоза.
Лямбда-исчисление тоже не стоит на месте. Обобщённые типы - это отображения из типа в тип, то бишь функции, что вполне укладываются в лямбда-исчисление. Вообще - это тема моего следующего проекта для хабра))
Ни в коем случае не стараюсь как-нибудь принизить "практиков", кого бы Вы не имели ввиду))
Я наверное что то не понимаю, но о каких типах в лямбда исчислении может идти речь? Ведь лямбда исчисление создавалось, как "математика без множеств", а значит и без типов.
Создавалось-то оно как бестиповое, но типы в нём появились достаточно скоро. Лямбда-выражения в современных языках построены именно на типизированном лямбда-исчислении.
Вода и канцеляриты в ваших комментариях как из диплома от "искусственного интеллекта". Сделать, что ли, в своём расширении для хабра возможность пометок "WARNING: царь автор ненастоящий". Даже если автор изначально мясной, но балуется, то ему же хуже. Читать беседы ботов я не хочу.
Извините, но вот
Но к сожалению, такого рода утверждения не будут считаться полными и однозначными определениями. В нашем случае, мы должны ещё гарантировать, что нет никаких
,
и прочих, кто ещё связан отображениями с
.
Почему они не могут считаться полными, и что нам дает отсутствие или наличие еще An... ?
Но с другой стороны, например, если для
есть отображение в
, то
вполне можно исключить из определения типа
почему мы можем исключить ?? на основании чего ? а если при приобразовании у нас потеря точности ?
Зачастую такие отображения бывает удобно отобразить на диаграмме в виде ориентированного графа
Это про все виды отображений или про некоторые виды, отображений? если про некоторые, тогда стрелки в обратную сторону в случае сюръекции не возможны (или возможны) ?
Тут речь идёт об однозначности формулировки типа. Вопрос в том, какой тип мы можеи назвать "А1 или А2". Или же не получится выделить какой-то единстаенный тип, подходящий под эту формулировку?
Понятие универсального свойста позволяет однозначно формулировать новые типы. В этой статье подобные вопросы раскрываются очень хорошо, на мой взгляд.
Стрелки-то можно нарисовать какие угодно, но в теории типов принято ассоциировать такие стрелки с конеретными функциями, принимающие аргумент одгого типа и возвращающие значение другого типа (отображение между типами). Т.е. буквально, если у вас есть функция из А в В (написанная только что, или например, неявное преобразование к сурертипу от компиляьора...), то вы можете соединить на диаграмме эти типы стрелкой в соответствующем нарравлении.
Я же правильно понимаю, что если допустим имеем 2 исходника source-1 source-2 (допустим C)
оба содержат по структуре в которых имена полей разные, но их кол-во и типы полей совпадают, а так же их последовательность
пример
struct A {
int a;
int b;
}
struct B {
int c;
int d;
}Компилятор С как знаем обращается к полям не по имени, а по смещению
то тогда верно утверждать что это один и тот же тип ?
Типы изоморфные (при слабой типизации всегда можно переломать указатель с одного типа на другой и обратно без потерь), но разные. С этими типами могут быть связанные разные наборы функций, а типы как раз и отличаются разным набором входящих и исходящих отображений - положением на общей диаграмме типов.
Формулирование типов через универсальные свойства (уникальные кратчайшие пути) помогает факторизовать вычисления - декомпозировать сложные задачи на простые и описать их с помощью типов.
Я дико извиняюсь, но можно как-то разжевать для обычных смертных, что значит
формулирование типов через уникальные свойства ?
как проявляется помощь в факторизации вычислений ?
что за фактор ?
о каких сложных задачах идет речь? те что в jira или те что доказательство P = NP ?
что значить описать с помощью типов? пример бы глянуть, о чем речь.
Я смутно догадываюсь о чем речь, но смутно
Про сумму типов
Вот не плохо бы разжевать, есть другое более наглядное объяснение в рамках Scala - это Either, можно сказать Either это такой enum
enum Either[A,B] {
Left(A),
Right(B)
}
// или Scala2
sealed trait Either[A,B]
case class Left[A,B](a:A) extends Either
case class Right[A,B](b:B) extends Eitherи дать например ссылку сюда https://github.com/anton-k/ru-neophyte-guide-to-scala/blob/master/src/p07-either.md
Что в конечном итоге Left/Right - это тип (.class) внутри JVM и к некой переменной a типа Either, применима операция instanceOf, а match - это сахар над instanceOf.
Что важно, что переменная a не может одновременно содержать Left и Right. Но, при этом сохраняется информация о типе, что Either переменную можно определить Left/Right - и извлечь ее и с ней работать, зная что она Left.
Тут важно еще пояснить, зачем это знать, просто в Scala - world, точнее в части ее библиотек не принято кидать Exception, и большинство функций используют такую семантику:
// было
def some_fun( arg: A ): R
// стало
def some_fun( arg: A ): Either[Error,R]Что обычно в Left хранятся ошибки и это знание важно, а вот не просто, так нам захотелось ввести Left/Right
Важный момент. Наверное стоило раскрыть его подробнее.
Вычисления обычно проводяься так: на входе у нас есть значение типа А (возможно, несколько значерий, объединённых типом-произведением), передав его в одну функцию, получаем значение типа В и так далее. Получаетя цепочка вида А->В->...->R - по сути это один из путей на диагрмме типов. Задача состоит в том, чтобы найти путь до R как можно короче.
Допустим есть три функции А->В, В->С и А->С. Очевидно, что если мы хотим получить значение типа С из А, то вызов последней функции будет оптимальнее, чем последоаптельный вызов пнрвых двух - путь на диаграмме короче. Уникальность универсального морфизма и определяет его оптимальность - из всех возможных путей он оказыаается самым коротким. Строя вычисления, основанные на универсальных свойствах типов как раз и получается находить наиболее коротеие пути вычислений.
Под факторизацией здесь понимается разделение длинного пути вычисления на отдельные шаги-функции. По сути, декомпощиция задачи. Возможно, не самое удачное использование слова "факторизация"...
По поводу типа Either я в статье отметил, что не зотел углублятся в тему обобщённых типов - что это и почему их можно захотеть. Надеюсь написать об этом отдельную статью, и её публикация окажется достаточно обоснованной))
Я вот про ту самую цепь A->B->C, в целом понятно, что чем короче путь - тем "лучше"
Просто у меня может не правильное понимание, допустим есть такие функции
def a( value:Long ):Int = value % 10
def b( value:Int ):String = value.toString
val result = b(a(10))def c( value:Long ):String = value.toStringФормально с - это короткий путь из Long в String, но его результат очевидно не совпадает с композицией b * a
Я тут сознательно нарушаю, я так понимаю правильнее всего говорить не о буквальной трактовке типов, а о таких типах которые при вычислении значений не дают отличий ?
В теории хороший компилятор пометил бы результат композиции b * a - как некий тип String* (со звездочкой, а-ля зависимый тип) и данный тип не был эквивалентен типу из результата функции c.
Или рассуждения не верны ?
Другой вопрос, всякий раз когда я смотрю на диаграмму суммы типов
всегда мучает вопрос, а при чем тут D ?
ну хорошо, есть у нас такие пути
1) A -- ia -> A+B -- u --> D
2) A -- f --> D
вроде как короче, A+B получается тогда - как пятое колесо телеге, может сразу из A в D, и выкинуть из проекта A+B ?
A+B - это вроде важный концепт и выкидывать его не хочется
Что хотел сказать автор этим ? или я читаю не глазами, а жо---ой
Формально я понимаю, что запись в языке `def f( a: A | B )` - короче, чем воротить свои велосипеды с sealed + case class
Другое так же понимаю, что def f( a: A & A ) формально это def f( a: A )
По простой причине некий тип A обладает теми же методами, что и A
А вот тип A & B - по сути обладает методами и свойствами обоих типов одновременно, интересно другое
допустим A имеет метод def f( a : Int ) = a % 10,
а тип B имеет такой же метод, но с другой реализацией def f( a: Int ) = a % 16
тогда вызов a.f( 13 ) - какая в итоге будет вызвана реализация - это на откуп компилятору отдается.
Если сумму типов рассматривать как множественное наследование, тогда как-то легче в голове уложить.
Обзор и так получился гигантским. Очень много деталей оказалось за бортом. Для тех, кто заинтересуется, оставлены лишь прямые ссылки, или намёки для загугливания.
Многие понятия были сформулированы ещё в теории типов раньше, чем на её основе появилась теория категорий. Тут лишь хотелось бы подчеркнуть, что понятие универсального свойства автоматически следует из желания чётко сформулировать, что такое типы "А и В", "А или В" и другие. Без чёткой формулировки мы не сможем оперировать этими понятиями, чтобы конструктивно доказывать корректность алгоритма.
С множественным наследованием та же беда, что и с пересечением типов в Scala. Чтобы как-то обеспечить предсказуемость поведения нужно идти на какие-то компромиссы, гвоздями прибивать какие-то дополнительные правила к спецификации языка...
"Сторонние" типы в формулировании универсальных свойств нужны как раз для того, чтобы как-то определить способ, как из них выброать самый оптимальный - универсальный.
Спасибо за комментарий
Я же правильно понимаю, что множественное наследование - это та самая приславутая проблема алмаза, и что она успешно решается в рамках С3 линириализации https://ru.wikipedia.org/wiki/C3-линеаризация ?
Я к той же Scala, где в Scala 2 до умножения типов (A & B & C) использовали подход class SomeClass extends A with B with C ?
Типы в этой схеме фиксированы, но тут играет роль понятие коммутативности путей. В данном случае пути "c" и "b * а" не коммутативны - не для всех исходных значений будет получен одинаковый результат. "Коммутативность" входит и в понятие универсального свойства - "существует единственный морфизм, делающий диаграмму коммутативной".
Мне кажется, автор достаточно удачно провёл границу между тем, что включить в статью, а что оставить за рамками. Предложенные Вами примеры сами по себе неплохие, но, на мой взгляд, не очень вписываются в стиль статьи. В частности, instanceOf, перекос (bias) Either, исключения - это низкоуровневые детали реализации, несущественные с точки зрения рассматриваемых понятий.
Потрясающая статья.
Спасибо за проделанную работу!
Статья очень интересная, но очень непонятная. Видимо, рассчитана не на новичков. Постоянно при чтении возникают вопросы:
нам требуется дополнительная структура над множествами - набор функций позволяющий "уменьшать количество" элементов списка вплоть до единственного. Такая структура называется "моноид".
Абстрактный моноид обычно описывается так:
ассоциативная бинарная операция
У вас написано сначала, что «моноид» это набор функций, но дальше в определении вы пишете «[одна] бинарная операция». Противоречие.
В самом деле, если есть возможности моноида (бинарная операция и нейтральный элемент) инструкции не меняются, если в качестве множества мы выбираем int, double или string - описание алгоритма остаётся тем же (но потребуются другие реализации моноида).
Как можно в алгоритме заменить int на string и получить тот же алгоритм? 2 + 2 = 4, но "2" + "2" = "22". Было бы хорошо, если бы вы привели пример в статье.
Суть типа полностью определяется совокупностью отображений, связывающих его с другими типами (не только с типами, но это пока не важно))). Зачастую такие отображения бывает удобно отобразить на диаграмме в виде ориентированного графа:
Я не понимаю, что на этом графе является узлами и что обозначают ребра. Узлы - это типы (вроде Int, String), а ребра - функции, которые преобразуют их (вроде strlen(), которая преобразует String в Int)? А где тут тогда функции, принимающие несколько аргументов? Было бы хорошо, если бы вы объяснили, как строится такой граф и привели пример графа для простого алгоритма.
с другой стороны, если у нас есть объект типа C, то у нас есть (мы можем получить) объекты типов B_1 и B_2.
Можем ли мы определить тип C, как ... "B_1 и B_2"?
Я не вижу тут логики. Вот у нас есть тип String, мы из него можем получить Int (длина строки) и Bool (является ли строка пустой), тогда по вашей логике, String это «Int и Bool»? Очевидно же, что нет.
Но с другой стороны, например, если для A_1 есть отображение в A_2, то A_2 вполне можно исключить из определения типа C. Аналогично, среди типов B также могут найтись те, кто связан с отображениями, значит там тоже кого-то можно исключить из формулировки C через произведения.
Здесь просто непонятно ничего. Что значит «связан с отображениями»? Что значит «из формулировки C через произведения». Слово «произведения», конечно, вызывает в памяти product types, но в статье до этого момента про них ни слова.
Нам нужно выбрать "наилучшего" универсального представителя - нам нужно некое универсальное свойство.
Что значит «универсальный представитель»? По какому критерию он «наилучший»? Что за свойство имеется в виду?
"Единственность" функции, идущей от одного типа к другому, означает эквивалентность всех функции связывающих эти типы в том же направлении.
Я не понимаю, если у нас функция одна и единственная, то откуда взялись «все функции, связывающие эти типы»?
Существует тип и единственная функция принимающая (или возвращающая) значения этого типа, такая что соответствующая диаграмма будет коммутативной.
Что значит «соответствующая диаграмма»? Диаграмма всех типов и функций в программе? И зачем нужно условие про диаграмму, если у нас есть только одна функция, возвращающая значения типа? Где тут возьмутся «разные пути» (из определения коммутативности), если стрелка к этому типу только одна?
Вооружившись понятием универсального свойства, попробуем определить новый тип как "A или B". В математике это обычно называют суммой типов.
Вы бы привели пример из какого-нибудь известного языка, а то так непонятно, что это значит.
Для любых типа D и функций f и g существует единственный (с точностью до изоморфизма) тип A+B и единственная функция u, делающие диаграмму коммутативной.
Я не очень понимаю, если у нас есть функции f и g, преобразующие A и B в D, то зачем нам тип A + B? Он выглядит как лишнее звено. И еще не понимаю, как будет выглядеть диаграмма, если A и B это один и тот же тип, например, Int.
Для любых типа D и функций f и g существует единственный (с точностью до изоморфизма) тип A\times B
У вас на диаграмме C вместо D...
Если мы формулируем какое-то универсальное свойство, то мы автоматически получаем и дуальное ему.
Было бы неплохо объяснить с простыми примерами, что значит дуальность. Я встречал это слово в нескольких местах (например, в схемах логических элементов на CMOS-транзисторах), но тут это явно что-то другое.
Но сперва давайте рассмотрим те же самые типы, но с другой точки зрения. Переобозначим конструкторы типа B i_1 и i_2 п проекторы типа A p_1 и p_2, получая A=B\times B.
А нельзя ли тут было привести простой пример с типами вроде Int? Пусть A это Int. Тогда B = A + A = A × 2 это структура из Int и, допустим, Bool, а по формуле A = B×B, получается Int = структура из 2 таких структур? Что-то в голове не укладывается.
Каррирование
Не понимаю, что хорошего в каррировании? В чем смысл представления функции из N аргументов в виде N функций от 1 аргумента? Только усложняется все, по моему. Также, непонятно, как с помощью каррирования можно представить функцию с необязательными аргументами или именованными аргументами.
Также, каррирование позволяет зафиксировать первый аргумент функции, но не позволяет зафиксировать последний:
val div = (a) => (b) => a/b
val div10 = div(10) // Зафиксировали 1-й аргумент
var divBy2 = ??? // а как зафиксировать второй?
Нелогично, согласитесь?
Я бы заменил каррирование на фиксирование произвольных аргументов:
val div = (a, b) => a/b
val divBy2 = div(?, 2)
Вот так гораздо удобнее и логичнее, чем с вашим каррированием.
Такой тип-одиночка называется единицей
В чем смысл использовать тип, у которого единственное значение? Не проще ли вообще ничего не передавать в функцию тогда?
A × 0 = 0
Непонятно, как это интерпретировать. Структура из 2 полей, где первое имеет тип A, а второе?
У вас написано сначала, что «моноид» это набор функций, но дальше в определении вы пишете «[одна] бинарная операция». Противоречие.
Одна функция — это тоже набор функций. Попробуйте мыслить чуть абстрактнее.
Как можно в алгоритме заменить int на string и получить тот же алгоритм? 2 + 2 = 4, но "2" + "2" = "22".
Тут две части алгоритма. Одна часть — это функция "суммирования", что бы это ни означало. Она "складывает" два аргумента, и она разумеется является разной для строк и целых, и она специфична для каждого типа. Другая часть — это функция высшего порядка, которая может работать с разными функциями "суммирования" (смысл у которых может быть достаточно разный, поэтому обычно это называют более общим термином свертка), при условии, что они удовлетворяют некоторым свойствам. Пример тут очень простой — функция высшего порядка fold/foldr/reduce и многие другие названия, потому что такие функции существуют во множестве языков.
То что вы многое не поняли — вполне естественно, статья довольно сложная и не для новичков.
Уровень статьи выше "начального", но далёк от "сложного"))
Бинарную операцию в моноиде можно трактовать как функцию из пары значений (ну или в каррированном виде). С другой стороны, нейтральный элемент можно понимать как нулярную операцию, не принимающую аргументов типов А - функция из типа единицы. Итого, моноид - это пара функций. Ловкость рук и никакого мошенничества))
Алгоритм определяется прежде всего своей сигантурой. Например, на входе список типа А, а на выходе значение типа А. Если мы ничего не знаем про тип А, но на предоставили моноид для типа А, то мы можем свернуть этот список. При разных типах и разных моноидах результат будет, конечно, разный, но сам алгоритм свёртки списка не измениться. Попробуйте сами написать такой алгоритм, например, с циклом foreach (на входе список тип А и моноид для него, а на выходе значение типа А) - алгоритм не будет зависеть от того, что именно пониматься под А.
Несколько аргументов на вход функции - это кортеж - произведение типов, которое также отображается на диаграмме типов. А значит там есть место и для функции от нескольких переменных.
По поводу заморочек с универсальным свойствами - часть ответов есть в самой статье, а за подробностями обычно предлагаю перейти по этой ссылке.
Про каррирование тоже можно отдельную статью написать)). Обычно используется в тех случаях, когда какая функция требует на вход функцию меньшего числа аргументов, чем у нас есть, а первый аргумент можно фиксировать. Иногда сразу опеределяют функции в каррированном виде, а в других случаях можно воспользоваться методами, уже реализованными в стандартной библиотеке языка. В статье подчёркивается сам факт наличия такого изоморфизма. А примеров применения его в интернете не мало (боюсь у меня сейчас не найдётся возможности написать что-нибудь прямо в этом ответе((( )
Метод без параметров эквивалентен функции из единицы. Просто в теории типов речь всегда идёт о функциях одного аргумента (даже если это кортеж).
В статье говорится не о равенстве типов (А, Nothing) и Nothing, а об их изоморфизме - значения обоих типов невозможно получить честным (чистым) способом.
Статья по стилю и оформлению хорошая. Но уверен, разбив её на несколько статей - было-бы правильней. Но всё равно - спасибо.
Многие вопросы по теме затронули предыдущие комментаторы. Хотел-бы со своей стороны маленькую деталь спросить.
Например
Int32вполне можно считать подтипом дляInt64, но ни о каком наследовании тут нет речи. Наследование выстраивает типы в иерархическую структуру, но подтипизация в этом плане гораздо гибче.
Подтипом считать можно, но такого понятия как подтип в языках ведь не существует и на этот манер под такой подтип можно и bool занести. Он вообще наверное по вашим критериям основа всех типов?
И гибкость подтипов - не совсем понял, какая практическая польза от этой 'гибкости' типов? Но видать статью надо попробовать ещё раз пройти.
Спасибо за отзыв! Хотел, разбить статью, но не получилось - каждый раздел получается незаконченным, оторванным от основной темы.. Видимо, опыта пока малоато))
Понятие подипизации есть в разных языках, но в каждом оно может иметь какие-то отличительные особенности. Где-то вполне допускается неявное привеление от bool к int (0 или 1), а в других языках - нет.
"Гибкость" подтипищации упомянута в сравнении с наследованием, которое часто путают с подтипищацией. Подтипищация проявлятся как наличие неявного преобразования от одного типа к другому. Во многих языках мы можем сами создаватьнеявные преобразования (гибкость)) - иерархия наследования нас не ограничивает.
Я в своем pet-proj делал для себя компилятор, так чтоб всегда вычислялись типы конечного выражения и в рамках вычисления проводил проверку на совместимость типов
в качестве совместимости я определил одну бинарную функцию isAssignable( left: Type, right: Type ) : bool, в Scalа она выглядила так leftSomeType.isAssignable( rightType )
при помощи нее строил граф отношений (частично упорядоченное множество на базе упомянутой функции) в рамках области видимости импортируемых типов
isAssignable включала как и отношения наследования, так и не явных преобразований из Int в Long
Правильно ли я понимаю что речь именно о этом ? что это и есть случай под-типизации ?
Знаком с математической логикой и теорий категорий. Где-то на индексных типах понимание текста утратилось полностью. Думаю для человека, который видит это впервые, будет совершенно не понятно. Предлагаю эксперимент: напишите 5-6 задач на понимание "вашей теории типов" и сделайте опрос, кто сколько решил.
Где-то на индексных типах
Все совпадения названий с "книжными" совершенно случайны!))
Кажется, что контекстуальный смысл слова "индекс" раскрыт в статье, разве нет?
В любом случае, тут я не раскрываю "свою теорию типов". Как и было упомянуто в начале, это лишь поверхностный обзор основных понятий теории. А за деталями лучше обращаться к специализированной литературе. Мною допущено много вольностей в изложении, но если есть принципиальные ошибки, которые могут ввести читателя в заблуждение - буду рад их исправить.
Насколько я понял статья рассматривает "Теорию типов" как некую всем известную теорию, неужели никто не поинтересуется кто же является автором этой всем известной теории, в каком году появились первые упоминания этой теории, неужели никому не интересно?
Неужели никто не обратит внимания на то что определения в виде:
Тип - это не более чем некая метка, приписываемая к каждому терму (переменной, выражению и т.п.)
Никак не достаточно чтобы основать какую либо теорию!
Это придуманное, фактически, взятое с потолка определение на котором, оказывается, можно построить целую теорию.
Поражает конечно не это, поражает уровень аудитории которая на полном серьезе воспринимает такой откровенный наукообразный бред.
Вы же можете прочитать здесь и то что пропагандирует эта статья:
Итак, мы получили язык для вычисления без каких либо ограничений.
...
Не знаю, для чего может быть полезна эта картинка, но впечатляет!
Неужели никого не смущает что "Теория" нашла "язык без ограничений" для области применения ВНЕ смысла или смыслов.
Я согласен: потрясающая статья!
Не нужно воспринимать эту статью как некое научное откровение. Это именно что популярный поверхностный обзор известных положений теории типов. Уверен, что у аудитории достаточно высокий уровень, чтобы именно в таком ключе воспринимать эту работу. После прочтения у читателя может возникнуть много вопросов, на некоторые пробую ответить сам, ответы на другие несложно найти в свободном доступе.
Это именно что популярный поверхностный обзор известных положений теории типов
Тогда вы начинаете противоречить самому себе. Ранее вы утверждали, что хотели показать неизбежность применения теории типов в программировании. Теперь - это уже просто обзор.
Со своей стороны соглашусь с комментаторами, которые указывают на сложность понимания статьи. Если внимательно вчитываться, да ещё пользоваться дополнительными источниками, тогда можно понять о чём речь. Но терпение заканчивается и далее статья просто пролистывается до комментариев.
Задайте себе следующие вопросы:
Кто ваша целевая аудитория?
Как много представителей такой аудитории на популярном околоайтишном ресурсе?
Сколь сильна мотивация тех, кто всё же соответствует пересечению множеств "целевая аудитория" и "аудитория ресурса"?
Сколько человек из полученного пересечения смогут выдержать напряжённое чтение с постоянным отвлечение на дополнительные источники информации?
Сколько из способных выдержать плюнут на всё и получат информацию из более подробно излагающих тему материалов?
Надеюсь, в следующий раз вы поменяете способ изложения.
А про мотивацию добавлю, что она есть следствие понимания нужности и важности темы для читающего. Но именно пояснению полезности вы и не уделили внимания, а это стоило начать делать с первых же строк. Пример вам уже приводили - покажите преимущество подхода в сравнении с альтернативой.
Среди законов Мёрфи есть такой: "Если есть хоть один шанс, что вас поймут неправильно, то вас ОБЯЗАЕЛЬНО поймут неправильно"))
Никаких противоречий в своих словах не вижу. В этой статье не излагался какой-либо "подход", полезность которого осталась не раскрытой. Это именно фрагментарный обзор (местами сложной) теории, без глубоких деталей. С акцентом на не раз уже упомянутую в комментариях "неизбежность", естественность появления представленных абстракций.
Представленный материал интересен мне самому, я верю что найдутся читатели, с кем я смогу разделить эти интересы. Да, такой формат и стиль изложения может понравиться не всем, но, как говорится, всем не угодишь... Важным показателем для меня являются оценки под статьёй и комментарии читателей, в том числе и Ваш. Постараюсь учесть все мнения при подготовке следующей статьи.
я как раз воспринимаю эту статью как не-научное откровение, как поверхостный обзор придуманных положений несуществующей теории.
Статья демонстрирует не просто высокий уровень наукообразной демагогии, по моему это, определенно, талант!
Можете ответить на вопрос когда, где и кем была сформулирована "Теория типов"?
или
какой смысл проводить
популярный поверхностный обзор известных положений теории
если они известны?
Кстати, словосочетание "популярный поверхностный обзор" вполне можно использовать как определение "демагогии", как мне кажется.
В компьютере восьми-байтовая ячейка памяти может хранить в себе значения как из множества
Int64, так и изdouble- эти множества имеют одинаковую мощность...
Не совсем. В классическом double двоичное представление NaN-значения не уникально.
Там речь шла о том, что и `Int64`, и `double` занимает в памяти 8 байт, и каждое сочетание бит там может интерпретироваться как корректное значение любого из этих типов. Разные NaNы также являются корректными в том смысле, что их можно использовать во всех операциях (результатом как правило будут также NaNы, но это уже на важно).
Конечно, двоичных представлений наборов из 8 байт одно и то же количество (2^64) и можно между этими двоичными представлениями создать (тривиальную) биекцию. Но дальше начинается скользкое поле "что является одним и тем же значением". В принципе, если пользоваться totalOrder IEEE 754 и сделать на основе его отношение эквивалентности, то значений действительно 2^64, но все другие способы сравнения значений дают меньше значений, чем 2^64. Правда с оговоркой, что в большинстве этих "других способов сравнения" результат этого сравнения NaN и NaN даёт false (т. е. математически это не является симметричным, а значит не является отношением эквивалентности). А в прикладном ПО totalOrder IEEE 754 фактически не используется.
Короче, я бы поостерёгся писать, что они равномощны, потому что это сильно зависит от контекста и деталей реализации (полнота поддержки IEEE 754 - тоже одна из таких деталей).
Очень примечательно: по-видимому, из соответствия Карри-Ховарда следует, что любая сколь угодно сложная логика (темпоральная, немонотонная) представима в виде теории типов. А ещё любой современный компилятор, скажем, Rust, также является продвинутой системой доказательств, т.е. ризонером для очень выразительных логических вычислений.
К сожалению, не хватает компетенции, чтобы ответить за все системы логики, но теория типов разрабатывалась для самого обоснования математики, чтобы была возможность проверить, корректны ли рассуждения в этом весьма гибком формализме, или нет. Конструктивная теория типов привнесла существенные выразительные возможности, а HoTT вообше претендует на звание фундамента всей математики. Теория категорий зародилась как обобщение теории типов, но и её саму можно выразить с помощью типов!
Дейстаительно, инструмены статической типизации отвечают за доказательство корректности программы. Вот только во многих языках они.. "альтернативно продвинутые")). Например, при слабой системе вывода типов случаются ложноотрицательные вердикты, а изменяемые переменные приводят к ложноположительным и т.п.
В Scala достаточно мощная система типов, в сравнении с Java, C# и т.п., но до каких нибудь Coq или Agda ему далеко...
Да, есть системы типов с модальностями (напр., R. Davies et al. A Modal Analysis of Staged Computation), есть кучная куча систем с линейными типами и т.п.
Одна из важных особенностей теории типов в традиционном её понимании в том, что она соответствует proof-relevant логикам, т.е. в теории типов терм/доказательство M:A принципиально может обладать свойствами, отличными от другого терма/доказательства N:A того же типа/высказывания A. Соответственно, все логики, в которых «плевать на само доказательство, лишь бы оно было», плохо интерпретируются в терминах программ и типов.
Другая особенность — это вычислительная семантика термов/доказательств. В HoTT, например, на каждый тип приходятся правила вывода, среди которых помимо стандартных для логики правил (англ. терминология) Formation, Introduction, Exclusion есть ещё Evaluation (соответствует β-редукции) и Uniqueness (соответствует η-редукции). Если в логике нет аналога β-редукции, сложно доказательства интерпретировать как программы.
Offtop к сообщению @Underskyer1. Теория категория зародилась как обобщения безудержно плодящихся топологических теорий и, как было почти сразу обнаружено тогда же в середине XX века, алгебраических систем ввиду сходства типичных конструкций и построений, а также применимости алгебраических методов в геометрии и наоборот. Теория типов жила и развивалась весь XX век независимо и только в самом конце начали пытаться натянуть её на инструменты теории категорий.
Спасибо за уточнение. Действительно, теория категорий не позиционировалась как обобщение теории типов. Хотел лишь сказать, что она базируется на некоторых идеях, сформулированных в теории типов, т.е. по сути выросла из неё, вобрав её в себя как небольшую часть. Но, не смотря на это, теорию категорий всё ещё можно сформулировать на языке теории типов. Этот факт показался мне достойным упоминания в предыдущем комментарии))
Если не сложно укажите пожалуйста источник изображения с пазлом: https://twitter.com/01k/status/1067788059989684224?s=46
Теория типов