ПС
Где можно про это почитать?
Size: a a a
Типы в языках программирования, моделирования, представления знаний и жизни
505 membersпожаловаться на группу
2022 January 24
[
Писал теоретический вопрос о своих эмпирических наблюдениях и понял, что я тупой
AC
Более хитрый вариант рекурсии в типах ведущий к unsoundness описан в https://counterexamples.org/strict-positivity.html
ПС
Знакомый пример с non-strict positive, спасибо
Но мне всё-таки хочется пример с non-termination
Но мне всё-таки хочется пример с non-termination
AC
Так он non-termination и вызывает через бесконечную рекурсию на типах. Там только unsafe coerce напрямую не строят, но имея
worse : False это не сложно.AC
Ну или можно тот пример из Java Unsound повторить.
[
Из хаскеля с ансейф перформ👀
[
Кстати, а как с точки зрения теории типов мутабельность + ансейф перформ + генерализация типа на топлевеле ведут к ансаунд?
[
Или это типа ноун ишью хаскельной типизации?
AC
Known issue. Haskell type system is unsound by design (at least in GHC).
AC
В конце концов
unsafeCoerce там есть в стандартной библиотеке — его не нужно писать самому.[
Ну одно дело - бекдор, который можно удалить, тупо убрав хак из стд и другое - возможность написать самому миллионы реализаций
[
С другой стороны эти миллионы реализаций тоже убираются, если не экспортировать конструктор IO
AC
[
Сейф хаскель не работает
AC
Впрочем, Safe Haskell тоже Unsound спасибо Curry's paradox и прочем non-positive types. Или всё-таки sound?.. 🤔
AC
Подробности имеются?
[
Ну я его сломать не пытался
[
Но там есть андефайнед