Ну вот как-то так: пусть такая конструкция возможна и f=...g...g... не компилируется. Тогда рассмотрим const id f, в ней второй аргумент не используется, вроде, должен отбрасываться. То есть, скомпилируется. Примерно так...
в строгом языке или ленивом?
Зигохистоморфный
Alexander
Я не очень понимаю, но кажется, ленивость не должна тут влиять
Igor
Вопрос на засыпку.
Возможно ли в Haskell сделать так, чтобы при каждом вызове некоей полиморфной функции программист обязан был передавать всегда новый тип, иначе - ошибка компиляции? Интерес академический.
Действительно, интересная задача.
Вспомнил, что видел в доках Dotty что-то похожее, там была реализация стейт-машины в компайл тайме, вроде это что-то похожее. Но это не Haskell.
http://dotty.epfl.ch/docs/reference/erased-terms.html
Alexander
Вот было бы круто, если бы такое расширение было в GHC. Можно было бы создавать функции вроде
resource <- aquireResource resourceDef
и
closeResource resource
и не бояться, что какая-то из функций вызовется дважды.
Но это описание уж очень смахивает на то, что @qnikst про линейные типы рассказывал
Зигохистоморфный
Вот было бы круто, если бы такое расширение было в GHC. Можно было бы создавать функции вроде
resource <- aquireResource resourceDef
и
closeResource resource
и не бояться, что какая-то из функций вызовется дважды.
Но это описание уж очень смахивает на то, что @qnikst про линейные типы рассказывал
а resourcet? вроде он беспокоится за ресурсы
Alexander
линейные типы такого прям не дадут
Alexander
давай разбираться
Alexander
пусть у нас будет магическая функция foo
Alexander
foo 1 можно в двух местах проекта написать?
Alexander
это осмысленно?
Alexander
можно ли написать foo (op a b)
Alexander
но видимо функции пофиг на значение, ей только тип важен?
Alexander
вообще ничего не мешает функцию заделать идемпотентной
Зигохистоморфный
если только тип, то как-то через прокси
Dmitry
Не, погодите-ка. Это компилятору, получается, надо обнаружить одинаковые вычисления. А это - заявка на решение проблемы останова. Так что не получится
Alexander
хранить set типов на которых вызвано, и mvar
Alexander
при вызове проверять вызывалась ли, и если да то noop
Alexander
дёшево и сердито
Dmitry
Это в рантайме
Alexander
тут нету вычислений, не важно ж значение (наверное)
Alexander
нас попросили один раз для типа
Alexander
Значение, в общем случае, не важно, да
Dmitry
А компилятор энергично типы проверяет? Можно на типах сэмулировать ленивость?
Alexander
нет
Alexander
то, что глобально у нас в одном экземпляре это инстансы
Alexander
Не, погодите-ка. Это компилятору, получается, надо обнаружить одинаковые вычисления. А это - заявка на решение проблемы останова. Так что не получится
А поясни. Я не очень понимаю, как это связано
Alexander
т.е. если есть какая типофамилия сопоставляющая скажем Int и тип, то можно сделать что она будет объявлена один раз
Alexander
для каждого типа, поможет ли это хз
Зигохистоморфный
что если иметь HSet + HList c типами, что были вызваны? ну проверять есть ли такие типы в коллекции или нет
Alexander
А компилятор энергично типы проверяет? Можно на типах сэмулировать ленивость?
Сразу же вопрос: на тьюринг-полной системе типов можно эмулировать любую вычислительную функцию. А что с ленивостью?
Alexander
вообще какое-то желание поднять линейные типы на уровень выше
Alexander
ага, которых нету уже
Alexander
насколько я знаю теории в этом направлении нету
Alexander
но вообще на XY похоже
Alexander
все тип
Alexander
Это еще 8 лет будет продолжаться, все норм :)
Alexander
Или я путаю?
Cheese
я не понимаю математический смысл этого. ведь f x ... f x ≡ y ... y where y = f x. то есть эти ситуации неотличимы
Dmitry
Ну если бы была ленивость на типах, мы могли бы сделать что-то типа Const a b, где b лениво тайпчекался. Тогда туда можно было бы запихать f=....g....g..., то есть в таком лениво тайпчекере можно было бы обойти ограничение на единичность.
Alexander
Значит ли это, что есть некая семантика, которая невыразима в системе типов?
Cheese
наверно, можно через TH в компайлтайме (рантайме TH) записывать каждый тип в глобальную переменную
Зигохистоморфный
ну еще можно идексировать типы, и чтобы не совпадали индексы при вызове
Cheese
Значит ли это, что есть некая семантика, которая невыразима в системе типов?
это значит, что в твоей хотелке нет семантики
Зигохистоморфный
индексация временем :D тогда точно никогда не совпадет
Alexander
Хе-хе
Alexander
это значит, что в твоей хотелке нет семантики
Я не понимаю. Что мне помешает проапдейтить GHC, чтобы при разборе некоторого AST он смотрел, есть ли такое AST уже или нет.
Cheese
Зигохистоморфный
Я не понимаю. Что мне помешает проапдейтить GHC, чтобы при разборе некоторого AST он смотрел, есть ли такое AST уже или нет.
ты же можешь анотировать аст через кофри комонаду
Зигохистоморфный
и потом сравнивать только аннотации
Alexander
Все, здесь я уже перестал что-либо понимать. 😆
То есть, вы говорите, что задача некорректна?
Зигохистоморфный
Cheese
Все, здесь я уже перестал что-либо понимать. 😆
То есть, вы говорите, что задача некорректна?
я думаю, она в каком-то смысле корректна, но её невозможно решить и от неё нет пользы
Alexander
Prove it!
Зигохистоморфный
ну как бы всегда можно пойти от обратного)
Зигохистоморфный
а потом чтд или не чтд
Cheese
Prove it!
я выше писал, что в семантике Хаскеля f x + f x и y + y where y = f x эквивалентны. следовательно, ты можешь решить свою задачу в рамках AST, но не в рамках Хаскеля
Alexander
Ну ладно.
Хотя, может, тут новый синтаксис можно было бы ввести
Cheese
я выше писал, что в семантике Хаскеля f x + f x и y + y where y = f x эквивалентны. следовательно, ты можешь решить свою задачу в рамках AST, но не в рамках Хаскеля
на практике эта эквивалентность выливается в то, что компилятор может несколько одинаковых вхождений заменять на одно, чтобы не перевычислять, или наоборот, одно вхождение инлайнить в разные места
Dmitry
Сразу же вопрос: на тьюринг-полной системе типов можно эмулировать любую вычислительную функцию. А что с ленивостью?
Если система ттюринг-полная, то на ней можно смоделировать присваивание ячейке и проверку ячейки на значение, так? Ну так пусть в начале работы этой Штуки будет создана ячейка с "0", а первое использование функции проверит, что в этой ячейке. Если 0, то запишет туда 1, если не 0, то выдаст ошибку компиляции. Всё просто ;))
Cheese
Если система ттюринг-полная, то на ней можно смоделировать присваивание ячейке и проверку ячейки на значение, так? Ну так пусть в начале работы этой Штуки будет создана ячейка с "0", а первое использование функции проверит, что в этой ячейке. Если 0, то запишет туда 1, если не 0, то выдаст ошибку компиляции. Всё просто ;))
выдать ошибку компиляции во время исполнения?
Alexander
а можно узнать саму задачу-то?
Alexander
Alexander
это максимум ката какая-то из разряда because I can
Alexander
это может быть решением какой-то задачи, но не самой задачей
кана
Это вообще, видимо, сводится к хотелке невозможности вызвать одну и ту же функцию два раза с одним и тем же аргументом, что, скорее всего, противоречит самой сути языка. Но я таки не уверен
Нужно про линейные типы смотреть, из функции возвращать новую функцию, которая будет требовать аргумент другого типа
Alexander
это не решит проблему
кана
это не решит проблему
Почему? Это не даст нам вызвать функцию дважы и даст возможность менять тип аргумента (инкрементить нат в фантоме там)
Alexander
а то, что вернул я ещё раз с аргументос того же типа вызову
Alexander
Foo xs = Foo (forall a. a NotIn xs => a -> Foo (a:xs)) и такую штуку линейно еще
Alexander
тогда взлетит
кана
newtype F (n :: Nat)
= F { runF :: Proxy n -> Int -> (F (S n), String) }
кана
и вот в скоуп, где нужна эта функция, передать линейно F Z
Alexander
ну здесь только один домен для типов
Alexander
так не интересно