ATS и зависимые типы

[thedeemon]

For you, when one sees emptiness
In terms of the meaning of dependent origination,
Then being devoid of intrinsic existence and
Possessing valid functions do not contradict.

-- Дже Цонкапа, "Сборник цитат для привлечения внимания", Союзпечать, 1402 г. (src)
В нашем детском саду всякий слышал о зависимых типах, что они умеют параметризоваться не

Comments

[gds]

нравится в качестве обзора "как оно бывает". Жду продолжения.

[ask_v]

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

:)

[thedeemon]

Разгружание мешков может обогатить духовно, но вряд ли интеллектуально. :)

В моей реальной жизни таких вещей тоже раньше не было, пока сам не стал их привносить. Столько всего есть в мире CS интересного и еще неизученного...

[ex_juan_gan]

Нет, ну попробовать-то можно поразгружать - потом сразу очень захочется обратно в программисты.

[nealar]

+1
Вроде бы, ничего особенного, зависимые типы там, линейная логика и всё такое.
Но, скорость въезжания и глубина проникновения автора в эти туманные материи поражает воображение.

[altmind]

спасибо за пост. несмотря на отсутствие подготовки, понял почти весь :) хочу еще постов об ATS

[thedeemon]

Если что-то конкретное непонятно, я с удовольствием попробую пояснить. Когда для других формулируешь и объясняешь, сам начинаешь лучше понимать.

[rigidus]

Присоединяюсь.

[nponeccop]

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

Благодаря наличию подготовки, не понял почти ничего.
Пойду лучше статейку почитаю.

[udpn]

Троллфейс в тексте _волшебен_.

[ex_juan_gan]

Классное чтение; спасибо!