@haskellru - страница 696 - Telegram web archive

A64m

НА ЭТЕ

Евгений

А что, кстати, случилось с лексах?

Andrei

разрабатывается

Andrei

стек научилась

Alexander

ну вот регрессия за регрессией

Dmitry

{-# language ViewPatterns #-} module Blah where import System.Random data Grid = Grid { size :: (Int, Int) , blah :: String } pickPoint :: RandomGen gen => gen -> Grid -> (Int, Int) pickPoint gen grid = (x, y) where (w, h) = size grid ((`mod` w) -> x, gen1) = next gen ((`mod` h) -> y, _gen2) = next gen1 Blah.hs:15:13: error: Variable not in scope: w :: Int | 15 | ((`mod` w) -> x, gen1) = next gen | ^ Blah.hs:16:13: error: Variable not in scope: h :: Int | 16 | ((`mod` h) -> y, _gen2) = next gen1 | ^ Exit code: 1

Dmitry

вот это было неожиданно

Dmitry

https://ghc.haskell.org/trac/ghc/ticket/14293

Dmitry

написал через first

分解物質

{-# language ViewPatterns #-} module Blah where import System.Random data Grid = Grid { size :: (Int, Int) , blah :: String } pickPoint :: RandomGen gen => gen -> Grid -> (Int, Int) pickPoint gen grid = (x, y) where (w, h) = size grid ((`mod` w) -> x, gen1) = next gen ((`mod` h) -> y, _gen2) = next gen1 Blah.hs:15:13: error: Variable not in scope: w :: Int | 15 | ((`mod` w) -> x, gen1) = next gen | ^ Blah.hs:16:13: error: Variable not in scope: h :: Int | 16 | ((`mod` h) -> y, _gen2) = next gen1 | ^ Exit code: 1

это в ghc-8 сделали отчёт ошибок как у rustc?

Anonymous

8.2

Dmitry

сделали как у clang

Anonymous

да, мне тоже кажется что оно не настолько дружелюбно как у rustc

Alexander

у rustc есть explain

Alexander

тут нету

Denis

второй баг в ghc зарепортили за пару недель :E

Denis

BugInBug - секретное расширение, включено по дефолту в новых версиях

Alexander

@catamorphism а что там у вас нашлось?

Alexander

у нас как-то все слишком гладко пока..

Denis

https://ghc.haskell.org/trac/ghc/ticket/14338 https://ghc.haskell.org/trac/ghc/ticket/14434

Alexander

14434 круто

Alexander

интересно как у нас ничего такого не выловилось

Denis

мы 14338 сильнее поели, если честно

Denis

у нас зато на 7.10 был гладкий переход, а вы чего-то там наловили

Mi Shа

Что отрекомендуете почитать по конечным автоматам?

murad

Да, я бы тоже хотел ознакомиться с этой темой.

murad

Кстати, как тема «конечных автоматов» практически применяется в «программировании»? Кто-то может дать доходчивый ответ?

Кабачок

Бывает пишем конечные автоматы

Ignat

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

Кабачок

Иногда даже типами кодируем очередность шагов

A64m

А TTG тем временем ревертнули

Alexander

:(

A64m

опять из-за бага в 8.0

Евгений

Кстати, как тема «конечных автоматов» практически применяется в «программировании»? Кто-то может дать доходчивый ответ?

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

Евгений

Собственно в реальной практике больше они никак не используются :) Практически везде где мог бы быть конечный автомат проще сунуть регулярку

A64m

новый констант фолдинг тоже из-за бага в 8.0 не билдится

Кабачок

Хмм, в Котлине сопрограммы компилируются в конечные автоматы.

Ignat

в крестах тоже

Ignat

(на данный момент, во всяком случае)

Alexander

мне нужна помощь идрисоводов

Alexander

https://gist.github.com/qnikst/2968ab573018fae42ac928e10c467dce <- что тут более человечески можно сделать?

Alexander

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

Alexander

на то, как это запускается на смотрите, там чужой код

Alexander

@catamorphism ты вроде в таких штуках шаришь?

Denis

попинай с утреца

Denis

а то спать пора

Alexander

ну вот

Alexander

ок

Alexander

@catamorphism может пока не лег не скажешь можно ли так сделать

Alexander

у меня есть X (Sing S) и Y S я хочу функцию X s -> Y такой чтобы в Y s == fromSing того что из s

Alexander

это как-то вообще возможно?

Denis

Ничего не понял

Denis

на коде с типами существующими можешь вопрос задать?

Alexander

вон в гисте constr

Alexander

60-62 строки

Denis

https://gist.github.com/qnikst/2968ab573018fae42ac928e10c467dce#file-idris-hs-L61 почему ты считаешь что это unsafe?

Alexander

в 61 нету никакой гарантии, что я делаю то, что надо я могу написать = S Adding m

Denis

я то ли причину не понял, то ли оно сейф

Alexander

т.е. это получается trusted base, код которому я доверяю, но доказательств что он правильный нет

Denis

гарантия будет если при конструировании Next ты её зафорсишь

Denis

не понял какие стейты правильные, а какие нет

Denis

короче проблема в том, что я не понимаю что ты пытаешься сделать

Alexander

constr :: NextState x -> Maybe State constr (Next SSubtracting m) = Just (S Adding m)

Alexander

я могу так написать

Alexander

мне интересно могу ли я сделать, что-то чтобы это не тайпчекалось

Alexander

но почему-то мне кажется что это принципиально невозможно..

Denis

т.е. ты хочешь чтобы EditorState справа и слева был одинаковый?

Alexander

да

Denis

ну он и так будет одинаковый, т.к. ты там делаешь fromSing s, а s слева захватываешь

Denis

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

Alexander

ну т.е. получается тут trusted метод

Denis

а иначе тебе нужно чтобы у тебя в типе функции перед стрелкой и после был этот тип

Alexander

я в общем-то не против

Denis

у тебя справа от стрелки нет

Alexander

угу

Denis

ну т.е. у тебя correct by implementation

Denis

если не даешь юзерам писать такие функции, то и думать больше не о чем

Alexander

ну и отлично

Denis

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

Denis

но это уже специально надо стараться