Навеяно OCaml-ем и http://facebook.github.io/reason/ -ом. /pr/, объясни мне, зачем нужны сорта, кайнды и вообще все эти ✱ →✱ →✱ ? Почему нельзя использовать функции типов, с тем же самым синтаксисом, что и функции значений?
Ну что же вы, комплюктер-скикентисты?
вау. спасибо опушка. окамл с вменяемым синтаксисом подвезли
Не совсем понял твой вопрос.
Сложна сложна слоожна
А, разобрался. Пирс ввел виды, чтобы исключить бессмыслицы на уровне типов. Выражения вида «true 5» в какой-нибудь System F и так не типизируются, а вот выражения вида «n : Nat Nat» — уже хрен знает. Вот он и ввел виды, чтобы дополнительно типизировать сами типы.Еще он не строит систему типизации над видами. А я вот хочу построить. Причем я хочу сделать так, чтобы синтаксис был одинаковым и для «терм : тип», и для «тип : вид», и для «вид : сорт», и для любых высших порядков. Можно сделать просто: «терм : (тип : вид)», но… какие подводные камни?
>>748546> но… какие подводные камниВ том, что конструкторы типов ведут себя аналогично функциям, и в языках с зависимыми типами нет какой либо границы между миром типов и миром термов?Например, в Idris можно писать так: http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html#dependent-types
Новый окамл с нескучным синтаксисом. Все-таки пейсбук - самые зашкварные парашники из всех.
>>748788> Новый окамл с нескучным синтаксисом.Да. Лучшее, что случалось в языкостроении, ящитаю.
А систему модулей оставили такой же уёбищной.
>>748815Просто эталон НИНУЖНО. Окамл-то старый остался, а значит, все его проблемы - однопоточность и неработоспособность на виндах - никуда не делись. Зато починили то, что не было сломано - синтаксис. Просто гениально.
>>748114 (OP)>http://facebook.github.io/reason/ZverOcaml Maximum Ultimate xxxDarkVasyaNxxx Edition>>748876Чем тебе система модулей не нравится?
>>748978Это синтаксис-то не был сломан?
>>748114 (OP)> Почему нельзя использовать функции типов, с тем же самым синтаксисом, что и функции значений?Чтобы удобнее читать было. А то откроешь кот, а там везде какие-то функции, и непонятно над чем они и че они типизируют.
>>748303Не торжествуй заранее, вдруг там батареек нет и инфраструктура сделана тупо, плохо.
>>755728А что с ним не так? Попиши на фешарпе не выключая свет - на окамловый молиться начнёшь.
Мама, мама! Ночью вылез раби из под кровати и укусил меня за пятку! Избегаю ограниченного языка!
>>748114 (OP)ocaml с JS-синтаксисом.Достижение из достижений.
>>748114 (OP)Б-же мой! Нахуя вот это вот?
>>755759Короч были OCaml и SML. И нормально выглядил второй. Толком не знаю что к чему, но SML так и остался просто стандартом без норм реализаций. А в окамле видимо случился какой-то местный хайп среди функциональщиков типо смотрите добавили объекты как же жить стало хорошо. Хуй знает может в окамле есть какая-то реально недостающая функциональность но синтаксис у него убогий. Поэтому можно порадоваться за майкрософта-рабов, что им дали вполне умеренный мл с вполне нормальным синтаксисом. Другое дело что это такие неважные мелочи.
>>756352Знаешь, я, конечно, не эксперт в логике и всякой математике, но что-то мне кажется, что аргументировать утверждение "у окамла плохой синтаксис" утверждением "у окамла убогий синтаксис" - это, как бы сказать, слегка неправильный подход.
>>748114 (OP)В depended-typed языках с бесконечной ерархией универсумов так и есть. Но на практике достаточно типов и видов, дальше забуриваться особого смысла нет. В общем если у тебя изначально depended-typed язык, то логично делать всё однообразно. Но хаскели и прочие окамлы изначально таковыми не являлись, поэтому в них сделали типы, потом почесали репу и добавили еще и виды. А потом решили, что в общем-то дальше добавлять ничего и не нужно.
>>756570Ну слушай. В этой битве ты победил. Я просто мимопроходил и захотелось сказать, что да, хоть это и вкусовщина, но всякий раз как пытаюсь разобраться есть ли что-нибудь в окамле нового для себя воротит банально от синтаксиса. Короче хотел докинуть мнения, но чёт не вяжуться мои слова в связные предложения.
Раз зависимых типов трэд почил в бозе, поинтересуюсь тут. Есть переменная целочисленного беззнакового типа совпадающая разрядностью с разрядностью платформы. В конструкторе некий объект её инкременирует, в деструкторе декременирует, больше никто её не трогает. Человеку-то очевидна невозможность её переполнения, но как можно было бы продемонстировать это гипотетическому компилятору? Вообще из языков с зависимыми типами не так уж много императивных, а в тех что есть переполнения вообще игнорируются, но интересует-таки теоретическая возможность реализовать подобное.
>>748876Да они вообще семантику и проверку типов нигде не поменяли.Только с парсером побаловались.
>>758158ты наркоман ну или математик, сам придумал какую то проблему, конпеляторы знают разрядность под которой они работают
>>758158Я по оразованию математик, но попробую хотя бы план тебе наметить. Во-первых, тебе нужно формализовать понятие объекта и доказать для начала, что для заданного объекта деструктор не может быть вызван, если не был вызван конструктор. Во-вторых, как ни крути, надо доказать, что количество объектов у тебя не сможет превысить 2^битность твоего беззнакового типа.
