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

[arseniiv]

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

Главное, что принцип работает и компилируется - то самое завещанное SICP счастье абстрактного списка через последовательное сцепление пар, реализованное без data а через функции.

Работать-то работает… Кстати, а числа, кодируемые функциями $\lambda f.\; f^{(n\text{-кратная композиция)}$, видели?

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

А при таком последовательном сцеплении пар тип тожепоследовательно накручивается и зависит от длины списка.

А, это. В хаскеле комбинатор фиксированной точки на уровне типов выразим, но только используя data, вроде. Тут я плаваю, не верьте мне и проведите своё исследование. Просто я видел упоминания типа Fix довольно близко к упоминаниям type-level вычислений, но для чего он там нужен, особо не интересовался. Обычную же функцию fix, fix f = f $ fix f типизировать можно. Вот сие

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

> let fix f = f (fix f)
fix :: (t -> t) -> t
> let factorial = fix (\f x -> if x == 0 then 1 else x * f (x - 1))
factorial :: Integer -> Integer
> factorial 6
720
it :: Integer

работает, и если вам только это было и нужно (сомневаюсь) — ура! [Ухожу спать, всем удачи.]

-- Пн мар 09, 2015 06:25:07 --

(Оффтоп)

А вообще я не там скобку поставил сначала, и Хиндли и Милнер тут как тут! Тот самый бесконечный тип, попадалось такое и раньше.

[_Ivana]

Вы про нумералы Черча? Если да, то видел, хотя и не вникал глубоко. Я верю, что лямбда-формализм может многое :)
Факториалы (и другие рекурсивные функции) через фикс я уже давно баловался. Конечно сейчас нужно было не это. А нужна была, повторюсь, реализация "АТД список" только через функции, что и получилось.

[arseniiv]

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

Вы про нумералы Черча?

О них, просто не помнил, чьи они (есть же ещё вторые, как раз через списки). Выражения арифметических действий, включая возведение в степень — это прекрасно.

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

А нужна была, повторюсь, реализация "АТД список" только через функции, что и получилось.

Да, спасибо, я не помнил, помогает ли фикс в них. По идее, не должен, так что зря я.

[_Ivana]

Это я не видел как фикс может помочь, а некоторые товарищи его зачем-то используют: http://www.s-schoener.com/blog/2014/05/ ... n-haskell/

И вообще набрав в гугле "ChurchList a = forall b . (a -> b -> b) -> b -> b" я нашел немало ссылок по теме. Правда, все они через ранки, буду разбираться.

[aa_dav]

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

Если функции как данные и как объекты первого класса я еще могу представить как чанки в ОЗУ, а тут данные как функции или аргументы, спрятанные в их параметрах...

Ага, это забавное свойство ФП. Но ничего сверхъестественного здесь нет - хранилищем данных является контекст функции. И на уровне реализации вместе с замыканиями всё это превращается в garbage collector. Собственно замыкания - это та фишка, которая и делает возможным такие целенаправленные сцепки и расцепки контекстов, и, как следствие, превращать функции в хранилища данных.

[aa_dav]

P.S.
Собственно, если вопрос именно в том - как ситуация выглядит "из глаз" императивного подхода, то функция как значение в программе суть структура из ссылки на код и ссылки на контекст функции. Контекст может ссылаться не только на числовые значения, но и на другие функции-значения со своими контекстами и потому образовывать древовидные структуры.

[aa_dav]

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

Зачем тогда в том же Haskell есть АТД как основа всего сущего?

Хаскель - он язык типизированный, а потому сразу же типы напрашиваются в основы языка.
Это скорее наоборот в схеме можно имитировать "тип", например "дата", по схеме из начало топика:

(define (date year month day) ... )

так, что сконструированный "объект"

(let x (date 1980 12 20) 
...
(x 0) вернет год
(x 1) вернет месяц и т.п.

И ведь всё это даже напоминает объекты из ООП, только в стиле ФЯ - немутабельные - мы предьявили "интерфейс" по которому конструируем нечто и потом из него получаем что-то. Есть интерфейс, есть запрятанные за ним данные. Что это как не объект, что это как не тип?

[_Ivana]

aa_dav, спасибо. Вообще мне эта ситуация интересна со многих сторон - и реализация "из глаз" императивного подхода, и формальное описание через лямбды, и практические опыты. Не сразу привыкаешь к концепциям типа: частично применили функцию к нескольким параметрам, получили новую функцию, которая в себе их содержит, потом эту новую применили к параметру-функции, которая вытаскивает и комбинирует часть параметров, сохраненных при первом применении и т.п. А параллельно выясняются отличия и ограничения статически типизированных языков, что в них невозможно сконструировать бесконечный тип. В общем, тема провоцирует интерес в различных направлениях.

[arseniiv]

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

А параллельно выясняются отличия и ограничения статически типизированных языков, что в них невозможно сконструировать бесконечный тип.

Ну, вроде ограничений на присутствие в языке $\mu$ нет ($\mu x.1+ax\sim[a]$). Вот тот же самый type-level Fix можно сделать, но не через type.

Кстати, если вдруг что, изменяемость данных тоже не противоречит строгой типизации — например, Disciple (я на его сайте ничего не понял, пока не почитал статью ), сочетающий несколько уже известных к его созданию идей (известных автору — я всё прочитал впервые). Там ещё и способ описания побочных эффектов, не прибегая к монадам.

[aa_dav]

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

А параллельно выясняются отличия и ограничения статически типизированных языков, что в них невозможно сконструировать бесконечный тип.

Эммм... Тут по моему не так. Я очень плохо помню хаскель, но насколько помню дерево там можно заявить в виде типа и никаких проблем с функциями с ним работающими не будет. Просто строгая типизация предполагает... строгую типизацию.

-- 11.03.2015, 09:35 --

P.S.
А с другой стороны там разве нельзя объявить тип T, который хранит Int и функцию возвращающую T или Null, к примеру? Будет очень похоже. Но не помню хаскелля в деталях.

[_Ivana]

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

[aa_dav]

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

В том то и дело, что я не хочу объявлять новый тип явно - типом, а хочу написать набор функций-интерфейсов, которые будут задавать мой тип абстрактно

Ну если только как самоцель... Так то Хаскель проблему составных типов уже решил как раз типами собственно. Типизация немного суживает "красоту простоты решения", в данном смысле но у неё зато другие преимущества. В любом случае, то что контекст функции может хранить замыкание, и, как следствие, хранить данные - сохраняется. Но уже просто не нужно как лишняя перемычка там где можно данное воткнуть прямо в тип, без промежуточной функции-хранителя.
SICP, конечно, по мозгам ударяет. Но Хаскель это своего рода, по моим внутренним впечатлениям, С++ от мира ФП, такой же перегруженный конструкциями, огромный и подавляющий новичка. :)

[arseniiv]

_Ivana
В любом случае «создать» тип, не используя newtype/data, не получится. Он либо выразим выбранным множеством способов и «уже был» в языке, либо не выразим и его никак туда не добавить, ведь этот тип должен участвовать в типах функций.

aa_dav в сообщении #988740 писал(а):

Но Хаскель это своего рода, по моим внутренним впечатлениям, С++ от мира ФП, такой же перегруженный конструкциями, огромный и подавляющий новичка. :)

Да ладно. Без расширений GHC — перегруженный? Я чего-то не понимаю в этом мире.

[aa_dav]

arseniiv в сообщении #988867 писал(а):

Да ладно. Без расширений GHC — перегруженный? Я чего-то не понимаю в этом мире.

Конечно - куча правил синтаксиса и синтаксических конструкций, зачастую делающих одно и то же просто разными выражениями. По сравнению с лиспом, святой наивностью из скобок, вообще земля и небо. Да просто посчитайте число символов которые что-то важное значат в лексике. А еще правила перевода строк, еще более сложные чем просто вложенные отступы.
Вообще видно, что всеми силами добивались краткости - и таки, бесспорно, добились. Но синтаксис стал тяжелый, если это не тяжелый синтаксис, то я не знаю что такое тяжелый синтаксис.

[arseniiv]

aa_dav в сообщении #988896 писал(а):

По сравнению с лиспом, святой наивностью из скобок, вообще земля и небо.

Так вы же не с одним лиспом сравнивали, а с самим C++!

aa_dav в сообщении #988896 писал(а):

Да просто посчитайте число символов которые что-то важное значат в лексике.

Опять же, с чем сравнивать будем? Может, сравним с APL?

aa_dav в сообщении #988896 писал(а):

А еще правила перевода строк, еще более сложные чем просто вложенные отступы.

Можно всегда использовать { ; }.