LINUX.ORG.RU

Вышла Agda 2.4.0

 ,


0

5

Чистый функциональный язык программирования и система интерактивного доказательства Agda обновилась до версии 2.4.0. Новый выпуск содержит солидное число изменений и улучшений, некоторые из которых представлены ниже:

  • экспериментальная возможность: Varying arity — теперь клозы функции могут иметь различное число аргументов;
  • бекэнд MAlonzo теперь позволяет компилировать неполные программы (т.е. без функции main). Основная цель — написать на Agda лишь часть программы, для которой позднее можно дописать недостающий Haskell-код. Введена новая опция командной строки --compile-no-main;
  • представлено новый модуль Agda.Primitive;
  • экспериментальная возможнось: copatterns (с соответствующей опцией {-# OPTIONS --copatterns #-});
  • незначительные изменения в синтаксисе;
  • многочисленные улучшения в agda-mode для Emacs.

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

★★★★★

Проверено: maxcom ()
Последнее исправление: ymn (всего исправлений: 2)

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

В жопу монады. За аппликативными функторами светлое будущее!

В хаскелле монады - это подкласс функторов.

anonymous
()

теперь клозы функции

Шо это?

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

Ну да, не прошло и четверти века, как «взгляд в будущее» увидел что-то расположенное слегка дальше собственного носа.

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

А что обычный человек делает в топике про Agda? Алсо ни одного коммента про зависимые типы. Сплошной хаскель.

KblCb ★★★★★
()
Последнее исправление: KblCb (всего исправлений: 1)
Ответ на: комментарий от anonymous

Это-то понятно. Непонятно почему в моем арчике xmonad просит 827 мегабайт места для установки

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

Между ними огромная пропасть.

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

Вот сам и пиши ssl на агдах и коках с ебиграмами. Как раз к концу двадцать второго века твои потомки закончат пилить функциональность из начала 90х.

anonymous
()

Ахах...язык философского программирования, с монадами и доказательствами :D

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

А в чём нестыковка в хаскеле?

Сейчас это разные классы?

anonymous
()

Чистый функциональный язык программирования

Еще более чистый чем хаскель?

loz ★★★★★
()
Ответ на: комментарий от loz
Попросил его написать метод, разворачивающий строку, классическая такая проверка на вшивость. Мелкое тощее горбатое существо с рожей и голосом профессионального алкаша бубнило и булькало чтото с полчаса, ничего родить не смогло, потом начало втирать, что вот зато в мегаязыке Хаскель строки сделаны односвязными списками и что это типа тру, а все остальное ламеризм. Еще чтото втирал что кулькакеры на Вакс использовали мегаформат для строк ASCIID, а ламеры не поняли и теперь везде позорный ASCIIZ (внимание: собеседование вообще про Java было). 

(C) с просторов ЛОРа

Bioreactor ★★★★★
()

Никто не напишет «не нужно»? Неужели нужно?

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

Что такое аппликативные функторы?

Все очень просто. Как я объясняю это для детей.

Есть коробка с конфетами (контейнер) и девочка (функция). Девочка достает конфету из коробки и съедает ее, т.е мы применяем девочку к конфетам - это функтор.

Есть коробка с конфетами (контейнер) и девочка (функция). Только девочка лежит и спит внутри коробки. Сначала достаем девочку из коробки, а та в свою очередь достает конфету из коробки и съедает ее - это аппл. функтор.

anonymous
()

В воздухе густо запахло наваристым борщом.

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

Фишка в том, что в зависимости от контекста вместо девочки в коробку можно положить ее маму, или мальчика или собаку.

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

вместо девочки в коробку можно положить ее маму, или мальчика или собаку.

А конфеты все равно съест девочка

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

_автоматического_

да, с этим я погорячился.

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

И не знаю насчёт полезности, но есть

http://github.com/search?q=agda

http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Libraries

http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.PapersUsingAgda

http://homotopytypetheory.org/coq/

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

И для чего эти Agda пригодны? Ну кроме как с пацанами за пивом пальцы гнуть в присутствии дефченок?

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