После семинара между двумя Александрами (Гусевым и Коноваловым) возникла переписка с ограничеснной рассылкой только тем, кто был на семинаре. Я захотел встрять и посылаю письмо в refal@botik c надеждой, что это обсуждение будет интересно всем. Также я указал в BCC тех, кто был на семинаре, но на нашу рассылку не подписан, и еще некоторых коллег.
Оба Александра выразили свою нелюбовь к понятию ссылки как к кандидату к включению в область данных Рефала. А я выступлю в защиту этого понятия, в том числе с математической точки зрения. Подозреваю, нарушения эквивалентности при наивных преобразованиях в Рефале с лямбда-выражениями, о которых на семинаре рассказывал Александр, произошло именно потому, что семантика равенства по ссылке, "ссылочного равенства", была не до конца осознана. Она действительно нетривиальна. Эквивалентные преобразования, по определению, должны сохранять семантику. А для этого семантика должна быть понята и сформулирована. *From: Александр Гусев <gusev_aleksa...@mail.ru <gusev_aleksa...@mail.ru>> Sent: Monday, May 17, 2021 11:17 PM* > Лично я - противник использования ссылок в Рефале. Оставьте их языкам > близким к машинному уровню. Здесь же «ссылка» должна быть просто отсылкой к > функции или объекту, но не адресом. Даже если в низкоуровневой основе это и > адрес. Это как использование goto в императивных языках понижает качество > кода. Goto - это для низкоуровневого кода, ассемблера и естественно > присутствует в любой программе, но на машинном уровне. > *On Tue, 18 May 2021 at 14:53, Александр Коновалов <a.v.konovalo...@mail.ru <a.v.konovalo...@mail.ru>> wrote:* > В общем-то я тоже. Поэтому в компиляторе до сих пор нет ссылочных типов > данных вроде динамических ящиков. Единственные ссылочные данные, которые > есть — это замыкания и они иммутабельны. В Рефале-2, Рефале Плюс > и Рефале-6 мутабельные ссылочные данные есть. > Давайте сразу договоримся, что ни о каких адресах речи не идет. Рефал – язык высокого уровня, и его (достаточно простая) семантика должна быть сформулирована в терминах абстрактного вычислителя. Ссылки – это понятие высокого уровня. Ссылки вызывают у нас протест, на мой взгляд, только потому, что они выходят за теоретико-множественный мир значений, привычный из обычной научной деятельности, выученной из школы и университетского мат-анализа. Пойди наука, математика и логика по-другому (скажем, в другой, неземной цивилизации), мы (инопланетяне) считали бы привычные землянам значения некоей ограниченной формой данных и информации. Ведь в жизни мы без труда наивно используем понятие "тот же самый". Посмотрим, например, на такой диалог: - Мама: На столе лежит *то же самое *яблоко, что я оставила тебе на ужин? Ты не съел? - Вовочка: Я его съел. А на стол положил *такое же* из сумки, чтобы ты утром поела. На Рефале и других функциональных языках мы можем говорить только про "такое же" яблоко. Поди отличи вчерашнее и сегодняшнее яблоки по их фотоснимкам на Рефале! Не сможете. А как видите, наш наивный мозг без труда использует понятие "то же самый", который формализуется уникальной ссылкой на вчерашний объект-яблоко, а сегодняшний объект-яблоко будет идентифицироваться другой, новой ссылкой. Это значит, что цивилизация, не испорченная математикой XIX (Фреге, Кантор) и XX (Гильберт, Бурбаки) веков, в принципе, могла бы сразу породить языки программирования с объектами и ссылками на них, а не идти долгим путем от Фортрана и Алгола-60 через Лисп и Рефал к Симуле-67 и затем к осознанию фундаментальности объектно-ориентированного программирования. Занятно, что в английском языке нет слов для такого четкого различения этих понятий, как в русском. Слово "the same" означает и "такой же", и "тот же самый". Интересно, труднее ли носителям английского языка понимать эту разницу, чем русским? В "Феномене науки" Турчин пишет, что "предметы", выделяемые "указателем внимания", и предикаты, признаки, значения – это разные сущности. У него это погружено в более широкое обсуждение и разбросано в нескольких местах. Я сейчас нашел их гуглением по слову "кинолента", поскольку помнил, что он использует эту метафору. Почитайте вот эти разделы и обратите внимание на приведенную во втором пункте цитату: - *6.11. Физический предмет и логический объект* http://www.refal.net/turchin/phenomenon/chapter06.htm#06.11 - *7.5. Феноменологическое определение семантики* http://www.refal.net/turchin/phenomenon/chapter07.htm#07.05 «Теперь, когда мы ввели понятие указателя внимания, мы можем *определить предмет как киноленту ситуаций с одной непрерывной линией указателя внимания*.» - *10.10. Платонизм в ретроспективе* http://www.refal.net/turchin/phenomenon/chapter10.htm#10.10 Турчин вводит понятие предмета в мире со временем. И в истории программирования понятие объекта появилось как обобщение изменяемой сущности в императивных языках. Но оказывается, все-таки есть возможность в логике и в языках программирования ввести понятие ссылки раньше понятия времени, то есть еще сохраняя чистую функциональность. А раз *можно*, то и *нужно *так поступить, чтобы построить адекватную иерархию понятий, – сначала формализовать понятие ссылки, а уже потом, и лишь только когда требуется, ввести понятие времени. Посему я хотел бы иметь такой универсальный метаязык (пусть это будет расширенный Рефал), в котором есть такие фундаментальные понятия нашего познания мира как предмет, уникальное имя предмета, а значит и программистское понятие объекта, про который говорят, используя слова "тот же самый". А также есть формализация этих слов в понятии ссылки, уникального имени. Отсюда возникает потребность внести это понятие в Рефал. Что имеется в виду? Ссылки порождаются оператором генерации новой, свежей, уникальной ссылки *new* или *fresh* – называйте по вкусу. Первое – из объектно-ориентированных языков, второе более распространено в математических текстах и используется в работах группы Andrew Pitts <https://www.cl.cam.ac.uk/~amp12>'а и их чисто функциональных языках *FreshML *и *Fresh Objective Caml*: https://www.cl.cam.ac.uk/~amp12/freshml/ Формальное понятие ссылки можно (а значит и *нужно* – по Бритве Оккама) ввести до понятия того, на что она ссылается. Здесь слово "ссылка", "имя" сбивает с толку: "ссылка на что? имя чего?". А вот "ничего" – сама по себе. В работах группы Pitts'а для таких абстрактных ссылок и имен самих-по-себе используется менее двусмысленное слово "*атом*". Атом, сгенерированный оператором *new*, обладает единственным свойством: *он равен самому себе и не равен всему остальному в момент порождения*. При копировании – например, в вызове f(new) функции, возвращающей пару: f(x)=(x,x) – сохраняется тождественность атома самому себе в каждом его вхождении. Теоретико-множественный математик сойдет с ума от термов, использующих оператор new, как f(new), поскольку для них не выполняется *референциальная прозрачность *(*referential transparency*), пронизывающая основания нынешней логики и математики, а именно: Повторное вычисление может давать неравные результаты, например, для f выше: f(new) =/= f(new) Вот это и есть сущностная причина нелюбви функциональных программистов к ссылкам. И отношения математиков к ним как к низкоуровневому машинному понятию, вносящему "низменную грязь" в их "идеально чистый" математический мир. Но те, кто хочет иметь формальные языки, отражающие и моделирующие реальный мир, должны с ними смириться и строить для них "хорошие теории", чтобы было комфортно думать о ссылках и именах. В этом деле нам, "слабым программистам", за последние 30 лет пришли на помощь "сильные математики" во главе с Andrew Pitts <https://www.cl.cam.ac.uk/~amp12>'ом. Но еще много работы впереди, и мы без нее не останемся. На закуску порассуждаем математически, почему понятие ссылки, атома со связанным с ними равенством (назовем его *ссылочным*) – самое "фундаментальное". Напомним, что даже потеряв референциальную прозрачность, мы сохраняем упомянутое выше свойство, что при копировании равенство сохраняется: - *let* x := *new*; y := *new in* x =/= y - *let* x := *new*; y := x *in* x == y Теперь заметим, что все виды равенств, все отношения эквивалентности частично упорядочены импликацией: влечет ли одно равенство (обозначим =1=) другое (=2=): - x =1= y => x =2= y *Утверждение*. Из ссылочного равенства следуют все другие отношения равенства / эквивалентности, то есть: - для ссылочного равенства R и любого отношения эквивалентности E: x R y => x E y Говоря языком логики, ссылочное равенство – самое "сильное". Оно связывает равенством минимальное число сущностей. Меньше не придумаешь, не нарушая сохранения равенства при копировании. А без этого уж никуда! Говоря языком теории категорий, в категории равенств, категории отношений эквивалентности, ссылочное равенство – *инициальное *(*initial*). Это заумное слово означает в точности вышеприведенное утверждение и ничего больше. Вот поэтому, ссылки – это вовсе не адреса в памяти машины, а фундаментальное математическое понятие. Enjoy it! Андрей Климов >
