> Что такое "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..]

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

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

упс, нет

только хотел написать ай донт финк соу

но первое редуцируется во второе же

а второе в первое — нет

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

например, 1+1+2/0 = 2+2/0 так?

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

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

например, 1+1+2/0 = 2+2/0 так?

возможно, стоить разделять "равенство по (частичной) редукции" и "равенство по значению (нормальной форме)"

думаю, примерно такой же смысл вкладывается в понятия интенсиального и экстенсиального равенств?

а как вам вот такой терм 1:[1,1..] ++ [3]

равен он [1,1..]? и если да, то в каком смысле и как это определить и доказать равенство?

равен он [1,1..]? и если да, то в каком смысле и как это определить и доказать равенство?

равен, почему нет

доказать легко: докажем, что для любого наперёд заданного n -> n-ые элементы списков равны

значит равны и сами списки

а если не вставлять костыли специально для списков?

можно определить так, что для любой редукции a' формулы a существует последовательность шагов редукции b в a' и наоборот

нет, тоже не то

сравнить нормальные формы, вычисленные до любой конечной глубины?

WHNF-n

а если не вставлять костыли специально для списков?

если интересно, глянь пакет http://hackage.haskell.org/package/infinite-search-0.12/docs/Data-Searchable.html

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

главное придумать, что выбрать за Set

хочется сделать Set = мно-во пар элементов двух этих списков, и соотв-нно натравить предикат "а есть ли хоть одна пара не вида (x, x)"

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

А есть статьи или книги которые всю эту теорию объясняют?

This module is based on the paper "Exhaustible sets in higher-type computation" by Martin Escardo

Haskell — невозможное возможно? / Хабрахабр https://m.habrahabr.ru/post/201446/

я в text уже натыкался на кривые rewrite rules

Может string не так и плох?:)

bos иногда излишне оптимистичен

там хоть кто-то этот баг довел до сведения разработчиков? это всё-таки ахтунг

что я находил - довел в тот же день

с патчес

и его прям в тот же день приняли

про то, что выше, не знаю

multRandomNumbers rands prev = case rands of (x:xs) -> curRand : multRandomNumbers xs curRand where curRand = prev * ( 0.995 + ( x * 0.01 ) )Я правильно понимаю, что на x в третьей строке ругается из-за того, что подразумеваютcя матчи, в которых x нет? Что делать в таких случаях? Можно объявить локальную функцию для конкретного матча?

let?

multRandomNumbers rands prev = case rands of (x:xs) -> let curRand = curRand = prev * ( 0.995 + ( x * 0.01 ) ) in curRand : multRandomNumbers xs curRand

[] -> [] тут по-любому возможен, явно или неявно. Хоть список и бесконечный в конкретном случае

Точно, забыл, что им так можно пользоваться

а чего нельзя сразу rands сматчить в аргументе?

Вау, и так можно? ☺

multRandomNumbers (x:xs) prev = curRand : multRandomNumbers xs curRand where curRand = prev * ( 0.995 + ( x * 0.01 ) )

а чо так сложно?

r = 0:(zipWith nextRand randoms r) where nextRand x prev = prev * ( 0.995 + ( x * 0.01 ) )

0 - начальный элемент, randoms - список случайных чисел

zip/zipWith я ещё не осилил, хотя часто встречаю; пойду курить, чо оно такое

Хмм, а почему так не компилится? multRandomNumbers :: [Float] -> Float -> [Float] multRandomNumbers (rand:otherRands) prev = curRand : multRandomNumbers otherRands curRand where curRand = prev * ( 0.995 + ( rand * 0.0126315789473684 ) ) realRand = case curRand of <0.8 -> 0.8 >1.2 -> 1.2 _ -> curRand

Ну если не компилится то там написано почему

parse error on input ‘->’

case в where юзать нельзя, что ли?

<0.8 в case нельзя

А чо можно?

Патерн матчинг можно

zip/zipWith я ещё не осилил, хотя часто встречаю; пойду курить, чо оно такое

ты язык по гуглу что ли учишь?:) возьми нормальный учебник с let ты не знаком, с zip не знаком, зато уже код с монадами пишешь (вчера было)

ты язык по гуглу что ли учишь?:) возьми нормальный учебник с let ты не знаком, с zip не знаком, зато уже код с монадами пишешь (вчера было)

Я все языки так учил: понадобилось чото — нашёл в справке, даже до интернетов ещё. Не вижу смысла муштровать кучу теории, хоть это и полезно (в теоркат въезжаю потихоньку). Тем более, zip, как вижу — сахарок какой-то, раз получилось без него, просто велосипедно А без монад реальной жизни нет, только в ghci что-то считать, смысл их откладывать? ☺

вот глянь https://anton-k.github.io/ru-haskell-book/book/4.html

насчёт let и пр.