[Agda] Size limit on generated code?

[Edwin Brady]

On 3 Oct 2014, at 17:40, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:

>> The issue of the IO interface is maybe a subtle one.  An executable agda
>> program is, in my dreams,
>> a thing that (when executed) does something, intertwined with proofs
>> that the effect its execution will
>> have on the world meets a specification (expressed in terms of
>> state-predicate transformers, or some such foundation).  A lot of the
>> "proofs" might not be run-time-relevant, if the run-time system is to
>> trust the type-checker.  (But it may be relevant to the prosecution of
>> guilty parties when some airplane falls out of
>> the sky.)
> 
> Is there a library for this kind of IO yet?  (In Agda, Coq, or...)

Not in Agda or Coq, as far as I know, but in ...

The latest incarnation of the Effects library in Idris, as described in http://eb.host.cs.st-andrews.ac.uk/drafts/dep-eff.pdf (which will shortly appear in the proceedings of TFP 2014) allows this sort of reasoning about IO actions. There’s an example of it in action here: https://github.com/edwinb/idris-demos/blob/master/Hangman/hangman.idr

I’m sure something similar could be done fairly easily in Agda, but I don’t know how the compiler would react to it :).

Edwin.