Полнота парадигм в Ruby

Сейчас пишу проект, в котором уже 6.5к строк на руби

Files:         130
Modules:        60
Classes:       109
Constants:     173
Methods:       554

Пока все идет нормально.

«содержимое объекта справа станет и содержимым объекта слева»

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

это уже дело архитектуры.

Разумеется. Для этого берут жабу или сишарп и решают такую важную с точки зрения архитектуры подзадачу глобально и надёжно.

даже не тьюринг-полный, что на нем писать

прописываю вам Тьюринг-похудение

нет, правда. агда же не general-purpose, что на ней писать, кроме матана?

агда же не general-purpose

Agda имеет доступ к рантайму GHC. чем конкретно она не general purpose?

что на ней писать, кроме матана?

что угодно. кроме интерпретаторов Agda, конечно

ну ясно. спорить не буду, не разбираюсь настолько. ждем ДЕ на агде, архиватор на агде и видеоплеер на агде.

ждем ДЕ на агде, архиватор на агде и видеоплеер на агде

а вот это, к сожалению, вряд ли - для этих целей всегда есть более удачная альтернатива. потенциальная возможность не означает, что она когда-нибудь будет реализована

Agda имеет доступ к рантайму GHC

Там же коиндукция есть. Например

forever : ∀ {A} → IO A → IO _
forever x = loop where loop = ♯ x >> ♯ (♯ loop >> ♯ return tt)

Потом собирается в бинарник в который быстро-быстро утекает вся память :)

кроме интерпретаторов Agda, конечно

Почему нет? Тут есть интерпретатор нетипизированного лямбда-исчисления с нетерминируемыми примерами.

А можете рассказать немного об Agda? Вы на ней работаете? Она полная по тьюрингу? Какова ее область применениея? Заранее благодраю!

А можете рассказать немного об Agda?

пожалуйста

Вы на ней работаете?

я на работе работаю. в TI

Она полная по тьюрингу?

не совсем

Какова ее область применениея?

на ней можно писать программы и, в значительной мере, доказывать их свойства

не совсем

Можешь пояснить что имеется в виду? То есть какую программу нельзя написать на agda какую можно написать на Тьюринг-полном языке?

Можешь пояснить что имеется в виду?

что-то вот такое. для меня связь между тотальностью и Тьюринг-полнотой - тот самый well known fact, на который ссылается автор; однако я охотно признаю, что он, скорее всего, прав

И он же пишет

Remember, «Agda is total, so it can't be Turing Complete» is as much nonsense as saying «Haskell is pure so it can't do IO».

и

Dependent types make a lot of people nervous. They make me nervous, but I like being nervous, or at least I find it hard not to be nervous anyway. But it doesn't help that there's quite such a fog of ignorance around the topic. Some of that's due to the fact that we all still have a lot to learn. But proponents of less radical approaches have been known to stoke fear of dependent types without always making sure the facts are wholly with them. I won't name names. These «undecidable typechecking», «Turing incomplete», «no phase distinction», «no type erasure», «proofs everywhere», etc, myths persist, even though they're rubbish.

Завершаемость и соответствующие проверки распространяются только на индуктивные типы данных и рекурсивные программы - там termination cheker следит за размерами вещей, но он не будет возражать против частичных незавершаемых корекурсивных программ над коиндуктивными типами данных:

http://wiki.portal.chalmers.se/agda/agda.php?n=ReferenceManual.Codatatypes

Values of coinductive types can be constructed using corecursion, which does not need to terminate, but has to be productive.

Полноценные IO, Streams, event machines, partiality monad, языки без строгой нормализации так реализуются. Это ещё не касаясь возможности отключать termination cheker и писать FFI к GHC.

То есть тотальность/завершаемость и частичность/незавершаемость разделены подобно тому как разделены чистый stateless и императивный stateful уровни в хаскеле.