LINUX.ORG.RU

Вышла Agda 2.5.1

 ,


1

4

Чистый функциональный язык программирования и система интерактивного доказательства Agda обновилась до версии 2.5.1.

Некоторые изменения:

  • представлена официальная пользовательская документация;
  • с помощью прагмы HASKELL можно добавлять к модулю произвольный код на Haskell;
  • многочисленные изменения в области метапрограммирования и рефлексии;
  • исправлены некоторые ошибки в бекэндах:
    • теперь нет необходимости указывать {-# COMPILED_DATA #-} для встроенных типов Bool, Int, Float и других;
    • клозы функций с разной арностью компилируются корректно;
    • поддержка co-patterns в бекэндах GHC/UHC;
  • поддержка Utrecht Haskell Compiler (UHC) в качестве бекэнда.

>>> Подробности

★★★★★

Проверено: splinter ()
Последнее исправление: splinter (всего исправлений: 1)

А что, UHC жив, вроде GHC наше всё?

anonymous
()

Как я понимаю единственная ценность данного языка заключается в помощи распила грантов?

anonymous
()
Ответ на: комментарий от nightuser

Software Foundations

Содержания прям как из какой-то параллельной software вселенной. Интересно, сколько народу живёт в ней? Кстати, всяких онлайн курсов (да и неонлайн, наверняка, тоже) по машинному обучению и нейронным сетям становится всё больше. А как вот с курсами по этой параллельной вселенной ПО?

gag ★★★★★
()
Ответ на: комментарий от gag

MOOC мне не попадались, есть Oregon Programming Languages Summer School. Основной упор — теория типов, логика, теория категорий. Начиная вот отсюда можешь посмотреть архив по годам.

Coq используют в учебных процессах несколько крупных университетов. По Agda раньше проводились (сейчас не знаю) семинары в ИТМО.

Сомневаюсь, что появятся полноценные онлайн курсы по этой тематике.

ymn ★★★★★
() автор топика
Ответ на: комментарий от Sociopsih

А почему? Не актуально?

Ну это было бы примерно как создавать курсы по использованию сферического коня в вакууме.

anonymous
()
Ответ на: комментарий от gag

В лаборатории JetBrains на матмехе осенью был курс по Coq, основанный как раз на данной книжке.

По Agda вроде скоро в АУ будет курс.

nightuser
()

Зачем? Есть ASM

anonymous
()
Ответ на: комментарий от anonymous

Кто ж борщехлебам-фофанам гранты давать будет?/Дураков нет.

anonymous
()
Ответ на: комментарий от anonymous

Как я понимаю единственная ценность данного языка заключается в помощи распила грантов?

Нет, в доказательстве корректности распила.

korvin_ ★★★★★
()
Вы не можете добавлять комментарии в эту тему. Тема перемещена в архив.