p
в твоем случае подставилось тело nontotal 0 (как я понял)
Size: a a a
2021 January 21
p
если нетотальная - просто подставляется тело
или нет
p
в общем если функция нетотальная то она не редуцируется
EG
А, ну подожди, так это означает, что нетотальные функции таки не работают, и система типов таки детерминированная
p
А, ну подожди, так это означает, что нетотальные функции таки не работают, и система типов таки детерминированная
ты можешь записать нетотальную функцию на тайплевеле но она не средуцируется и ты не сможешь создать терм с этим типом
p
(как я понял)
EG
ты можешь записать нетотальную функцию на тайплевеле но она не средуцируется и ты не сможешь создать терм с этим типом
Ну, это не мешает тогда проверке типов за конечное время
p
ага
а
nontotal : Int -> Type
nontotal x = nontotal x
foo : (nontotal 0) -> (nontotal 0)
foo x = foo x
main : IO ()
main = putStrLn (foo "x")
ЯННП
Идрис отказывается это компилировать, утверждая, что nontotal 0 это не String. Вопрос: как он узнал?
Наверное увидел безусловную бесконечную рекурсию и решил что функция не тотальная
EG
Наверное увидел безусловную бесконечную рекурсию и решил что функция не тотальная
Да понятно, что она не тотальная
p
там тайплевел decidable и не-тьюринг полный.
EG
Это смешно, на самом деле
Хоть в каком-то месте тайплевел раста круче
Хоть в каком-то месте тайплевел раста круче
EG
На нём можно написать брейнфак!
p
Это смешно, на самом деле
Хоть в каком-то месте тайплевел раста круче
Хоть в каком-то месте тайплевел раста круче
почему
p
На нём можно написать брейнфак!
что крутого
p
наоборот
EG
Ну
Так как Idris, очевидно, не решает проблему останова, не все корректные типы выразимы в Idris.
Так как Idris, очевидно, не решает проблему останова, не все корректные типы выразимы в Idris.
ML
Коллеги есть древняя задача и множество способов ее решения:
Лев ходит по пустыне. В свое время физики предложили свою подборку методов решения задачи о поимке льва в пустыне и помещении его в клетку. А как решают ту же задачу различные деятели эпохи информационных технологий?
Программист на Паскале.
Просматривает пустыню полным перебором. Обнаружив льва, строит вокруг него клетку.
Продвинутый программист на Паскале.
Сортирует пустыню по возрастанию, после чего ищет льва двоичным поиском и строит вокруг него клетку. Если в процессе строительства лев уходит, бросает работу с криком "Rаngе Сhесk Еrrоr".
Программист на Си.
Ищет в пустыне камень и помещает его в клетку. Присваивает камню значение "лев".
Продвинутый программист на Си.
Присваивает пустыне значение "клетка".
Программист на Си++.
Проектирует клетку таким образом, чтобы лев был ее составной частью. При инициализации клетки лев автоматически генерируется внутри.
Программист на Аде.
Говорит, что лев и клетка - это объекты разных типов, и нечего морочить ему голову некорректными задачами.
Программист на Дельфи.
Пишет во все конференции: "Народ, где взять компонент, который ищет в пустыне льва и помещает его в клетку?".
Железячник.
Покупает в зоопарке львицу, делает ей операцию по смене пола и долго пытается запихнуть ее в клетку для канарейки.
Геймер-асtiоnер.
Вооружается супершотганом, плазмаганом, рэйлганом, нэйлганом, шестиствольным пулеметом и бензопилой. Прочесывает пустыню, разнося все на своем пути. Ищет среди убитых льва и пытается обнаружить у него в животе желтый ключ. Если находит, отпирает им клетку и ждет награды.
Геймер-квестовик.
Ищет по всей пустыне льва, находит, кладет в карман. Затем ищет по всей пустыне клетку, попутно пытаясь засунуть льва в чайник, башмак, телевизор, ведро с краской и другие попадающиеся на пути емкости.
Геймер-стратег.
Поднимает по всей пустыне налоги, чтобы получить деньги на строительство клетки и охотничьих юнитов. К моменту окончания строительства все львы дохнут от голода.
Пользователь интернета.
Заходит в свой любимый поисковик, пишет в строке Sеаrсh "пустыня", ищет в найденном "лев в клетке". Если не находит, говорит, что задача неразрешима.
Вебмастер.
Заходит в свой любимый поисковик и пишет в строке Sеаrсh "пустыня + лев". Создает документ клетка.html и прописывает в нем ссылку на найденное.
Спамер.
Рассылает по всей пустыне множество клеток, к каждой из которых привязана бумажка: "Если вы лев, пожалуйста, зайдите внутрь и закройтесь изнутри".
Троянщик.
Делает то же, что и спамер, но вместо бумажки снаружи вешает внутри клетки картинку с голой львицей.
Админ.
Выкапывает вокруг клетки ров, заполняет его концентрированной кислотой, устанавливает вдоль берега противотанковые ежи и противопехотные мины, все это опутывает колючей проволокой. К проволоке и прутьям клетки подключает провода от генератора высокого напряжения. Вешает на клетку 10 кодовых и 12
амбарных замков. Заходит внутрь, запирается на все замки, пускает ток, ключи проглатывает, коды забывает и говорит, что теперь ему никакой лев не страшен.
Хакер.
Нейтрализует кислоту щелочью, перекусывает проволоку, проползает под ежами, перепрыгивает с шестом через мины, отключает ток, взламывает замки и входит в клетку. Не обнаружив внутри льва, матерится с досады, дает пинка админу и уходит обратно в пустыню.
Лев ходит по пустыне. В свое время физики предложили свою подборку методов решения задачи о поимке льва в пустыне и помещении его в клетку. А как решают ту же задачу различные деятели эпохи информационных технологий?
Программист на Паскале.
Просматривает пустыню полным перебором. Обнаружив льва, строит вокруг него клетку.
Продвинутый программист на Паскале.
Сортирует пустыню по возрастанию, после чего ищет льва двоичным поиском и строит вокруг него клетку. Если в процессе строительства лев уходит, бросает работу с криком "Rаngе Сhесk Еrrоr".
Программист на Си.
Ищет в пустыне камень и помещает его в клетку. Присваивает камню значение "лев".
Продвинутый программист на Си.
Присваивает пустыне значение "клетка".
Программист на Си++.
Проектирует клетку таким образом, чтобы лев был ее составной частью. При инициализации клетки лев автоматически генерируется внутри.
Программист на Аде.
Говорит, что лев и клетка - это объекты разных типов, и нечего морочить ему голову некорректными задачами.
Программист на Дельфи.
Пишет во все конференции: "Народ, где взять компонент, который ищет в пустыне льва и помещает его в клетку?".
Железячник.
Покупает в зоопарке львицу, делает ей операцию по смене пола и долго пытается запихнуть ее в клетку для канарейки.
Геймер-асtiоnер.
Вооружается супершотганом, плазмаганом, рэйлганом, нэйлганом, шестиствольным пулеметом и бензопилой. Прочесывает пустыню, разнося все на своем пути. Ищет среди убитых льва и пытается обнаружить у него в животе желтый ключ. Если находит, отпирает им клетку и ждет награды.
Геймер-квестовик.
Ищет по всей пустыне льва, находит, кладет в карман. Затем ищет по всей пустыне клетку, попутно пытаясь засунуть льва в чайник, башмак, телевизор, ведро с краской и другие попадающиеся на пути емкости.
Геймер-стратег.
Поднимает по всей пустыне налоги, чтобы получить деньги на строительство клетки и охотничьих юнитов. К моменту окончания строительства все львы дохнут от голода.
Пользователь интернета.
Заходит в свой любимый поисковик, пишет в строке Sеаrсh "пустыня", ищет в найденном "лев в клетке". Если не находит, говорит, что задача неразрешима.
Вебмастер.
Заходит в свой любимый поисковик и пишет в строке Sеаrсh "пустыня + лев". Создает документ клетка.html и прописывает в нем ссылку на найденное.
Спамер.
Рассылает по всей пустыне множество клеток, к каждой из которых привязана бумажка: "Если вы лев, пожалуйста, зайдите внутрь и закройтесь изнутри".
Троянщик.
Делает то же, что и спамер, но вместо бумажки снаружи вешает внутри клетки картинку с голой львицей.
Админ.
Выкапывает вокруг клетки ров, заполняет его концентрированной кислотой, устанавливает вдоль берега противотанковые ежи и противопехотные мины, все это опутывает колючей проволокой. К проволоке и прутьям клетки подключает провода от генератора высокого напряжения. Вешает на клетку 10 кодовых и 12
амбарных замков. Заходит внутрь, запирается на все замки, пускает ток, ключи проглатывает, коды забывает и говорит, что теперь ему никакой лев не страшен.
Хакер.
Нейтрализует кислоту щелочью, перекусывает проволоку, проползает под ежами, перепрыгивает с шестом через мины, отключает ток, взламывает замки и входит в клетку. Не обнаружив внутри льва, матерится с досады, дает пинка админу и уходит обратно в пустыню.
ML
А как решают задачу поимки льва в пустыне на Rust ?
EG
Michael Larin
Коллеги есть древняя задача и множество способов ее решения:
Лев ходит по пустыне. В свое время физики предложили свою подборку методов решения задачи о поимке льва в пустыне и помещении его в клетку. А как решают ту же задачу различные деятели эпохи информационных технологий?
Программист на Паскале.
Просматривает пустыню полным перебором. Обнаружив льва, строит вокруг него клетку.
Продвинутый программист на Паскале.
Сортирует пустыню по возрастанию, после чего ищет льва двоичным поиском и строит вокруг него клетку. Если в процессе строительства лев уходит, бросает работу с криком "Rаngе Сhесk Еrrоr".
Программист на Си.
Ищет в пустыне камень и помещает его в клетку. Присваивает камню значение "лев".
Продвинутый программист на Си.
Присваивает пустыне значение "клетка".
Программист на Си++.
Проектирует клетку таким образом, чтобы лев был ее составной частью. При инициализации клетки лев автоматически генерируется внутри.
Программист на Аде.
Говорит, что лев и клетка - это объекты разных типов, и нечего морочить ему голову некорректными задачами.
Программист на Дельфи.
Пишет во все конференции: "Народ, где взять компонент, который ищет в пустыне льва и помещает его в клетку?".
Железячник.
Покупает в зоопарке львицу, делает ей операцию по смене пола и долго пытается запихнуть ее в клетку для канарейки.
Геймер-асtiоnер.
Вооружается супершотганом, плазмаганом, рэйлганом, нэйлганом, шестиствольным пулеметом и бензопилой. Прочесывает пустыню, разнося все на своем пути. Ищет среди убитых льва и пытается обнаружить у него в животе желтый ключ. Если находит, отпирает им клетку и ждет награды.
Геймер-квестовик.
Ищет по всей пустыне льва, находит, кладет в карман. Затем ищет по всей пустыне клетку, попутно пытаясь засунуть льва в чайник, башмак, телевизор, ведро с краской и другие попадающиеся на пути емкости.
Геймер-стратег.
Поднимает по всей пустыне налоги, чтобы получить деньги на строительство клетки и охотничьих юнитов. К моменту окончания строительства все львы дохнут от голода.
Пользователь интернета.
Заходит в свой любимый поисковик, пишет в строке Sеаrсh "пустыня", ищет в найденном "лев в клетке". Если не находит, говорит, что задача неразрешима.
Вебмастер.
Заходит в свой любимый поисковик и пишет в строке Sеаrсh "пустыня + лев". Создает документ клетка.html и прописывает в нем ссылку на найденное.
Спамер.
Рассылает по всей пустыне множество клеток, к каждой из которых привязана бумажка: "Если вы лев, пожалуйста, зайдите внутрь и закройтесь изнутри".
Троянщик.
Делает то же, что и спамер, но вместо бумажки снаружи вешает внутри клетки картинку с голой львицей.
Админ.
Выкапывает вокруг клетки ров, заполняет его концентрированной кислотой, устанавливает вдоль берега противотанковые ежи и противопехотные мины, все это опутывает колючей проволокой. К проволоке и прутьям клетки подключает провода от генератора высокого напряжения. Вешает на клетку 10 кодовых и 12
амбарных замков. Заходит внутрь, запирается на все замки, пускает ток, ключи проглатывает, коды забывает и говорит, что теперь ему никакой лев не страшен.
Хакер.
Нейтрализует кислоту щелочью, перекусывает проволоку, проползает под ежами, перепрыгивает с шестом через мины, отключает ток, взламывает замки и входит в клетку. Не обнаружив внутри льва, матерится с досады, дает пинка админу и уходит обратно в пустыню.
Лев ходит по пустыне. В свое время физики предложили свою подборку методов решения задачи о поимке льва в пустыне и помещении его в клетку. А как решают ту же задачу различные деятели эпохи информационных технологий?
Программист на Паскале.
Просматривает пустыню полным перебором. Обнаружив льва, строит вокруг него клетку.
Продвинутый программист на Паскале.
Сортирует пустыню по возрастанию, после чего ищет льва двоичным поиском и строит вокруг него клетку. Если в процессе строительства лев уходит, бросает работу с криком "Rаngе Сhесk Еrrоr".
Программист на Си.
Ищет в пустыне камень и помещает его в клетку. Присваивает камню значение "лев".
Продвинутый программист на Си.
Присваивает пустыне значение "клетка".
Программист на Си++.
Проектирует клетку таким образом, чтобы лев был ее составной частью. При инициализации клетки лев автоматически генерируется внутри.
Программист на Аде.
Говорит, что лев и клетка - это объекты разных типов, и нечего морочить ему голову некорректными задачами.
Программист на Дельфи.
Пишет во все конференции: "Народ, где взять компонент, который ищет в пустыне льва и помещает его в клетку?".
Железячник.
Покупает в зоопарке львицу, делает ей операцию по смене пола и долго пытается запихнуть ее в клетку для канарейки.
Геймер-асtiоnер.
Вооружается супершотганом, плазмаганом, рэйлганом, нэйлганом, шестиствольным пулеметом и бензопилой. Прочесывает пустыню, разнося все на своем пути. Ищет среди убитых льва и пытается обнаружить у него в животе желтый ключ. Если находит, отпирает им клетку и ждет награды.
Геймер-квестовик.
Ищет по всей пустыне льва, находит, кладет в карман. Затем ищет по всей пустыне клетку, попутно пытаясь засунуть льва в чайник, башмак, телевизор, ведро с краской и другие попадающиеся на пути емкости.
Геймер-стратег.
Поднимает по всей пустыне налоги, чтобы получить деньги на строительство клетки и охотничьих юнитов. К моменту окончания строительства все львы дохнут от голода.
Пользователь интернета.
Заходит в свой любимый поисковик, пишет в строке Sеаrсh "пустыня", ищет в найденном "лев в клетке". Если не находит, говорит, что задача неразрешима.
Вебмастер.
Заходит в свой любимый поисковик и пишет в строке Sеаrсh "пустыня + лев". Создает документ клетка.html и прописывает в нем ссылку на найденное.
Спамер.
Рассылает по всей пустыне множество клеток, к каждой из которых привязана бумажка: "Если вы лев, пожалуйста, зайдите внутрь и закройтесь изнутри".
Троянщик.
Делает то же, что и спамер, но вместо бумажки снаружи вешает внутри клетки картинку с голой львицей.
Админ.
Выкапывает вокруг клетки ров, заполняет его концентрированной кислотой, устанавливает вдоль берега противотанковые ежи и противопехотные мины, все это опутывает колючей проволокой. К проволоке и прутьям клетки подключает провода от генератора высокого напряжения. Вешает на клетку 10 кодовых и 12
амбарных замков. Заходит внутрь, запирается на все замки, пускает ток, ключи проглатывает, коды забывает и говорит, что теперь ему никакой лев не страшен.
Хакер.
Нейтрализует кислоту щелочью, перекусывает проволоку, проползает под ежами, перепрыгивает с шестом через мины, отключает ток, взламывает замки и входит в клетку. Не обнаружив внутри льва, матерится с досады, дает пинка админу и уходит обратно в пустыню.
> во все конференции
> конференции
> к о н ф е р е н ц и и
Спасибо, что не эхи. Ты где этот боян выкопал?
> конференции
> к о н ф е р е н ц и и
Спасибо, что не эхи. Ты где этот боян выкопал?