>>835514 (OP)
Агда это больше прувер для доказательства теорем и т.п. матеши, Идрис больше для написания программ. А так, те же яйца зависимые типы, вид сбоку.

>>835807
И то, и другое с упором на дженерал пёпэс.
Только в идрисе фич больше, синтаксис, как в хачкиле и компилится сразу в Си в то время, как агда (по сути агда 2 - это уже совсем другой ЯП) юзает GHC

А есть языки с зависимыми типами, но не чисто функциональные? Чтобы были присваивания, мутабельные структуры, чтобы хеллоу ворлд можно было сделать без монадного цирка? И желательно чтобы тоже в сишку компилировался.
Или это невозможно сделать по каким-то причинам?

>>836484
ATS.

>>836489
Спасибо. Посмотрел его немного, пока что отдает легким безумием. Синтаксис ад какой-то, фичей море но при этом даже нет ООП. В туториале авторы маниакально применяют рекурсию вместо циклов, не очень понятно из каких соображений.
Но сама концепция интересна.

>>836522
>>836484
Пиздец зелень

>>836885
Почему-то мне тоже кажется, что любая попытка втащить зависимае типы в императивный мир отдаёт идиотизмом.

>>837013
Чего нет? Вон в Scala втащили HKT и норм, вполне можно представить как оно смотрелось бы и с завтипами. Вообще типы ортогональны парадигме.

Святая толстота.

>>837021
Такое впечатление что в /pr люди почти всегда имеют очень слабое представление о то о чем они говорят. HKT не имеют отношения к зависимым типам. В скале есть есть зависимые типы в очень необычном виде: http://stackoverflow.com/questions/12935731/any-reason-why-scala-does-not-explicitly-support-dependent-types

>>837021
>Типы ортогональны парадигме
Погугли по ко- и контрвариации в той же сакале. И почему это хуёво соотносится с присваиванием

>>837386
И почему?

Поясните, если есть код на паскале, можно ли проверить его корректность в этих ваших пруверах?

>>838238
Можно. Делается это просто. Шаг 1: переписываешь код с паскаля на этот ваш прувер. Шаг 2: доказываешь, что программы эквивалентны. Шаг 3: компиляешь - если получилось, то программа корректна (или ты нашёл баг в этом вашем прувере).
И я сейчас нихуя не шучу.

А какие там системы типов? Я где-то читал что в агде - исчисление конструкций. Это правда, или там только Мартин-Лёф? А как в идрис? И какие конкретно в идрис преимущества для создания компилируемых программ.

>>837021
>типы ортогональны парадигме
Ой ли?

>>839438
Конечно. Типы, это хуёвина которую можно добавить куда угодно. Добавляешь типы в ФП - получаешь цацкель, добавляешь в ООП - получаешь скалу, добавляешь в логическое программирование - получаешь меркари и так далее. Они не прибиты к ФП гвоздями.

Добавил типы в ООП - получил скалу. Добавил типы в логический ЯП - получил

>>839438
Конечно. Типы, это хуёвина которую можно добавить куда угодно. Добавляешь типы в ФП - получаешь цацкель, добавляешь в ООП - получаешь скалу, добавляешь в логическое программирование - получаешь меркари и так далее. Они не прибиты к ФП гвоздями.

Если просто добавить типы в ЯП, где их не было, получится ЯП, в котором типы никак не участвуют в дизайне программ.
Хороший пример - TypeScript. А во всяких хаскелях ты выражаешь и проектируешь программы отталкиваясь от типов, все эти (g)adt, тайпкласы, итд.
Но это всё неважно.

>>839517
Ну так под типами я подразумеваю не просто типизацию, а именно систему типов, где типы участвуют в дизайне программ. (Haskell, Scala, Mercury).

бамп, что-ли.

>>841336
Не следует путать импликацию (→) и логическое следование (⇒). Импликация как логическое выражение может сама принимать значения истины или лжи. Логическое же следование A ⇒ B утверждает, что во всех случаях, когда формула A истинна, B также будет истинно.

>>841336
Если в обозначениях ОП-поста то слева от этой стрелочки стоит контекст т.е. словарик из терм:тип на сколько я понимаю.

Agda is too mainstream!

>>838845
Тогда тебе нужен транслятор из паскаля в какое-то представление с зависимыми типами. Писать его можешь хоть на яваскрипте.

Объясните отличия Agda от CoC. Что ещё за тактики там?

>>847151
>Coq
fix

>>847151
Coq умеет в автоматические доказательства.

>>844490
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

>>847212
>автоматические доказательства
это отличие от агды?

бамп

На всякий случай... бамп

UP

>>838088
Потому что мамку твою ебал.
Сказал же погугли, еблан тупорылый. Уверен, ты даже о том,что такое ковариация понятия не имеешь

Так что все-таки первокультурней? Идрис или агда?

>>874500
А если сравнивать агду и петуха?