Спасибо, Андрей! Всё замечательно выражено. Действительно, если даны правильные определения, дискутировать становится подчас не о чем. Я, конечно, подразумевал именно адресные ссылки, которые наблюдал в языках высокого уровня и остался ими недоволен. А вот математически описанные Вами ссылки - это отлично, проходит!
Отправлено из мобильной Почты Mail.ru вторник, 18 мая 2021 г., 23:01 +0300 от refal <[email protected]>: >После семинара между двумя Александрами (Гусевым и Коноваловым) возникла >переписка с ограничеснной рассылкой только тем, кто был на семинаре. Я >захотел встрять и п осылаю письмо в refal@botik c надеждой, что это обсуждение >будет интересно всем. Также я указал > >в BCC > >тех, кто был на семинаре, но на нашу рассылку не подписан, и еще некоторых >коллег. > >Оба Александра выразили свою нелюбовь к понятию ссылки как к кандидату к >включению в область данных Рефала. А я выступлю в защиту этого понятия, в том >числе с математической точки зрения. > >Подозреваю, нарушения эквивалентности при наивных преобразованиях в Рефале с >лямбда-выражениями, о которых на семинаре рассказывал Александр, произошло >именно потому, что семантика равенства по ссылке, "ссылочного равенства", была >не до конца осознана. Она действительно нетривиальна. Эквивалентные >преобразования, по определению, должны сохранять семантику. А для этого >семантика должна быть понята и сформулирована. > >From: Александр Гусев < [email protected] > >Sent: Monday, May 17, 2021 11:17 PM >>Лично я - противник использования ссылок в Рефале. Оставьте их языкам близким >>к машинному уровню. Здесь же «ссылка» должна быть просто отсылкой к функции >>или объекту, но не адресом. Даже если в низкоуровневой основе это и адрес. >>Это как использование goto в императивных языках понижает качество кода. Goto >>- это для низкоуровневого кода, ассемблера и естественно присутствует в любой >>программе, но на ма шинном уровне. >On Tue, 18 May 2021 at 14:53, Александр Коновалов < [email protected] > >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 'а и их чисто >функциональных языках 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 'ом. Но еще много работы впереди, и мы без нее не останемся. > >На закуску порассуждаем > >математически, почему понятие ссылки, атома со связанным с ними равенством >(назовем его ссылочным ) – самое "фундаментальное". Напомним, что даже >потеряв референциальную прозрачность, мы сохраняем упомянутое выше свойство, >что при копировании равенство сохраняется: >* 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! > >Андрей Климов
