Типы, как наборы функций, удовлетворяющие условиям?

[_Ivana]

Просветите дилетанта и помогите внести хотя бы малую ясность в таком вопросе. Я до последнего времени жил в представлениях, что есть ОЗУ/ЕЕПРОМ с линейной адресацией и определенной разрядностью, набор регистров и система команд процессора. И все было просто и понятно - навалил кучу байт - это ДАННЫЕ, трактуешь их как хочешь, загружаешь в регистры, ИЗМЕНЯЕШЬ командами, пишешь обратно... Последовательность псевдокоманд в ОЗУ - это тоже ДАННЫЕ, хоть и можно их последовательно считывать и в зависимости от содержимого выполнять разные инструкции, изменяющие другие данные... И всякие Си/Паскали и т.п. воспринимались как ОБЕРТКИ над этой стройной картиной - наш друг компилятор, который нафигачит кучу инструкций для кратких абстракций в коде, ну появились ТИПЫ - некоторые соглашения как мы интерпретируем байты ДАННЫХ, параметры/возвращаемые значения функций - но стек то и так уже был...
Несколько месяцев назад эта идиллия несколько трансформировалась с открытием "функций как объектов первого класса" - ну допустим это понятно, чанки - те же паттерны кодирования инструкций в ячейках памяти данных/стеке. Всякий страх из серии "ТИПЫ - это неподвижные точки специальных объектов, называемых алгебрами функторов" пока вообще не ассоциируется ни с какой концепцией, и отложен до лучших времен. Но вчера взялся за простую книжку "для юных сурков" - SICP, до определенного момента было все понятно и хорошо, но разрыв шаблона случился при прочтении следующего откровения:

Цитата:

Мы ведь ни разу не сказали, что такое пара, и указывали только, что для работы с
парами язык дает нам процедуры cons, car и cdr. Но единственное, что нам надо
знать об этих процедурах — это что если мы склеиваем два объекта при помощи cons,
то с помощью car и cdr мы можем получить их обратно. То есть эти операции удовле-
творяют условию, что для любых объектов x и y, если z есть (cons x y), то (car
z) есть x, а (cdr z) есть y. Действительно, мы упомянули, что три эти процедуры
включены в наш язык как примитивы. Однако любая тройка процедур, которая удовле-
творяет вышеуказанному условию, может использоваться как основа реализации пар.

Эта идея ярко иллюстрируется тем, что мы могли бы реализовать cons, car и cdr без
использования каких-либо структур данных, а только при помощи одних процедур. Вот
эти определения:
(define (cons x y)
(define (dispatch m)
(cond ((= m 0) x)
((= m 1) y)
(else (error "Аргумент не 0 или 1 -- CONS" m))))
dispatch)
(define (car z) (z 0))
(define (cdr z) (z 1))
Такое использование процедур совершенно не соответствует нашему интуитивному по-
нятию о том, как должны выглядеть данные. Однако для того, чтобы показать, что это
законный способ представления пар, требуется только проверить, что эти процедуры
удовлетворяют вышеуказанному условию.

Это что теперь - все можно, режь-коли, души гусей? (С) Если функции как данные и как объекты первого класса я еще могу представить как чанки в ОЗУ, а тут данные как функции или аргументы, спрятанные в их параметрах... Зачем тогда в том же Haskell есть АТД как основа всего сущего? Если там тоже функции - объекты первого класса, можно ли там также реализовать данные как функции без АТД и другие функции на них? В общем, помогите непротиворечиво совместить в голове все эти концепции...

[AlexDem]

Здесь можно напомнить про принцип KISS.

[_Ivana]

AlexDem

(Оффтоп)

Цитата:

Молодая, симпатичная девушка приходит в церковь, подходит к священнику. На ней ни макияжа, ни бижутерии, одежда консервативно-строгая. Потупив голову, спрашивает:
- Батюшка! Выскажите свою концептуальную оценку по поводу последней монографии протоиерея Иоанна Меендорфа посвященной им Варлаамитско Паламитской полемике; написанной в эпоху окормления им русской диаспоры в Париже??
Батюшка:
- Замуж, дура! Срочно замуж!!!

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

[iifat]

Стесняюсь спросить, вот это — произведение пера начинающего мастера слова, или же (по некоторым слабым признакам) вопрос из области программирования? Или ж таки из области морали и права?
Не специалист в обеих последних, но, полагаю, прежде чем душить гусей, стоит ознакомиться с уголовным и административным правом региона проживания, а также поразмыслить над моральными и нравственными принципами вашими лично и религии, которую вы исповедуете.
По части программирования — это называется как-то типа аксиоматическим заданием функций и имеются языки, не вспомню названий, хотя если интересно — попробую поискать. А, кажись, Alphard, попробуйте погуглить.

[arseniiv]

_Ivana
Вот кстати об АТД. Обычно (насколько я не видел сокращения алгебраических типов данных в АТД) под этим сокращением понимается абстрактный тип данных. Это то, на что вы наткнулись: описание типа не тем, как он получается из известных типов, а тем, какие функции $\ldots\to t\to\ldots$ мы имеем. По сути, так рано или поздно даже придётся поступить: иначе не определить примитивные типы типа той же пары $a\times b$, или единичного типа $1$ (() в хаскеле), и т. п..

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

_Ivana в сообщении #986821 писал(а):

Если там тоже функции - объекты первого класса, можно ли там также реализовать данные как функции без АТД и другие функции на них?

Ты не пове Конечно, можно!

Только, похоже, это не совсем abstract data types зовётся, а как правильно — не могу вспомнить. Щас копался-копался, даже на okmij.org не нашёл.

P. S. Ан нет, тоже ADT! Похоже, вот эту статью я где-то и читал.

[AlexDem]

_Ivana в сообщении #986825 писал(а):

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

Я не программировал на языках, которые Вы привели, поэтому, может, будет не совсем по теме. У нас было подобное обсуждение на уровне понятий:

AlexDem в сообщении #383257 писал(а):

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

AlexDem в сообщении #384934 писал(а):

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

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

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

-- менее минуты назад --

(Ну а класс - это и есть тип, и является он именованным набором отношений, про что Вы и спрашивали, вроде)

[iifat]

AlexDem в сообщении #986869 писал(а):

Что такое объект?

Ну, вообще-то, объектов «как таковых» не существует. Существует куча контекстов в каждом из которых под этим словом понимают что-то своё. А абстрактные типы данных, помнится, гораздо старше.

[AlexDem]

Я подозреваю, что всё это тонкости реализации и здесь совершенно не существенно. Те же АТД можно считать классами (а переменные этих типов - объектами) без ущерба для ничего.

-- менее минуты назад --

Забыл добавить - в этой связи полезно посмотреть формат RDF, где вся информация о предметной области задаётся в виде троек: субъект-предикат-объект. После чего мысленно пакуем тройки в таблицу реляционной СУБД, вспоминаем, что каждая таблица там - это отношение, и вуаля (если так будет проще понять).

[odelschwank]

_Ivana в сообщении #986821 писал(а):

Если там тоже функции - объекты первого класса, можно ли там также реализовать данные как функции без АТД и другие функции на них?

Забавно, что да:

Используется синтаксис Haskell

cons x y z = z x y
car p = p (\x y -> x)
cdr p = p (\x y -> y)

С оговорками, конечно. Например, сигнатуру типа такой пары я не берусь написать)

[_Ivana]

Ну сигнатуру можно и у интерпретатора спросить:

Используется синтаксис Haskell

Prelude> :t cons
cons :: t1 -> t2 -> (t1 -> t2 -> t) -> t
Prelude> :t car
car :: ((t2 -> t1 -> t2) -> t) -> t
Prelude> let p = cons 1 2
Prelude> :t p
p :: (Num t2, Num t1) => (t1 -> t2 -> t) -> t
 

А вот попробовать разобраться в этих вещах действительно интересно, причем в трех направлениях:
- сугубо теоретическом, читая про структурную рекурсию/оригами/свертку-развертку на типах/ранки/леммы Ламбека и т.п.
- сугубо практическом, пробуя методом тыка переписывать прогнозируемо работающий код с использованием таких типов
- с точки зрения "как оно на самом деле" - с позиций содержимого ОЗУ и его обработки

[_Ivana]

Первый блин - попытка создать тип данных "список" оказался комом - интерпретатор на захотел создавать неопределенный тип. Приходится начинать с букваря - простое использование одной пары:

Используется синтаксис Haskell

--cons x y = (x,y)
--car = fst
--cdr = snd

cons x y z = z x y
car p = p (\x y -> x)
cdr p = p (\x y -> y)

f p x = cons (car p + x) (cdr p + 1)
g p = (car p) `div` (cdr p)
mean = g . foldl f (cons 0 0)

main = do
    print $ mean [1..10]
 

[arseniiv]

_Ivana в сообщении #987098 писал(а):

- с точки зрения "как оно на самом деле" - с позиций содержимого ОЗУ и его обработки

Реализовать-то можно по-разному. Можно скомпилировать функции и кидаться указателями (и не указателями), а можно что-то разной степени наивности, а если отвлечься от реализации, этот вопрос уже не задашь.

_Ivana в сообщении #987098 писал(а):

Ну сигнатуру можно и у интерпретатора спросить:

У car и cdr выводятся слишком общие типы. Можно это исправить вручную:

Используется синтаксис Haskell

> :set +m
> :set -XRankNTypes
> type P a b = forall c. (a -> b -> c) -> c
> let cons :: a -> b -> P a b
|     cons a b = \c -> c a b
> let car :: P a b -> a
|     car p = p (\x y -> x)
> let cdr :: P a b -> b
|     cdr p = p (\x y -> y)
 

Как можно видеть, теперь типы такие же как у (,), fst, snd с заменой (,) на P!

[_Ivana]

5 минут знакомства с волшебным функциональным языком Ela - и все работает, что не удается сделать в хаскеле - вот кот:

Используется синтаксис Haskell

mycons x y = \m -> if m==0 then x else y
mycar z = z 0
mycdr z = z 1
mynil = id
isnil l = (mycar l)==0

myfold f a l = if isnil l then a else myfold f (f a $ mycar l) (mycdr l)
mymap f l = if isnil l then mynil else (f $ mycar l) `mycons` mymap f (mycdr l)

int2mylist 0 = mynil
int2mylist n = mycons n $ int2mylist ((-) n 1)

myfold (+) 0 ( mymap (*10) ( int2mylist 10 ) )

набираем в онлайн интерпретаторе http://elalang.net/elac.aspx и радуемся
Правда, условие на конец списка глупое - но делал навскидку, верю что можно сделать и нормально - не по первому аргументу пары. Просто с Ela до сего момента не встречался, не знаю синтаксис и повадки еще.

[arseniiv]

_Ivana в сообщении #987670 писал(а):

Правда, условие на конец списка глупое - но делал навскидку, верю что можно сделать и нормально - не по первому аргументу пары.

Особо не думал и не вспоминал, но можно устроить список из Maybe-подобных вещей: just x = cons true x, nothing = cons false anything, где (фольклор λ-исчисления) true x y = x, false x y = y, а вместо if при большом желании используется id. Таким образом получим isJust = car, fromJust = cdr.

-- Пн мар 09, 2015 05:58:26 --

Кстати, а что конкретно с хаскелем-то не получалось?

[_Ivana]

Да это уже детали. Можно и тройку вместо пары организовать, где третий элемент будет определять 0-конец списка, 1-не конец. Этож АТД, реализацию можно теперь как угодно перекраивать :) Главное, что принцип работает и компилируется - то самое завещанное SICP счастье абстрактного списка через последовательное сцепление пар, реализованное без data а через функции.

-- 09.03.2015, 04:02 --

А с хаскелем не получалось ничего (как обычно у меня, то что на С пишу 5 минут на хаскеле 2 дня - без преувеличения). В хаскеле живут 2 человека - Хиндли и Милнер, они четко следят чтобы на вход любой функции приходило только то что надо, и не компилируют если это не выполняется. А при таком последовательном сцеплении пар тип тожепоследовательно накручивается и зависит от длины списка. В Лиспе и Эле этих товарищей нет и они не мешают жить.