Рабочий момент, Agda

[deniok]

Что-то у меня хаскелевский импорт вот так работает

{-# IMPORT System.IO #-}

а вот так ломается

{-# IMPORT System.IO (hPutStrLn) #-}

говоря Parse error (hPutStrLn). Хотя у Норелла в Dependently Typed Programming in Agda список импорта в примере используется. Agda 2.3.0.1 под Windows. Посмотрите у кого более свежая (2.3.2) и/или другая OS.

Comments

[deni-ok.livejournal.com]

Да, вполне можно. Я просто перевожу (уже перевёл) Dependently Typed Programming in Agda и заодно прогоняю весь код и тестирую на баги/устарелости (и шлю что нашёл авторскому коллективу :)

[maxim.livejournal.com]

К моменту публикации придется еще раз прогонять ;)

[deni-ok.livejournal.com]

Ну и что, подумаешь.
С молодым языком возиться приятно, пока стандарта и большой кодебазы нет, можно дать отмереть не очень нужным решениям.

[nivanych.livejournal.com]

А вот стандарт, пожалуй, уже направшивается.
Мне так видится, что сейчас агдочка более развита, чем хаскель в 97 году.

[deni-ok.livejournal.com]

Развита - это да, но зачем форсировать стандартизацию - не очень понятно. Мы и так справимся, а подсадить на Агду миллионы "индусов" - в этом есть гротеск, но нет эйдоса:)

[nivanych.livejournal.com]

Хотел было сказать, что до сих пор, на хаскель индусов не пересадили.
Но задумался — а ведь агдочка-то более простой язык, чем хацкель...

[sassa-nf.livejournal.com]

"а ведь агдочка-то..."

8-) КАК?!

[oxij.livejournal.com]

Если стандартизовать Агду, то придётся придумывать новую Агду для экспериментов. Компилятор и семантика языка там меняется (понемногу) в каждой версии, то что при этом старые программы в новых версиях иногда работают — чистая случайность.

[nivanych.livejournal.com]

GHC каким-то образом это удаётся.
Хотя и соглашусь, что он меняется сейчас меньше.

[oxij.livejournal.com]

Я тоже в прошлом году было взялся переводить Норелла, перевёл где-то половину, но легального способа опубликовать перевод статьи из Springer-Verilag не заплатив им много денег не существовало.
Сейчас что-то изменилось?

[deni-ok.livejournal.com]

Да? Это плохо. Может Лев (ау, lionet) что-то придумает.

А вы связывались с Нореллом по этому поводу?

[oxij.livejournal.com]

Я меншонил его в твитторе по этому поводу, но он не отреагировал, и я решил не продолжать.

[deni-ok.livejournal.com]

Ну поскольку моя цель скорее культуртрегерская, то в крайнем случае выложу полуанонимно.