Язык программирования Agua

[arseniiv]

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

(Оффтоп)

К созданию его меня привело изучение единственного полного человеческого языка, который слишком известен, чтобы его называть.

Как вы увидите далее и совсем скоро, компилятор языка вы сможете написать даже сами — для этого не потребуется особо глубоких знаний, а только лишь данное описание.


Agua строго типизирована, но мощь языка не позволит вам написать код, в котором типы не сойдутся — необходимые преобразования благодаря устройству системы типов единственны и могут быть проведены неявно. Кроме того, мы добились автоматического вывода типов, так что их не нужно и невозможно указывать в коде (что дополнительно упрощает разбор кода и быстроту компиляции).


Операции над значениями в Agua никогда не приводят к исключениям; кроме того, благодаря детальности системы типов, для каждого набора типов аргументов и результата оказалось возможным подобрать операцию автоматически, так что отпадает необходимость указывать, какую операцию применять, так как типы аргументов и результата выводятся и известны ещё на этапе компиляции. Из этого следует, что все возможные операции язык уже содержит — отпадает надобность подключения внешних модулей.


Наконец, одной из жемчужин языка явилось свойство системы типов, позволяющее отказаться от запроса пользователя вводить какие угодно данные, поскольку и их можно определить — и тоже(!) на этапе компиляции! Тут, можно сказать, у меня отключается речевой центр и остаются одни эмоции.





Да здравствует Agua — язык одного единичного типа!

[_Ivana]

Уже не надеялся увидеть на этом форуме что-то интересное мне. Но после таких вступительных слов хотелось бы обещанного "Как вы увидите далее и совсем скоро", а то у меня много вопросов, но я их держу при себе в надежде на каминг сун.

ЗЫ если это первоапрельская шутка, тогда я очередной раз утвержусь в первоначальном мнении насчет форума.

[arseniiv]

(Оффтоп)

Не надо насчёт форума, утверждайтесь в мнении насчёт автора темы.

Ну, тут, в общем-то, я всё уже и сказал:

arseniiv в сообщении #999073 писал(а):

язык одного единичного типа!

(Спойлеры.)

В единичном типе $1$ одно значение $*$, так что любых функций вида $1^n\to1$ всего по одной: $f(*,\ldots,*)=*$. Отсюда все замечательные свойства.

[kp9r4d]

А мне понравилось :3 По-моему если после прочтения фразы

arseniiv в сообщении #999073 писал(а):

Наконец, одной из жемчужин языка явилось свойство системы типов, позволяющее отказаться от запроса пользователя вводить какие угодно данные, поскольку и их можно определить — и тоже(!) на этапе компиляции!

могли возникнуть сомнения, что это не шутка, то тут надо утверждаться кое в чём другом, и уж точно не в каком бы то ни было мнении насчёт форума.

[Mysterious Light]

Стесняюсь задать вопрос... как обстоят дела с полнотой по Тьюринга?

Или же этот язык так хорош, что не обременяет программиста и потенциального пользователя такими метафизическими сложностями?

[arseniiv]

Mysterious Light в сообщении #999785 писал(а):

Или же этот язык так хорош, что не обременяет программиста и потенциального пользователя такими метафизическими сложностями?

Да. Действительно, кому нужна эта полнота, да ещё и по Тьюрингу?

[_Ivana]

arseniiv в сообщении #999204 писал(а):

Не надо насчёт форума, утверждайтесь в мнении насчёт автора темы.

Вот, кстати, выясняется, что с точностью до наоборот. Автор темы в свое время оказывается придумывал кое-что интересное, и тогда же обещал придумать еще. Если бы не случайное упоминание темы в ссылке одного участника - не заметил бы ее. А по прошествии пяти лет вместо подобных тем - только шутки.

[arseniiv]

После того языка трудно придумать что-то не менее же оригинальное (получится какая-нибудь не особо интересная смесь False, Scheme и Python). После чтения вики Esolang — ещё труднее. Я решил не рисковать созданием подобных тем, тем более что вопросов для обсуждения как-то не возникало, а предложения мне проще запостить у себя. Да и самих идей особо нет — без мотивации они не придут. Если кто-нибудь подкинет стоящую идею…

Вообще в течение этого года (в смысле $\approx300$ дней перед данным, а не с начала календарного года) я как-то занялся выдумкой даже вполне неэзотерического языка, но потом увидел Ceylon и провалился в локальный минимум. Хороший такой минимум, ниже всех остальных пока.

-- Пн апр 06, 2015 09:07:12 --

(Это не значит, конечно, что я всё это время непрервно на нём что-то пишу. Сейчас вообще вспоминаю C и разглядываю SDL2.)

-- Пн апр 06, 2015 09:41:57 --

(Оффтоп)

arseniiv в сообщении #346945 писал(а):

(О, скажите, пожалуйста, что почитать про связь примитивно-рекурсивных функций и Тьюринг-полноты, а то не знаю.)

[EngineEnergy]

Сначала пошёл в гугл читать...

Цитата:

El agua es una sustancia cuya molécula está formada por dos átomos de hidrógeno y uno de oxígeno (H2O). Es esencial para la supervivencia de todas las formas conocidas de vida. El término agua generalmente se refiere a la sustancia en su estado líquido, aunque la misma puede hallarse en su forma sólida llamada hielo, y en su forma gaseosa denominada vapor.

Потом оказалось это просто ваша реклама.
И в сети такой язык не водится.

[arseniiv]

EngineEnergy в сообщении #1000968 писал(а):

И в сети такой язык не водится.

Что значит «не водится»? Вот же он — разве не в сети?

[Theoristos]

arseniiv в сообщении #1000996 писал(а):

Что значит «не водится»? Вот же он — разве не в сети?

Осталось доказать, что это - язык.

[arseniiv]

(Оффтоп)

Это упражнение для читателя.