История изменений
Исправление AndreyKl, (текущая версия) :
В хаскиле есть только GADT+type families, которые позволяют наговнокодить простые индуктивные типы и некоторые функции над ними
да, это.
coq
да, не ответил - это ведь теорем прувер, не язык общего назначения, поэтому как пример плохо подходит. я понимаю что реализованы были довольно давно, но кок даже не претендует на «а давайте как вот сайтик запилим ан этом». А идрис - претендует.
По агде - я прошёл один туториал полтора (кажется) года назад и уже не помню на сколько там важна тотальность. В идрисе - то тальность определена как «либо завершается, либо обещает произвести результат на следующем шаге». что в общем, очень хорошо соответствует понятию «работоспособно». Хотя убедить компилятор в тотальности, похоже, не всегда легко. Но писать реальные программы похоже можно. На конференции по скале где Брэди рассказывал про идрис - он даже показывал игру емнип «космический бой» (или как он там - внизу экрана кораблик двигается влево вправо и стреляет, а сверху вниз движутся пришельцы и тоже стреляют).
по ф* ничего опять же сказать не могу, в вики что то не нашёл инфы навскидку, чтобы ознакомиться
Исправление AndreyKl, :
В хаскиле есть только GADT+type families, которые позволяют наговнокодить простые индуктивные типы и некоторые функции над ними
да, это.
coq
да, не ответил - это ведь теорем прувер, не язык общего назначения, поэтому как пример плохо подходит. я понимаю что реализованы были довольно давно, но кок даже не претендует на «а давайте как вот сайтик запилим ан этом». А идрис - претендует.
По агде - я прошёл один туториал полтора (кажется) года назад и уже не помню на сколько там важна тотальность. В идрисе - то тальность определена как «либо завершается, либо обещает произвести результат на следующем шаге». что в общем, очень хорошо соответствует понятию «работоспособно». Хотя убедить компилятор в тотальности, похоже, не всегда легко. Но писать реальные программы похоже можно. На конференции по скале где эдвин рассказывал про идрис - он даже показывал игру емнип «космический бой» (или как он там - внизу экрана кораблик двигается влево вправо и стреляет, а сверху вниз движутся пришельцы и тоже стреляют).
по ф* ничего опять же сказать не могу, в вики что то не нашёл инфы навскидку, чтобы ознакомиться
Исходная версия AndreyKl, :
В хаскиле есть только GADT+type families, которые позволяют наговнокодить простые индуктивные типы и некоторые функции над ними
да, это.
coq
да, не ответил - это ведь теорем прувер, не язык общего назначения, поэтому как пример плохо подходит. я понимаю что реализованы были довольно давно, но кок даже не претендует на «а давайте как вот сайтик запилим ан этом». А идрис - претендует.
По агде - я прошёл один туториал полтора (кажется) года назад и уже не помню на сколько там важна тотальность. В идрисе - то тальность определена как «либо завершается, либо обещает произвести результат на следующем шаге». что в общем, очень хорошо соответствует понятию «работоспособно». Хотя убедить компилятор в тотальности, похоже, не всегда легко. Но писать реальные программы похоже можно. На конференции по скале где эдвин рассказывал про идрис - он даже показывал игру емнип «космический бой» (или как он там - внизу экрана кораблик двигается влево вправо и стреляет, а сверху вниз движутся пришельцы и тоже стреляют).