Glasgow Haskell Compiler 9.12.1

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

Блин, где сердечко? Тут монады объясняют.

Это не в двух словах, потому что написано синтаксисом Хаскеля. Очевидно, целевая аудитория его не знает, а его оъяснение занимает куда больше двух слов.

Мил человек, а кто из этих трёх может ракеты запускать? Все или только монада? Я даже знаю, какая - IO называется.

Я уже спрашивал, и вроде мне отвечали «да». Можно ли в Хаскеле (например, с помощью монад) добиться следующего поведения:

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

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

Для каждого кода существует максимально быстрая форма выполнения. По её достижение можно закончить.

Но ведь сложение float не коммутативно.

Ещё сложение строк можно вспомнить.

К чёрту коммутативность. Сложение float не ассоциативно.

>>> (0.1 + 0.3) + 0.00001
0.40001000000000003
>>> 0.1 + (0.3 + 0.00001)
0.40001

Так с этой штукой и сделать ничего вроде нельзя.

В этом и суть. Такие типы используются там, где не должно быть возможности создать значение.

P. S. В Си считается, что все функции возвращают значения. Процедура возвращает значение типа void. Чем-то похоже на эту «монаду».

Нет. В Си и си-подобных языках void эквивалентен юниту, то есть () из Haskell.

Ну, во-первых, не существует - она зависит от того, какие данные придут на вход этому коду. Во-вторых, даже если мы примем какое-то определение максимально быстрой формы выполнения, то нужно понять, насколько долго она будет вычисляться и есть ли гарантия хотя бы того, что процесс оптимизации займёт конечное время. Например, мы можем начать вычислять такие a,b,c,N < 100000000000000 что a^n + b^n = c^n.

Если процесс оптимизации займёт конечное время, то устроит ли это конечное время пользователей нашего компилятора? В SBCL, к примеру, цикл оптимизации (основанный на тех самых rewrite rules или чём-то близком) завершается просто по достижению магического числа итераций, допустим, 42. Это означает, что любое изменение в исходнике может привести к тому, что то решение, до которого вчера оптимизатор додумался, сегодня уже не будет обнаружено. Но мы об этом напрямую не узнаем, поскольку компилятор не обо всех удачах и неудачах оптимизации нам сообщает. Мы узнаем об этом только тогда, когда заметим снижение производительности нашей программы. Это делает процесс разработки с таким оптимизатором весьма увлекательным приключением, полным неожиданностей. Уверен, что и в других компиляторах так. И это наводит на мысли, а всё ли в порядке с самим подходом? Да, это инженерная дисциплина, но всё же вопросы остаются.

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

GHC поставляется с пачкой «благословлённых» библиотек, которые по сути составляют стандартную библиотеку языка: base, template-haskell и другие.

Но здесь они не то чтобы прямо привязаны. Просто автор matterhorn так решил, а потом забил.

Стек — это хорошо, но matterhorn кабалом собирается.

Ичо? Сделай stack init и собирай стеком.

ну, тут уже придётся придираться..

как это error? это ведь само по себе чит и не вписывается в систему типов , поэтому надо пытаться рассуждать о том какая система типов была бы уровнем выше и что это было бы в той системе. А это была бы информация об ошибке.

Если процесс оптимизации займёт конечное время, то устроит ли это конечное время пользователей нашего компилятора? … И это наводит на мысли, а всё ли в порядке с самим подходом?

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

О, Денис! Сто лет тебя не встречал на ЛОРе... Любопытно, это потому что я редко захожу или потому что ты редко заходишь?

Это потому что в base постоянно что-то ломают.

Да, и при ограничении по времени уже никакой результат оптимизации не гарантирован. Чем-то напоминает нейронные сети по мутности обещаний. И в любой супер-пупер-компиляции этот вопрос неизбежно всплывёт, если мы захотим построить такой рай на Земле.

Или потому что мы оба редко заходим.

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

Монада - всего лишь мат. абстракция для понятия вычисления. Соответственно, если есть алгоритм, тогда можно и с помощью монад.

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

Как-то непонятно, что делать с этим ответом. Вот в Scheme есть call/cc, который запоминает состояние стека. Если я всё состояние вычисления сложу в одну переменную и научусь делать ей ленивое глубокое копирование, то моя задача на scheme будет решена. Однако это потребует уметь делать ленивое глубокое копирование хеш-таблиц и это требует труда. А я, естественно, хочу, чтобы был максимум готовых инструментов. На CL я тоже пытался решить эту задачу и не особо преуспел.

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

Т.е. я хочу, чтобы я писал любой алгоритм со стеком и структурами данных, размещённых как обычно (в куче, на стеке и т.п.), а волшебный Хаскель позволял мне запоминать его состояния и перезапускать его.

На самом деле в CL есть библиотека Screamer, которая делает примерно это. Просто она это делает неэффективно, используя CPS преобразование, и там код сворачивается в дикую цепочку лямбд, которые жрут кучу, в отличие от обычных вычислений. Хотя я сейчас думаю, может быть иначе это и невозможно сделать…

Есть ещё один способ это осуществить, на уровне ОС. Делаем вычисления и на каждом шаге делаем fork нашего процесса. Одна ветка спит и ждёт, пока понадобится снова, а вторая - продолжает вычисление. Тогда ОС обеспечивать худо-бедно эффективное вычисление, правда, это fork-бомба, потому что на текст в 10 кб понадобится 10 тыс. процессов. Можно ещё по-другому - сохранять core после каждого шага и потом его перезапускать (в линуксе так вообще говоря нельзя, но лиспы так умеют, SWI-пролог умеет и, наверное, ещё кто-нибудь).

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

Т.е. я хочу, чтобы я писал любой алгоритм со стеком и структурами данных, размещённых как обычно (в куче, на стеке и т.п.), а волшебный Хаскель позволял мне запоминать его состояния и перезапускать его.

Глубоко не вникал, но не похоже на правду.

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

Если кто то это сделал, ну будет «волшебный хаскель», если нет, то сначала волшебник den73 пишет эту магию, а потом для других - «волшебный хаскель». Всё банально, как обычно..

как это error?

error нужен чтобы компилятор не ругался на отсутствие метода в классе. Вызываться оно не будет (если кто-то не сделает unsafeCoerce или не сунет туда undefined, но это в любом случае невалидный код будет уже).

это ведь само по себе чит и не вписывается в систему типов

В смысле, не вписывается? Это тип, которому соответствуют 0 возможных значений.

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

мне кажется нет.

какой тип возвращает error и как ты собственно описываешь fmap с помощью error?

fmap :: (a -> b) -> f a -> f b

Qod. Опубликовал исходники компилятора, над которым работаю (комментарий)

какой тип возвращает error и как ты собственно описываешь fmap с помощью error?

error возвращает любой тип. Это bottom, оно принадлежит ко всем типам сразу (кроме unlifted типов, но там свои загоны, не думай об этом).

ghci> :t error "hello"
error "hello" :: a
ghci> :t (error "hello" :: Functor f => f a -> f b)
(error "hello" :: Functor f => f a -> f b)
  :: Functor f => f a -> f b

Человек, у которого годами на аватарке висела картинка про убийство, и в нике написано про ненависть, решил обсудить чьё-то психическое здоровье.

у которого годами на аватарке висела картинка про убийство

Чо за аватарка про убийство? Я не помню уже.

в нике написано про ненависть

Это название трека, игравшего в момент моей регистрации на ЛОРе. Я вообще люблю Noise Unit и прочие Front Line Assembly.

Ещё и провалы в памяти.

Спасибо. Здесь, как ты можешь видишь, error просто имеет любой тип. Это как раз и есть чит. Мы обманываем систему типов чтобы было удобно работать.

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

Значит монаду ты не описал.

Значит, данная конктреная монада не контейнер лишь потому что она и не монада вовсе.

А если бы мы рассмотрели (гипотетическую) систему типов уровнем выше, то это была бы информация об ошибке (при попытке создания экземпляра пустого типа). Т.е. что то вроде Either, которая очевидно, контейнер.

Поплачь.

Но вообще, твои хотелки тут и правда какой-то шизой попахивают.

Понятно, жаль, значит ещё отложу. Но мне кажется, что там всё же был какой-то просвет по сравнению с CL. Если это не зелёные треды, конечно. Хотя, зелёные треды - это одно, а fork и call/cc - это всё же несколько другое.

Т.е. я хочу, чтобы я писал любой алгоритм со стеком и структурами данных, размещённых как обычно (в куче, на стеке и т.п.), а волшебный Хаскель позволял мне запоминать его состояния и перезапускать его.

Используй любые чистые структуры и будет магия. Вместо хеш-таблиц Data.Map.

Здесь, как ты можешь видишь, error просто имеет любой тип. Это как раз и есть чит.

Мы её не обманывали. Bottom является частью системы типов в Haskell. Это последствие существования ленивых вычислений из-за того, что вычисление любого значения потенциально может окончиться бесконечным циклом. Хуже того, в манах написано, что undefined и error вполне могут быть реализованы через бесконечный цикл, и рассчитывать на какое-то поведение тут не слишком разумно.

ghci> import Prelude hiding (error)
ghci> :t error
<interactive>:1:1: error: [GHC-88464]
    Variable not in scope: error

ghci> let error :: String -> a; error s = error s
ghci> :t error
error :: String -> a
ghci> error "hello"
^CInterrupted.

Но «честную» функцию то ты не можешь описать.

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

Значит монаду ты не описал.

Это вполне валидный код. Он просто не будет выполняться :)

Ну ок, эта деталька есть. А как насчёт собственно call/cc? Интересно, для CL есть библиотека с такой вот Data.Map?

А как насчёт собственно call/cc?

https://hackage.haskell.org/package/mtl-2.3.1/docs/Control-Monad-Cont.html

Интересно, для CL есть библиотека с такой вот Data.Map?

gospodeeeeeeeee…

Если сузить вопрос, может ли монада (видимо монада Do конкретно) пройти сквозь вызов функции?

http://blog.sigfpe.com/2008/12/mother-of-all-monads.html

https://github.com/fare/lisp-interface-library/blob/master/pure/hash-table.lisp

Bottom является частью системы типов в Haskell.

Вот это утрвеждение и есть «чит». Вернее не оно, а то что у боттом в хаскеле могут быть значения. Bottom пустой тип. У него нет значений, в том и смысл его. Но если тебе язык позволяет создавать экземпляр любого типа, то ты можешь просто создать что угодно. А система типов как раз не должна позволять создавать что угодно. В этом её смысл изначально.

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

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

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

Что такое «честная функция»?

это реализация без использования значения типа Bottom.

Не уверен на 100%, но кажется, что это не совсем то, что надо, потому что это escape continuations.

Вот это утрвеждение и есть «чит». Bottom пустой тип. У него нет значений, в том и смысл его. Но если тебе язык позволяет создавать экземпляр любого типа, то ты можешь просто создать что угодно.

Нет, это не чит. И нет, не можешь. Существование bottom в Haskell является последствием двух фактов: ленивости вычислений и полноты по Тьюрингу.

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

Coq не полон по Тьюрингу, в нём есть termination checker.

(Да, я знаю про extraction, и что программы в результате могут иметь бесконечные циклы, но это не будет вычислением на самом Coq.)

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

Не, смысл у неё не в этом.

Нет, это не чит. И нет, не можешь.

ну как не могу? я просто напишу

x :: Void
x = error "я значение пустого типа"

Ну хаскель тоже из ML вышел, так-то. Просто он более орочий чем тот же окамл.

ну как не могу? я просто напишу

Ну да, bottom type внезапно содержит bottom. Кто бы мог подумать?

Когда в контексте Haskell говорят про пустой тип, подразумевается, что он пустой за исключением собственно bottom, которое содержится во всех типах вообще.

Хуже того, ты можешь написать вот так:

x :: Void
x = x

Но вычислить это значение ты никак не сможешь в любом случае, поэтому всё как бы ок.

если это не чит, то я как бы сдаюсь

Это не чит, это конструктивная особенность :)

Чит – это unsafeCoerce.

Просто для справки, имея значение типа боттом ты можешь делать любой `unsafeCoerce`. unsafeCoerce излишен (просто писанины меньше).

Если для тебя значение bottom не чит, для меня больше обсуждать эту тему нет смысла, спасибо за дискуссию.