Но это конечно не нормально

ого, сглаживание

not my screenshot

а разбор будет?

почему так

Неправильный rewrite rule в text

http://www.parsonsmatt.org/overcoming-records/

Почему в стейте постоянно начальное значение? Я что-то делаю не так? currentSpeed :: Float -> String currentSpeed i = "set speed " ++ ( show $ evalState ( modSpeed i ) initSpeed ) modSpeed :: Float -> State Float Float modSpeed i = do old <- get let new = ( old - 1) put new return new initSpeed = 1

Почему оно должно меняться?

Ну я же путаю новое, или?

Ну путаешь, а потом ничего с ним не делаешь

А что с ним делать нужно? Этот стейт каждый раз пересоздаётся, получается?

Разумеется

А как еще?

Это же чистая функция

Он не то что пересоздается, тут вообще переменных нет никаких

погодите, что значит начальное значение?

Как тогда запоминать? Синглтон нужен?

на выходе evalState должен быть 0

Какой синглтон?

синглтон? :D

глобальная переменная штоле?

ну да, а я так понимаю автор ожидает, что много раз если вызвать, то будет 0, -1, -2, etc

да, видимо, так и есть

Если уж очень-очень хочется, то делается это через IORef

но лучше просто не делать так и не хотеть так

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

Вот если currentSpeed :: Float -> String, то это значит, что ты передаешь число, а получаешь строку на выход

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

потому что это *функция*

а не процедура

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

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

https://hackage.haskell.org/package/MonadRandom-0.5.1/docs/Control-Monad-Random-Strict.html

так случайные числа можно же на стейте как раз написать?

дык, если нужно просто знать предыдущее число, почему бы не передавать его аргументом?

я даж писал ?

как упражнение

так случайные числа можно же на стейте как раз написать?

Rand и есть State

просто хелперов побольше для рандомной генерации

Я же правильно понимаю, что а хаскеле тру зависимых типов никогда не будет из-за боттома, а если и будут, то доказывать ничего будет нельзя? Да и на core это как-то не кладется, сплошные хаки типа symbolVal будут

Агда давно не обновлялась чет, идрис не продакшен реди (да че продакшен, тайпчек фильтра по вектору выжирает 10 гигов и виснет), хоть нравится мне он больше всех. Есть ли какие-то популярные хаскель-подобные языки с завтипами? Хочу в эту тему углубиться, но вижу только coq и изабеле. Lean еще понравился

Слышал, что jetbrains что-то делали

> давно не обновлялась

Месье требовательный

Касательно зависимых типов в Haskell, доказывать будет можно, но пруфы нужно будет запускать в рантайме (чтобы исключить боттом).

Если пруф-тёрм высчитается и не будет bottom, то все доказано нормально. Это, конечно, удар по производительности, но не deal-breaker.

Но в качестве proof assistant он не сгодится все равно, конечно.

Точнее, будет неудобно, как ни крути.

Agda и Coq нормальные, если именно для доказательств.

А именно для программирования готовых хороших решений нет. Недавно видел, что John Wiegley генерирует Haskell на Coq. В итоге все доказательства на Coq, а компиляет это GHC, и работает оно хорошо.

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

в Изабелле нет завтипов

А, хм, на сайте у них просто последний релиз то ли 2014, то ли 2016)

F*

(раз в неделю этот вброс)

Я же правильно понимаю, что а хаскеле тру зависимых типов никогда не будет из-за боттома, а если и будут, то доказывать ничего будет нельзя? Да и на core это как-то не кладется, сплошные хаки типа symbolVal будут

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

Semigroup уже суперкласс Monoid в HEAD

123456

ну, вы все поняли?

а что не так?

Флаг оптимизации меняет вывод программы с True на False

оуч...!!

Флаг оптимизации меняет вывод программы с True на False

Ну тип правила редукции меняются

Хотя по normalization theorem есть есть нормализация, то она единственна

Но тут побочные эффекты!

Порядок редукции не должен ничего менять там, это был неправильный rewrite rule в библиотеке.

Какие побочные эффекты, в length и filter?

В print

И что?

Теперь print должен менять то, что ему сказали распечатать, в зависимости от порядка редукции?

А можно подробнее объяснить как рулы так повлияли на результат?

Порядок редукции не должен ничего менять там, это был неправильный rewrite rule в библиотеке.

> неправильный rewrite rule Что такое "rewrite rule в библиотеке"

Типа, "а ладно, применю not, все равно побочные эффекты"

> Что такое "rewrite rule в библиотеке" в Haskell можно кастомные оптимизации прописывать. Определил ты map и добавил правило, что map f . map g = map (f . g)

И компилятор будет в отдельной фазе оптимизации применять эти правила

А можно подробнее объяснить как рулы так повлияли на результат?

Не знаю, но в баг-репорте конкретное правило нашли, которое приводило к этому, можешь поискать.

Звучит психоделично, это же exstentional equality

В смысле? Вполне universal

Опечатался

для любого f, g

Так тогда вроде не отличается от других оптимизаций, просто можно эксплойтить законы функций, которые нам известны, а компилятору — нет.

Экстенсиональное равенство это такой факап в теории типов, который приключился с мартином лёфом при первой попытке изобрести MLTT

http://reasonablypolymorphic.com/blog/modeling-music

Добавление в теорию типов правила "x: a = b |= a редуцируется в b" делает теорию типов противоречивой, то есть разрушает всякую корректность

Экстенсиональное равенство это такой факап в теории типов, который приключился с мартином лёфом при первой попытке изобрести MLTT

Это факап не концептуальный, а потому что тайпчекер для этого сложно сделать

(forall x. f x = g x) => f = g это прямо определение функционального равенства

вопрос только в том, делать это аксиомой или доказывать на case-by-case basis

откуда противоречивость тут может взяться?

> "x: a = b |= a редуцируется в b" вот это я вообще понять не смог

возьмем a = 2 и b = 1 + 1, разве можно сказать, что a редуцируется в b? Наоборот в данном случае. (Либо я неправильно правило прочитал)

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

но тогда не удастся доказать равенство [1,1..] и 1:[1,1..]

потому что эти термы не имеют нормальных форм, хотя очевидно экстенсиалоьно равны

но тогда не удастся доказать равенство [1,1..] и 1:[1,1..]

эти два выражения синтаксически совпадают (после рассахаривания)

эти два выражения синтаксически совпадают (после рассахаривания)

упс, нет