random crazy thought

[wizzard]

а вот был бы такой язык с мощной системой типов, способной на всякие proof`ы и inference, в духе Haskell или скорее Coq, и генерировал бы он код на чем-то, что бы легко интегрировалось с кровавым ентерпрайзом (Java/C++/Javascript/C#), и решал бы проблему Generation Gap (в смысле, чтобы можно было хинтить компилятору про фиксированные интерфейсы, и\или чтобы при компиляции можно было подгрести старую версию генерированного кода и показать вменяемые ошибки совместимости – цены б ему не было…

Comments

[ivan-ghandhi.livejournal.com]

Это Скале ещё работать и работать... но, в принципе-то, в том направлении, нет?

[wizzard]

Возможно. Но. хочется JS (для веба) и возможность править нагенерированное, с отражением изменений "обратно".

[justy-tylor.livejournal.com]

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

[wizzard]

>> только в динамическом языке

Да-да-да... Но в динамических языках на типы любят ложить болт :(

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

[thedeemon.livejournal.com]

1. Coq генерит код на OCaml
2. OCaml запускается на JVM (http://ocamljava.x9c.fr/)
3. Profit!

[wizzard]

Профит вижу. Дравбеки, наверное, тоже есть.

То есть в общем да, концептуально оно возможно. Devil in the details. Тот же ur/web пытается такое делать, и для f# есть (правда, клозедсурс) компилятор в бинарь+JS+SQL. С точки зрения ленивого юзера осталось подождать всего чуть-чуть :)

[thedeemon.livejournal.com]

С точки зрения ленивого юзера проще не париться и продолжать педалить на РНР/Java/whatever.

Очень мало кто способен освоить Coq или Agda, и еще меньше тех, кто может что-то практически полезное на них сделать. Слишком сложные они.

[wizzard]

Под ленивым юзером я подразумеваю себя ;)

Хотя в Coq я и сам пока ничего вменяемого написать не могу, оно ж все-таки proof assistant а не proof generator...

[cd-riper.livejournal.com]

F#?

[wizzard]

Not flexible enough. На клиент-гуи не хватит.

[cd-riper.livejournal.com]

почему?

[wizzard]

понятно что оно тьюринг-полное, да.

я видел компилятор f# в js (не вживую, видел только генерированный код).

но хочется возможность вносить правки и делать обратную трансформацию, а для нее надо компилятор переписать на вот зтом: http://www.seas.upenn.edu/~harmony/