mk строит дерево высотой n (==) выполняет поэлементное сравнение значений, не пытаясь сократить до сравнения адресов. Ну, как бы, логично получить такой эффект. Постулируется, что `x == x` для любых значений любых типов? Даже если рукожопо определить инстанс тайпкласса Eq? А если сравнивать бесконечные списки? let xs = [1..] in xs == xs, то вообще всё будет ужасно?
Ну и вопрос, а есть ли - и могут ли вообще быть - ленивые языки, которые пригодны к вот таким символьным вычислениям? Ведь, даже если мы строим пышное дерево, вырожденное до вот такого списка, то можем сделать так, чтобы ленивые санки там были разные. let x = mk (n-1) in let y _ = x in P (y 1) (y 2)
Мы можем сравнивать указатели. Но без гарантий от языка, что равные (структурно, или как ещё) вычисления получают одинаковые указатели, mk n == mk n будет вычислять обе стороны и проходить по экспоненциально большому пути вычисления сравнения.
Я почему то думал, что достаточно гарантии обратного: "одинаковые указатели -> равные вычисления", но ваш контрпример это опровергает...
Хотя может можно просто сравнивать такие вещи на этапе компиляции, сравнивая AST и заменяя mk n == mk n на константу true, если в дереве нет ничего с побочными эффектами (если это вообще _всегда_ можно понять).
Я, может, наивную вещь скажу, - поскольку не слежу за судьбой компиляторов хаскелла.
Теоремы об эквивалентности прагматически можно разделить на два класса:
- эвристики - записанные авторами компилятора или библиотеки заранее (неважно, вручную они найдены, или один раз натравили какой-то инструмент для автоматического вывода)
- все остальные всевозможные утверждения, справедливые для конкретной программы.
Насколько много у компилятора есть времени и сил, чтобы искать эти новые утверждения, чтобы они стали эвристиками ad hoc? Потому что находить их все - чую, дело пахнет комбинаторным взрывом.
Ну и, скажем, написали мы функцию mk, которая строит дерево-колбасу. Да, мы можем задуматься, а какими свойствами обладает эта колбаса, как для неё строить типичные операции - сравнения, отображения, ещё чего-то... А потом выяснится, что у нас глубина рекурсии всего 3-4, и количество обращений к ним умеренное, и самые тупые неоптимизированные реализации нас вполне устраивают. Почему тогда компилятор должен был пытаться выводить свойства колбасы?
( ... )
Кстати! Русские авторы с отсылками к русским авторам, на русской конференции... на английском языке. А на русском того же самого нет? Моё гугл-фу оказалось бессильно, нашёл только другие работы их же.
Статья интересная, но возможно, что я понял её неправильно. Суперкомпиляция позволяет рожать и применять теоремы равенства, это всё хорошо... но когда компилятор должен остановиться и начать уже компилировать, а не исследовать код?
Для популярной (например, стандартной) библиотеки автоматический вывод и создание ёмкого (а то и исчерпывающего) каталога правил переписывания - дело полезное. Делается единожды. Ещё и библиотеку можно построить так, чтобы упростить жизнь анализатору кода.
А в конкретной программе, да ещё и оснащённой всякими ловушками ("а давайте mk сделаем на последовательности Коллаца")?
Потому и задал свой наивный, но частично риторический вопрос.
Вот, пойду читать диссертацию Клиффорда Клика, начинается она весело, авось не усну :)
Просто, когда какая-то тема обозначена коротким мазком, sapienti sat, то вот те, кто не sapienti, - я, например, - оказываются очень даже не sat, но заинтригованы.
Хотя, в принципе, для произвольных структур можно ввести теоремы "если одни санки встречаются дважды..."
что-то типа ((a b) , (a b)) == (let ab = (a b) in (ab , ab))
где условие сопоставления - "мы по-быстрому знаем, что a==a' и b==b'" - потому что это санки с одинаковым адресом, или потому что это какие-то простые значения, или мы ещё раньше нашли равенство...
Тогда реализация тайпклассов всяких почленных операций для структур с небольшим количеством полей будет сперва делать проверку на быстрое равенство, а затем заниматься рекурсией.
С большим количеством полей - боюсь, тоже можно сделать заподло:
data Tree = Node Tree Tree Tree .... (100 штук) | Leaf some
и заставлять на каждом листе делать проверки всех со всеми за квадратичное время "а можем ли мы здесь что-то кешировать", - особенно, если пользователь мамой клялся, что все элементы по задумке разные, - это получится пессимизация вместо оптимизации.
(==) выполняет поэлементное сравнение значений, не пытаясь сократить до сравнения адресов. Ну, как бы, логично получить такой эффект.
Постулируется, что `x == x` для любых значений любых типов? Даже если рукожопо определить инстанс тайпкласса Eq?
А если сравнивать бесконечные списки? let xs = [1..] in xs == xs, то вообще всё будет ужасно?
Ну и вопрос, а есть ли - и могут ли вообще быть - ленивые языки, которые пригодны к вот таким символьным вычислениям?
Ведь, даже если мы строим пышное дерево, вырожденное до вот такого списка, то можем сделать так, чтобы ленивые санки там были разные.
let x = mk (n-1) in let y _ = x in P (y 1) (y 2)
Reply
let xs = [1..] in xs == xs технически может сравнить санки (их адрес), разве нет?
Reply
Технически может сравнить санки, но для этого нужны гарантии аксиоматики операции сравнения.
Обычно из идентичности следует равенство, но вот в си, например, float NaN не равен сам себе.
Ну и какой-нибудь злобный дурак может устроить wish you happy debug, определив для своего типа равенство хаотичным способом
Reply
Они есть в случае Хаскеля.
Reply
Reply
Прошу прощения, не указал, что отвечал на эту строку из комментария kodt_rsdn:
> А если сравнивать бесконечные списки? let xs = [1..] in xs == xs, то вообще всё будет ужасно?
предлагая как их возможно сравнивать
Reply
Reply
Я почему то думал, что достаточно гарантии обратного: "одинаковые указатели -> равные вычисления", но ваш контрпример это опровергает...
Хотя может можно просто сравнивать такие вещи на этапе компиляции, сравнивая AST и заменяя mk n == mk n на константу true, если в дереве нет ничего с побочными эффектами (если это вообще _всегда_ можно понять).
Reply
Хакнуть сравнение AST тоже несложно.
Достаточно подмешивать мусорные аргументы, которые ни на что не влияют.
mk' n r = if n == 0 then V "x" else let x = mk' (n-1) r in T x x
test n = (mk' n 1) == (mk' n 2)
Reply
;)
Reply
Я, может, наивную вещь скажу, - поскольку не слежу за судьбой компиляторов хаскелла.
Теоремы об эквивалентности прагматически можно разделить на два класса:
- эвристики - записанные авторами компилятора или библиотеки заранее (неважно, вручную они найдены, или один раз натравили какой-то инструмент для автоматического вывода)
- все остальные всевозможные утверждения, справедливые для конкретной программы.
Насколько много у компилятора есть времени и сил, чтобы искать эти новые утверждения, чтобы они стали эвристиками ad hoc? Потому что находить их все - чую, дело пахнет комбинаторным взрывом.
Ну и, скажем, написали мы функцию mk, которая строит дерево-колбасу. Да, мы можем задуматься, а какими свойствами обладает эта колбаса, как для неё строить типичные операции - сравнения, отображения, ещё чего-то... А потом выяснится, что у нас глубина рекурсии всего 3-4, и количество обращений к ним умеренное, и самые тупые неоптимизированные реализации нас вполне устраивают. Почему тогда компилятор должен был пытаться выводить свойства колбасы?
( ... )
Reply
Reply
Статью-то я прочёл.
Кстати! Русские авторы с отсылками к русским авторам, на русской конференции... на английском языке. А на русском того же самого нет? Моё гугл-фу оказалось бессильно, нашёл только другие работы их же.
Статья интересная, но возможно, что я понял её неправильно. Суперкомпиляция позволяет рожать и применять теоремы равенства, это всё хорошо... но когда компилятор должен остановиться и начать уже компилировать, а не исследовать код?
Для популярной (например, стандартной) библиотеки автоматический вывод и создание ёмкого (а то и исчерпывающего) каталога правил переписывания - дело полезное. Делается единожды. Ещё и библиотеку можно построить так, чтобы упростить жизнь анализатору кода.
А в конкретной программе, да ещё и оснащённой всякими ловушками ("а давайте mk сделаем на последовательности Коллаца")?
Потому и задал свой наивный, но частично риторический вопрос.
Reply
Reply
Ну прям неинтересно.
Вот, пойду читать диссертацию Клиффорда Клика, начинается она весело, авось не усну :)
Просто, когда какая-то тема обозначена коротким мазком, sapienti sat, то вот те, кто не sapienti, - я, например, - оказываются очень даже не sat, но заинтригованы.
Reply
Хотя, в принципе, для произвольных структур можно ввести теоремы "если одни санки встречаются дважды..."
что-то типа ((a b) , (a b)) == (let ab = (a b) in (ab , ab))
где условие сопоставления - "мы по-быстрому знаем, что a==a' и b==b'" - потому что это санки с одинаковым адресом, или потому что это какие-то простые значения, или мы ещё раньше нашли равенство...
Тогда реализация тайпклассов всяких почленных операций для структур с небольшим количеством полей будет сперва делать проверку на быстрое равенство, а затем заниматься рекурсией.
С большим количеством полей - боюсь, тоже можно сделать заподло:
data Tree = Node Tree Tree Tree .... (100 штук) | Leaf some
и заставлять на каждом листе делать проверки всех со всеми за квадратичное время "а можем ли мы здесь что-то кешировать", - особенно, если пользователь мамой клялся, что все элементы по задумке разные, - это получится пессимизация вместо оптимизации.
Reply
Leave a comment