Рабочий момент, 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

[nivanych.livejournal.com]

Проверил — не работает в 2.3.0.1 и 2.3.2 под Gentoo и в 2.3.2 под NixOS.

Ну, я предпочитаю наоборот — экспортировать в хаскель и там склеивать получившийся код.
Думаю, что на будущее, будет правильнее агдочкой описать подмножество хаскеля, типа "core"... Там для этого есть достаточно средств в помощь, чтобы не делать это полностью самому, а только контролировать трансляцию.

[nivanych.livejournal.com]

Вот тут
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.ForeignFunctionInterface
ничего не сказано про (hPutStrLn) ивсётакое.
Можно ж и так импортировать, а играться на уровне модулей, они у агдочки прикольные.

[dmytro starosud (from livejournal.com)]

А зачем вам это надо?
Ведь есть же ИО и всякое такое (ну с коробки в смысле).