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

монады есть? если есть, то не труЪ.

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

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

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

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

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

anonymous ()

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

Шо это?

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

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

Лол, нет. По-хорошему, да, но не в хаскеле :)

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

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

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

Ты уже ждк9 до ума довел? Крестостандарт прочитал? Нет? Иди читай.

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

вообще-то есть вот такая статья: http://habrahabr.ru/post/183150/

но хотелось бы, чтобы люди поясняли свои слова, когда обычному человеку в них ничерта не понятно

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

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

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

насколько оно близко к прологу?

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

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

makoven ★★★★★ ()

Как раз вспоминал про него в топике про новые уязвимости openSSL.

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

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

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

По-хорошему, да, но не в хаскеле

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

nemyax ()

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

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

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

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

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

Не всякая монада — аппликативный функтор.

ymn ★★★★★ ()

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

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

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

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

Bioreactor ★★★★★ ()

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

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

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

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

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

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

anonymous ()

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

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

Похоже, у этого содомита борщ был с грибами.

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

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

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

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

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

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

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

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

ymn ★★★★★ ()

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

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

Чтобы доказывать некоторые утверждения, например.

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

Что красное красивее зеленого?

Сомневаюсь я однако :)

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