Надо думать

Может, что-нибудь из TH и квазиквот поможет?

Здесь уже ничего не поможет...

Наверное, надо доказать (от противного), что такая конструкция не возможна

Кстати, такой вариант, судя по всему, тоже должен ломаться: (g x, g x) (просто пара значений этой особенной функции)

Кто уже прочёл TAPL и сможет?

Ну вот как-то так: пусть такая конструкция возможна и f=...g...g... не компилируется. Тогда рассмотрим const id f, в ней второй аргумент не используется, вроде, должен отбрасываться. То есть, скомпилируется. Примерно так...

Ну вот как-то так: пусть такая конструкция возможна и f=...g...g... не компилируется. Тогда рассмотрим const id f, в ней второй аргумент не используется, вроде, должен отбрасываться. То есть, скомпилируется. Примерно так...

в строгом языке или ленивом?

Я не очень понимаю, но кажется, ленивость не должна тут влиять

Вопрос на засыпку. Возможно ли в Haskell сделать так, чтобы при каждом вызове некоей полиморфной функции программист обязан был передавать всегда новый тип, иначе - ошибка компиляции? Интерес академический.

Действительно, интересная задача. Вспомнил, что видел в доках Dotty что-то похожее, там была реализация стейт-машины в компайл тайме, вроде это что-то похожее. Но это не Haskell. http://dotty.epfl.ch/docs/reference/erased-terms.html

Вот было бы круто, если бы такое расширение было в GHC. Можно было бы создавать функции вроде resource <- aquireResource resourceDef и closeResource resource и не бояться, что какая-то из функций вызовется дважды. Но это описание уж очень смахивает на то, что @qnikst про линейные типы рассказывал

Вот было бы круто, если бы такое расширение было в GHC. Можно было бы создавать функции вроде resource <- aquireResource resourceDef и closeResource resource и не бояться, что какая-то из функций вызовется дважды. Но это описание уж очень смахивает на то, что @qnikst про линейные типы рассказывал

а resourcet? вроде он беспокоится за ресурсы

линейные типы такого прям не дадут

давай разбираться

пусть у нас будет магическая функция foo

foo 1 можно в двух местах проекта написать?

это осмысленно?

можно ли написать foo (op a b)

но видимо функции пофиг на значение, ей только тип важен?

вообще ничего не мешает функцию заделать идемпотентной

если только тип, то как-то через прокси

Не, погодите-ка. Это компилятору, получается, надо обнаружить одинаковые вычисления. А это - заявка на решение проблемы останова. Так что не получится

хранить set типов на которых вызвано, и mvar

при вызове проверять вызывалась ли, и если да то noop

дёшево и сердито

Это в рантайме

тут нету вычислений, не важно ж значение (наверное)

нас попросили один раз для типа

Значение, в общем случае, не важно, да

А компилятор энергично типы проверяет? Можно на типах сэмулировать ленивость?

нет

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

Не, погодите-ка. Это компилятору, получается, надо обнаружить одинаковые вычисления. А это - заявка на решение проблемы останова. Так что не получится

А поясни. Я не очень понимаю, как это связано

т.е. если есть какая типофамилия сопоставляющая скажем Int и тип, то можно сделать что она будет объявлена один раз

для каждого типа, поможет ли это хз

что если иметь HSet + HList c типами, что были вызваны? ну проверять есть ли такие типы в коллекции или нет

А компилятор энергично типы проверяет? Можно на типах сэмулировать ленивость?

Сразу же вопрос: на тьюринг-полной системе типов можно эмулировать любую вычислительную функцию. А что с ленивостью?

вообще какое-то желание поднять линейные типы на уровень выше

вообще какое-то желание поднять линейные типы на уровень выше

на каинды?

ага, которых нету уже

насколько я знаю теории в этом направлении нету

но вообще на XY похоже

ага, которых нету уже

как это?

все тип

Это еще 8 лет будет продолжаться, все норм :)

Или я путаю?

я не понимаю математический смысл этого. ведь f x ... f x ≡ y ... y where y = f x. то есть эти ситуации неотличимы

все тип

хм, но поднимать все равно надо через плагины или синглтоны?

Ну если бы была ленивость на типах, мы могли бы сделать что-то типа Const a b, где b лениво тайпчекался. Тогда туда можно было бы запихать f=....g....g..., то есть в таком лениво тайпчекере можно было бы обойти ограничение на единичность.

Значит ли это, что есть некая семантика, которая невыразима в системе типов?

наверно, можно через TH в компайлтайме (рантайме TH) записывать каждый тип в глобальную переменную

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

Значит ли это, что есть некая семантика, которая невыразима в системе типов?

это значит, что в твоей хотелке нет семантики

индексация временем :D тогда точно никогда не совпадет

Хе-хе

это значит, что в твоей хотелке нет семантики

Я не понимаю. Что мне помешает проапдейтить GHC, чтобы при разборе некоторого AST он смотрел, есть ли такое AST уже или нет.

Я не понимаю. Что мне помешает проапдейтить GHC, чтобы при разборе некоторого AST он смотрел, есть ли такое AST уже или нет.

всё ещё нет семантики

Я не понимаю. Что мне помешает проапдейтить GHC, чтобы при разборе некоторого AST он смотрел, есть ли такое AST уже или нет.

ты же можешь анотировать аст через кофри комонаду

и потом сравнивать только аннотации

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

a monadplus is just a near-semiring in the category of endofunctors what the problem?

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

я думаю, она в каком-то смысле корректна, но её невозможно решить и от неё нет пользы

Prove it!

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

а потом чтд или не чтд

Prove it!

я выше писал, что в семантике Хаскеля f x + f x и y + y where y = f x эквивалентны. следовательно, ты можешь решить свою задачу в рамках AST, но не в рамках Хаскеля

Ну ладно. Хотя, может, тут новый синтаксис можно было бы ввести

ERROR: S client not available

я выше писал, что в семантике Хаскеля f x + f x и y + y where y = f x эквивалентны. следовательно, ты можешь решить свою задачу в рамках AST, но не в рамках Хаскеля

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

Сразу же вопрос: на тьюринг-полной системе типов можно эмулировать любую вычислительную функцию. А что с ленивостью?

Если система ттюринг-полная, то на ней можно смоделировать присваивание ячейке и проверку ячейки на значение, так? Ну так пусть в начале работы этой Штуки будет создана ячейка с "0", а первое использование функции проверит, что в этой ячейке. Если 0, то запишет туда 1, если не 0, то выдаст ошибку компиляции. Всё просто ;))

Если система ттюринг-полная, то на ней можно смоделировать присваивание ячейке и проверку ячейки на значение, так? Ну так пусть в начале работы этой Штуки будет создана ячейка с "0", а первое использование функции проверит, что в этой ячейке. Если 0, то запишет туда 1, если не 0, то выдаст ошибку компиляции. Всё просто ;))

выдать ошибку компиляции во время исполнения?

индексация временем :D тогда точно никогда не совпадет

но это не точно

а можно узнать саму задачу-то?

Вопрос на засыпку. Возможно ли в Haskell сделать так, чтобы при каждом вызове некоей полиморфной функции программист обязан был передавать всегда новый тип, иначе - ошибка компиляции? Интерес академический.

Это вся задача, собственно

а можно узнать саму задачу-то?

^

это максимум ката какая-то из разряда because I can

это может быть решением какой-то задачи, но не самой задачей

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

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

это не решит проблему

это не решит проблему

Почему? Это не даст нам вызвать функцию дважы и даст возможность менять тип аргумента (инкрементить нат в фантоме там)

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

Foo xs = Foo (forall a. a NotIn xs => a -> Foo (a:xs)) и такую штуку линейно еще

тогда взлетит

newtype F (n :: Nat) = F { runF :: Proxy n -> Int -> (F (S n), String) }

и вот в скоуп, где нужна эта функция, передать линейно F Z

ну здесь только один домен для типов

так не интересно

то, что выше это в общем-то тоже самое

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

я правильно понял, что tasty не умеет свои группы параллельно гонять, а tasty-hedgehog заворачивает только отдельные кейсы, но не [параллельные] группы?

я правильно понял, что tasty не умеет свои группы параллельно гонять, а tasty-hedgehog заворачивает только отдельные кейсы, но не [параллельные] группы?

второе да. первое — было бы странно

почему странно? деревья там только для группировки

почему странно? деревья там только для группировки

да, было бы странно, если бы не умел параллелить

Features: * Run tests in parallel but report results in a deterministic order хех.. первым же пунктом.

Что почитать по Haskell, если самые азы как-то осилил, но того, о чём в это чате пишут, до сих пор не понимаю?

я тоже мало чего понимаю. Это норм. ☺️

Бездонный язык

И нет желания начать понимать?

Изучаю Haskell больше трех лет и тоже не все понимаю, что пишут в этом чате. Вообще, понимание этого чата не является показателем понимания языка.

И нет желания начать понимать?

"хочу купить козу - не имею возможности.."