Как работает Джинн

Хорошо, я понимаю, что, вероятно, буду жалеть об этом всю оставшуюся жизнь, но... Как на самом деле работает Джинн?

В документации говорится, что он использует алгоритм, являющийся «расширением LJ», и указывается на длинную запутанную статью о LJT. Насколько я могу судить, это большая сложная система сильно формализованных правил для выяснения того, какие логические утверждения истинны, а какие ложны.Но это даже не началообъяснения того, как вы превращаете сигнатуру типа в исполняемое выражение. По-видимому, все сложные формальные рассуждения каким-то образом задействованы, но картина принципиально неполна.


Это немного похоже на тот случай, когда я пытался написать интерпретатор Паскаля на Бейсике. (Не смейтесь! Мне было всего двенадцать...) Я часами пытался понять это, и в конце концов мне пришлось сдаться. Я просто не мог понять, как, черт возьми, вы получаете от гигантской строки, содержащей всю программу, что-то, что вы можете сравнить с известными фрагментами программы, чтобы решить, что на самом деле делать.

Ответ, конечно же, заключается в том, что вам нужно написать нечто, называемое «анализатором». Как только вы понимаете, что это такое и что оно делает, вдруг все становится очевидным. О, это все равно не тривиально закодировать, но идеяпроста. Вам просто нужно написать фактический код. Если бы я знал о парсерах, когда мне было двенадцать, то, возможно, я бы не проводил два часа, просто глядя на пустой экран.

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

40
задан MathematicalOrchid 18 April 2012 в 21:08
поделиться