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 ()

Кто бы научил этим пользоваться. Жаль я уже не студент...

weare ★★ ()

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

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

Step One: Learn Haskell

Для языка, основанного на Haskell, рекомендуется знание Haskell. Удивительно, правда?

hateyoufeel ★★★★★ ()

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

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

Software Foundations

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

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

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

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

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

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

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

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

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

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

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

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

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

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

nightuser ()

Зачем? Есть ASM

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

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

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

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

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

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