[капитан][ФП] Чистые функции не такие чистые

Зачем !?

! просто так (строгость), можно и без него (нестрогость):

f :: *a -> *b
f x = f x

f :: IO a -> IO b
f x = x >> f x

f :: IO a -> IO b
f = forever

В хаскеле мы никак не сможем статически гарантировать, что при использовании такого IO все будет «хорошо», т.к. мы всегда можем вытащить этот World и сделать с ним все, что душе угодно (чистота в хаскеле системой типов и не гарантируется). С другой стороны, объявив в Clean World уникальным, мы получаем статические гарантии.

Вот тут нужно привести пруф в коде. Что могут дать уникальные типы, чего не умеют обычные полиморфные / параметрические (в примерах и картинках)? Почему нельзя считать *a эквивалентным IO a?

Интересный вопрос :)

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

можно и без него

Ну да, потому и спросил - зачем. Кстати, без строгости в Clean в таких местах очень интересных эффект - можно гарантировать, что никогда не откроется файл, который не будет закрыт, например :)

Вот тут нужно привести пруф в коде. Что могут дать уникальные типы, чего не умеют обычные полиморфные / параметрические (в примерах и картинках)?

Конкретный пример - есть монада State a b, ее можно сделать и в хаскеле и в Clean. Далее мы можем сделать сделать инстанс IO a = State a World. НО! в хаскеле нету никакого способа на типах гарантировать, что мы не сможем вытащить этот World и сделать все, что с ним хотим (от чего код, конечно, сломается). В Clean мы просто ставим *World и при написании некорректного кода система типов даст по рукам. То есть еще раз - при помощи IO в хаскеле можно написать корректный код только при условии, что мы не можем вытащить значение из IO. И типами запретить такое вытаскивание нельзя. В Clean мы тоже можем вытащить и тоже нельзя запретить вытаскивание. Но после вытаскивания мы не сможем напортачить. Короче, в Clean функция unsafePerformIO на самом деле safePerformIO :)

Почему нельзя считать *a эквивалентным IO a?

Потому что это семантически разные вещи. Типу IO a в Clean соответствует тип IO a - вычисление, которое вернет a. А вот *File - это обычный File. но только уникальный. Никакое не вычисление. Соответственно, ф-я putStrLn в хаскеле возвращает _вычисление_ (которое неизвестно кто и как потом будет исполнять и вообще непонятно, что это такое), а в Clean она вернет модифицированный World (в котором на наш монитор выведено сообщение). В хаскеле мы собираем вычисление из кусков - а в Clean собираем новые world/file/etc. из старых в виде обычных вычислений, как в любом другом ЯП.

Ну да, в ОП речь не про абстрактные функции, а конкретные на данной архитектуре (раз речь о CPU и памяти)

и в _любом_ языке программироания общего назначения функция это _как минимум_ то что называется функцией на данной архитектур

В рамках архитектуры x86 такого понятия как ф-я, насколько я знаю, нет. Есть переход (условный/безусловный). Который не обязательно является ф-ей.

никогда не откроется файл, который не будет закрыт, например :)

В этом контексте было бы интересно работать аналогичным образом с указателями. Гарантировано - никаких утечек.

никогда не откроется файл, который не будет закрыт

Однажды открытый файл всегда будет закрыт? :)

в хаскеле нету никакого способа на типах гарантировать, что мы не сможем вытащить этот World и сделать все, что с ним хотим (от чего код, конечно, сломается)

В хаскеле эти гарантии даёт система модулей - System.IO не экспортирует ни аккессоров и конструкторов IO, ни других небезопасных функций, поэтому ничего сломать не получится (опасные функции экспортирую System.IO.Unsafe и Unsafe.Coerce).

Короче, в Clean функция unsafePerformIO на самом деле safePerformIO

Как я понял, в хаскеле IO это абстрактный тип, тогда как в Clean его можно написать в языке (за счёт уникальных типов), при этом то что в хаскеле называется «нечистым» в Clean может быть и чистым (нечистым будут небезопасные, то есть вовсе невозможные, конструкции).

Эти уникальные типы имеют какое-нибудь отношение к линейным?

В рамках архитектуры x86 такого понятия как ф-я, насколько я знаю, нет.

Есть стэк, регистры EBP и ESP, инструкции CALL, RET, PUSH и POP, так что обычно функция определена с точностью до соглашения о вызове (а с точки зрения ОС функция должна иметь и имя, потому что PIC).

В этом контексте было бы интересно работать аналогичным образом с указателями. Гарантировано - никаких утечек.

Написать:

if random then release x

не получится?

В Cyclone система типов основана на линейной, но там до такого не дошли, ну и Cyclone не разграничивает чистые и нечистые функции.

или

if bigComputation then release x

Однажды открытый файл всегда будет закрыт? :)

Нет, он просто не будет открыт. Хотя я сейчас подумал - это не так, ведь форсить открытие можно не обязательно закрытием. Например, если считать из файла строку и вывест в другой файл (который обязательно будет закрыт) то первый все равно откроется. Вот если других аналогичных ф-й не было - тогда.

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

Да, но система типов тут не при чем. С ее точки зрения в выдергивании значения из IO нет ничего странного, и тут дыра в семантике.

Как я понял, в хаскеле IO это абстрактный тип, тогда как в Clean его можно написать в языке (за счёт уникальных типов)

Именно так. То есть если в хаскеле мы можем считать, что IO a = State a World, где World - какая-то особая вещь, зарытая в недрах реализации и при помощи системы модулей не даем доступа к кишкам, то в Clean все это выражается в рамках ЯП и World там есть самый что ни на есть настоящий (то есть конкретно - пишем тайпкласс для монад, монаду State и далее определяем IO a = State a *World).

при этом то что в хаскеле называется «нечистым» в Clean может быть и чистым

Именно так. Пример - если мы что-то откуда-то считали, то любое преобразование этого «чего-то» уже не чисто, то есть список длины n будет внутри IO, если эта n сама считана из файла или стандартного ввода. В clean же эта n - совершенно обычное число и список - совершенно обычный список (не обязательно уникальный или из уникальных значений). Вообще говоря - если в хаскеле у нас есть разделение чистое/нечистое, то в Clean его и нет на самом-то деле. То есть в CLean всегда все чисто. С точки зрения семантики f = openfile world, f1 = writefile f «1», f2 = writefile f1 «2»; return f2; Здесь все чисто, никаких сайд-эффектов нет, никаких мутаций не происходит. Мы натурально создаем 3 _разных_ файла f, f1 и f2. И результат работы - файл f2. То, что _на самом деле_ файл один - это просто оптимизация, которую дозволяет звездочка в типе. И она не влияет на семантику :)

Эти уникальные типы имеют какое-нибудь отношение к линейным?

Вроде как это линейные типы с ограничениями.

Есть стэк, регистры EBP и ESP, инструкции CALL, RET, PUSH и POP, так что обычно функция определена с точностью до соглашения о вызове

Ну это не отменяет того, что те или иные ЯП могут компилировать свои ф-и не в call/ret. Особенно если говорить о замыканиях. Замыкание - это функция?

не получится?

Не получится написать два раза release x, release x - это точно. А вот гарантировать, что release будет написано - уже нет, если к поинтеру была применена get. Если не была - то без release поинтер просто не будет создан, но нахрена он такой нужен, без get? Хотя при помощи какого-нибудь костыля может что-то и выйти. Какая-нибудь хитрая монада, да с уникальным типом внутри, например.

if random then release x

Обычно в подобных случаях считается худший вариант. То есть if true cond x - release считается недостижимым.

Кстати, без строгости в Clean в таких местах очень интересных эффект - можно гарантировать, что никогда не откроется файл, который не будет закрыт, например :)

http://rsdn.ru/forum/decl/4522924.flat.aspx не?

if true cond x

if cond x then release x

Ну да, однако нас не радует, что ресурс будет освобожден _когда-нибудь_. На практике требуется - как можно ближе к тому моменту, когда его _можно_ освободить.

А как оно с if работает?

Мопед не мой, я и не разбирался, только мельком глянул. Но мне не очень понятен вопрос, что имеется в виду?

Вообще говоря - если в хаскеле у нас есть разделение чистое/нечистое, то в Clean его и нет на самом-то деле.

На уровне типов нельзя отличить ссылочно-прозрачную функцию от ссылочно-непрозрачной? В хаскеле тоже нельзя, но функция без IO _гарантированно_ ссылочно-прозрачна, а функция с IO _возможно_ ссылочно-непрозрачна.

Замыкание - это функция?

Замыкания довольно далеки от народа^W обычных функций, в том смысле, что это VM надстройка на обычными функциями. Например, для функций int(*)(int x, int y) замыкание (по x или y) это

struct closure_int_int_int {
    int scope;
    int (*fun)(int, int);
};

так же для остальных функций. Для удобства использования нужно делать кодогенератор и/или VM с типами object (= *void?), agrs (= array/list of objects), scope (= map from numbers to objects или array of numbers x args), fun (= object(*)(agrs)), closure (= scope x fun). Тогда вызов замыкания будет осуществляться (обычной) функцией (apply / funcall) принимающей структуры closure и args, составляющей all_args из closure->scope и args и вызывающей (обычную) функцию closure->fun c all_args (который можно потом освободить, если язык не ленивый).

В SBCL, например:

struct closure {
    lispobj header;
    lispobj fun;
    lispobj info[1];
};

Тут ещё замыкания вложены, т.е. closure->fun может быть closure.

В хаскеле, где нет мутабельных замыканий, семантических замыканий и анонимных функций как таковых нет - lambda lifting всё переписывает в CAFs:

f x y = let z = 0 in \a b -> a + b + x + y + z + g
  where g = x + y

g' = \x y -> x + y
f' = \x y a b -> a + b + x + y + 0 + g' x y

f'' = \x y a b -> a + b + x + y + 0 + x + y

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

На уровне типов нельзя отличить ссылочно-прозрачную функцию от ссылочно-непрозрачной?

В Clean нет ссылочно-непрозрачных ф-й. Их нельзя написать. Вообще. То есть если в хаскеле мы можем написать чистую ф-ю которая возвращает нечистое вычисление, то в Clean вообще не существует такого понятия как «нечистое вычисление». Тут полная аналогия с циклом и хвостовой рекурсией. Можно писать непрозрачно и мутабельно с циклом, можно писать прозрачно и немутабельно с хвостовой рекурсией. Причем тот факт, что хвостовая рекурсия оптимизируется, на ссылочную прозрачность не влияет. Аналогично в Clean. При хвостовой рекурсии вместо создания нового функционального фрейма мы перезаписываем старый, тут при создании нового объекта мы перезаписываем старый. То есть это _в точности_ то же самое. Просто в Clean за счет аннотаций уникальности мы можем добавить подобные хвосторекурсивные оптимизации в любое место, а тайпчекер проверит, чтобы наш код оптимизации не ломал.

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

Ну вот в Clean все ф-и _гарантировано_ ссылочно-прозрачные.

Ну вот в Clean все ф-и _гарантировано_ ссылочно-прозрачные.

Это всё хорошо, но как там, например, организовать функцию random возвращающую случайные числа и потом использовать её в виде if random == n then ... (в хаскеле будет do m <- random; if m == n then ...)? Это будет :: *Integer и отличить её от функции которая не будет каждый раз возвращать разное число можно по тому признаку, что она не :: Integer?

Ну как-нибудь так - есть ф-я randomGenerator: Integer -> *Generator. Потом есть ф-я getRandomValue: *Generator -> (Integer, *Generator). Соответственно: [code] generator = randomGenerator 155342; (num1, newGenerator1) = getRandomValue generator (num2, newGenerator2) = getRandomValue newGenerator1 (num3, newGenerator3) = getRandomValue newGenerator2 (num4, newGenerator4) = getRandomValue newGenerator3 [code] Для удобства можно засунуть это в стейт-монаду. С num1...numn работаем как с обычными интегерами (то есть if n = num1 then ...) - они не зафавлены IO, как это будет в случае хаскеля.

Ну как-нибудь так - есть ф-я randomGenerator: Integer -> *Generator. Потом есть ф-я getRandomValue: *Generator -> (Integer, *Generator).

Соответственно:

 generator = randomGenerator 155342; 
(num1, newGenerator1) = getRandomValue generator 
(num2, newGenerator2) = getRandomValue newGenerator1 
(num3, newGenerator3) = getRandomValue newGenerator2 
(num4, newGenerator4) = getRandomValue newGenerator3 

 
Для удобства можно засунуть это в стейт-монаду. С num1...numn работаем как с обычными интегерами (то есть if n = num1 then ...) - они не зафавлены IO, как это будет в случае хаскеля.

они не зафавлены IO, как это будет в случае хаскеля.

Хотя в хаскеле это тоже будет просто стейт-монада, для генерации по зерну IO не нужен. Вот если у нас какой-нибудь генератор из разряда «считать какую-нибудь хрень с какого-то там порта» - тут нужно IO, а в clean функция получения генератора будет примерно такой: getGenerator: *World -> (*Generator, *World). Ну или напрямую getRandom: *World -> (Integer, *World).

Ага, а если readByteFromPort8080 :: *Byte - так и будет и прямо можно потом писать readByteFromPort8080 + 100500? Это на самом деле ничего - в хаскеле тоже можно написать такой (+) который будет вполне хорошо работать и для 1 + 2 и для readByteFromPort8080 + 100500, где readByteFromPort8080 :: IO Byte, просто обычные функции недостаточно умные - автоматически liftиться они не умеют, т.к. IO и прочие это обычные (абстрактные) типы, а не некие примитивные которые компилятор мог бы обрабатывать специальным образам для всех функций (как вот * в Clean).

readByteFromPort8080 + 100500?

скорее, эта функция имеет тип readByte: *Port -> (Integer, *Port). Короче принцип простой - мы просто везде засовываем содержащий состояние объект в стейт-монаду. Мы бы и в хаскеле могли так делать, но там просто нельзя гарантировать корректность работы с подобными монадами без сокрытия конструктора :)

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

Не понял, каким специальным образом? Clean обрабатывает их совершенно обычным образом.

просто обычные функции недостаточно умные - автоматически liftиться они не умеют

А Clean и не лифтит ничего. Разница просто в том, что clean более точно отделяет внешнее состояние. То есть вот в хаскеле мы читаем с порта и получаем IO Integer - здесь и наш Integer и состояние порта. И нет способа выдрать Integer, корректно отделив состояние. С другой стороны, в Clean мы получим (Integer, *Port), здесь Integer - совершенно чист, в нем никакого состояние нет. Все состояние отделено, собрано и заботливо инкапсулировано внутри *Port. Де-факто хаскелевский IO Integer это _и есть_ (Integer, *Port) (или (Integer, *World) если взять общий случай). Просто у него внутристи скрыты. Потому что если не скрыть их - то пользователь может напортачить. В Clean не может - система типов даст по рукам.

То есть, в чем разница подходов:

Haskell - вводим абстракцию «нечистого вычисления» внутрь которого забито состояние вместе с обрабатываемой информацией, для работы «обычных» ф-й на таких «загрязненных» данных приходится эти ф-и лифтить.

Clean - точно отделяем состояние от данных. В итоге грязь остается в самом состоянии, с данными работаем как с обычными данными, ведь грязь отделена.

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

скорее, эта функция имеет тип readByte: *Port -> (Integer, *Port).

А функция getLine (:: IO String в хаскеле) имеет тип *World -> (String, *World)? Если fst :: (a, b) -> a, то fst . getLine :: *World -> String, или разбирать тупл с уникальным типом нельзя?

Не понял, каким специальным образом?

Уникальные типы же он особым образом обрабатывает, и во время тайпчека и во время компиляции, а ближайший аналог в хаскеле, IO, тайпчекается как обычный ADT, но тоже особым образом обрабатывается компилятором.

Скажи ещё, что потраченные на вычисление функции (кило)ватты — тоже сайд-эффект функции.

Автор же сам пишет, что «pure functions are only pure at a certain level of abstraction». На этом уровне нам, как правило, совершенно безразлично, сколько ресурсов было затрачено на вычисление и сколько потом вернулось.

А функция getLine (:: IO String в хаскеле) имеет тип *World -> (String, *World)?

Да, именно так. То есть на практике кроме *World есть еще несколько типов, например может быть специальный такой тип *stdOut. Семантически, понятно, особой разницы с *World нету - это просто для удобства.

Если fst :: (a, b) -> a, то fst . getLine :: *World -> String

Именно так.

или разбирать тупл с уникальным типом нельзя?

Можно, конечно. В этом и суть. Но если мы напишем такую ф-ю (которая просто выкидывает *World и вернет один String), то это значит, что мы наш *World потеряли - он ведь уникальный, то есть на него была единственная ссылка. Эта ссылка ушла в ф-ю и оттуда не вернулась, а больше ссылок нет :)

Так что если мы уникальный тип не вернули ничего больше мы с ним сделать уже не сможем - например если бы вместо *World был бы *File, то мы бы уже даже не смогли этот файл закрыть. И записать/считать тоже ничего бы уже не смогли. А учитывая, что программа на Clean - это функция с типом *World -> *World и мы обязаны *World вернуть, терять его так мы не можем.

Уникальные типы же он особым образом обрабатывает

Почему? Не обрабатывает. Вот возьмем какой-нибудь ЯП на базе лямбда-исчисления с глобальными переменными (чтобы можно было там описать хвостовые вызовы). Допустим, у нас ЯП без оптимизации хвостовых вызовов. Мы пишем его семантику. Пишем компилятор. И тут видим - ба! Да можно ведь оптимизировать хвостовые вызовы! И вносим эту оптимизацию. Семантика меняется? Нет. Так и в Clean - особый способ компиляции уникальных типов _не влияет_ на семантику. Вместо мутирующих операций мы могли бы производить копирование, ничего не оптимизируя. И получали бы тот же результат, и все бы работало прекрасно. Мы, конечно, не смогли бы на реальном железе скопировать какой-нибудь *World... но в теории у нас железо нереальное, с бесконечным объемом памяти и неограниченным временем вычисления :)

С другой стороны, программа на хаскеле без специальной обработки ИО не делала бы вообще ничего, даже на астральном железе с астральными возможностями :)

Почему? Не обрабатывает.

То есть единственное что делает компилятор в связи с уникальными типами - это бьет по рукам, если мы шарим мутируемый объект. Это все.

Так и в Clean - особый способ компиляции уникальных типов _не влияет_ на семантику.

Но само их наличие это дополнение - и к синтаксису и к семантике, так?

То есть единственное что делает компилятор в связи с уникальными типами - это бьет по рукам, если мы шарим мутируемый объект. Это все.

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

Но само их наличие это дополнение - и к синтаксису и к семантике, так?

как и любое нетривиальное усложнение системы типов :)

Если бы это не меняло семантику, то уникальные типы можно было бы выразить в том же хаскеле.

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

Каким образом, например?

Типизированное и нетипизированное лямбда исчисления

Ввод типизации меняет семантику. Ввод оптимизации в Clean - нет. В этом разница.

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

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