Существует ли ЯПЗТ для JVM ?

ЯП что?

Coq

DT

Coq же поверх Ocaml который не-JVM

Вроде бы есть приблуда Coq2Scala, которая умеет экстрактить кок в скалу, но я не проверял работоспобность этого решения.

Не хочется создавать новую тему, поэтому спрошу здесь. Зачем нужны «ЯП с зависимыми типами наподобие Agda / Coq / F*» ?

так, а что ты знаешь о теории типов?

Coq

Чтобы писать корректные программы.

ЯПЗТ - язык программирования закрытого типа??

язык программирования с зависимыми типами.

Те, кто что-то знают о теории типов (или вообще о существовании теории типов), такие вопросы не задают.

ну мало ли, может он еще не весь лямбда-куб разобрал.

Точно, сидит в Fω, и интересуется на лоре, зачем ему зависимые типы. Я тоже так сначала подумал.

так, а что ты знаешь о теории типов?

Чтобы писать корректные программы.

Я в общих чертах знаю, что такое зависимые типы. А можно краткий пример того, как ЯПЗТ помогут например писать более корректные ERP, игры, видеоплееры или браузеры? Я не троллю, я правда не понимаю.

Чем больше инвариантов выразимы в системе типов, тем меньше некорректных программ может написать программист.

Например, можно убедить компилятор в корректности алгоритма сортировки: http://twanvl.nl/blog/agda/sorting

В индустриальном программировании это все (пока?) неприменимо, потому что сложно/дорого/несовместимо с agile/etc

погугли про изоморфизм карри-говарда и исчисление предикатов.

Чем больше инвариантов выразимы в системе типов, тем меньше некорректных программ может написать программист.

Если бы я мог кастовать анонимусов, я бы скастовал динамически типизированного анонимуса %)

Динамически типизированный анонимус занят ловлей багов в юнит-тестах

Ты когда поймешь что такое «зависимые типы», напиши мне, ок? :)

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

Scala + shapeless