Кто-нибуть может сравнить эти языки? Чем отличаются? Что зачем?
Агда это больше прувер для доказательства теорем и т.п. матеши, Идрис больше для написания программ. А так, те же яйца зависимые типы, вид сбоку.
И то, и другое с упором на дженерал пёпэс.
Только в идрисе фич больше, синтаксис, как в хачкиле и компилится сразу в Си в то время, как агда (по сути агда 2 - это уже совсем другой ЯП) юзает GHC
А есть языки с зависимыми типами, но не чисто функциональные? Чтобы были присваивания, мутабельные структуры, чтобы хеллоу ворлд можно было сделать без монадного цирка? И желательно чтобы тоже в сишку компилировался.
Или это невозможно сделать по каким-то причинам?
Или это невозможно сделать по каким-то причинам?
ATS.
Спасибо. Посмотрел его немного, пока что отдает легким безумием. Синтаксис ад какой-то, фичей море но при этом даже нет ООП. В туториале авторы маниакально применяют рекурсию вместо циклов, не очень понятно из каких соображений.
Но сама концепция интересна.
Пиздец зелень
Почему-то мне тоже кажется, что любая попытка втащить зависимае типы в императивный мир отдаёт идиотизмом.
Чего нет? Вон в Scala втащили HKT и норм, вполне можно представить как оно смотрелось бы и с завтипами. Вообще типы ортогональны парадигме.
Святая толстота.
Такое впечатление что в /pr люди почти всегда имеют очень слабое представление о то о чем они говорят. HKT не имеют отношения к зависимым типам. В скале есть есть зависимые типы в очень необычном виде: http://stackoverflow.com/questions/12935731/any-reason-why-scala-does-not-explicitly-support-dependent-types
>Типы ортогональны парадигме
Погугли по ко- и контрвариации в той же сакале. И почему это хуёво соотносится с присваиванием
И почему?
Поясните, если есть код на паскале, можно ли проверить его корректность в этих ваших пруверах?
Можно. Делается это просто. Шаг 1: переписываешь код с паскаля на этот ваш прувер. Шаг 2: доказываешь, что программы эквивалентны. Шаг 3: компиляешь - если получилось, то программа корректна (или ты нашёл баг в этом вашем прувере).
И я сейчас нихуя не шучу.
А если попроще как-то? Все конструкции в паскале разве нельзя просто объявить зависимыми типами?
А какие там системы типов? Я где-то читал что в агде - исчисление конструкций. Это правда, или там только Мартин-Лёф? А как в идрис? И какие конкретно в идрис преимущества для создания компилируемых программ.
>типы ортогональны парадигме
Ой ли?
Всего лишь инструмент
Конечно. Типы, это хуёвина которую можно добавить куда угодно. Добавляешь типы в ФП - получаешь цацкель, добавляешь в ООП - получаешь скалу, добавляешь в логическое программирование - получаешь меркари и так далее. Они не прибиты к ФП гвоздями.
Добавил типы в ООП - получил скалу. Добавил типы в логический ЯП - получил
Конечно. Типы, это хуёвина которую можно добавить куда угодно. Добавляешь типы в ФП - получаешь цацкель, добавляешь в ООП - получаешь скалу, добавляешь в логическое программирование - получаешь меркари и так далее. Они не прибиты к ФП гвоздями.
Если просто добавить типы в ЯП, где их не было, получится ЯП, в котором типы никак не участвуют в дизайне программ.
Хороший пример - TypeScript. А во всяких хаскелях ты выражаешь и проектируешь программы отталкиваясь от типов, все эти (g)adt, тайпкласы, итд.
Но это всё неважно.
Хороший пример - TypeScript. А во всяких хаскелях ты выражаешь и проектируешь программы отталкиваясь от типов, все эти (g)adt, тайпкласы, итд.
Но это всё неважно.
Ну так под типами я подразумеваю не просто типизацию, а именно систему типов, где типы участвуют в дизайне программ. (Haskell, Scala, Mercury).
бамп, что-ли.
Поясните. Чем пикрелейтед (знак логического следования) отличается от импликации (стрелочки -> или что тоже самое, подмножества)? В обеих случаях выражение значит "если а то б" или "из а следует б".
Не следует путать импликацию (→) и логическое следование (⇒). Импликация как логическое выражение может сама принимать значения истины или лжи. Логическое же следование A ⇒ B утверждает, что во всех случаях, когда формула A истинна, B также будет истинно.
Если в обозначениях ОП-поста то слева от этой стрелочки стоит контекст т.е. словарик из терм:тип на сколько я понимаю.
Agda is too mainstream!
Тогда тебе нужен транслятор из паскаля в какое-то представление с зависимыми типами. Писать его можешь хоть на яваскрипте.
Объясните отличия Agda от CoC. Что ещё за тактики там?
>Coq
fix
Coq умеет в автоматические доказательства.
well, that’s what they doing jealous, they confuse it
It’s not hip hop, it’s pop, cause I found a hella way to fuse it
With rock, shock rap with Doc
to make them loose it
I don’t know how to make songs like that, I don’t know what words to use
Let me know when it occurs to you
While I’m ripping any of these verses
>автоматические доказательства
это отличие от агды?
бамп
На всякий случай... бамп
UP
Потому что мамку твою ебал.
Сказал же погугли, еблан тупорылый. Уверен, ты даже о том,что такое ковариация понятия не имеешь
Так что все-таки первокультурней? Идрис или агда?
Агда первокультурнее. Идрис заявлен как язык для системного программирования с зависимыми типами, т.е. упор на прикладное применение, а не на чисто математическое.
А если сравнивать агду и петуха?
