[Agda] Agda compiler optimizations

Andreas Abel andreas.abel at ifi.lmu.de
Tue Oct 22 22:18:17 CEST 2013

Well, yes, you could represent a type like

   Sigma n : Nat.  n < 256

by a byte, etc.

However, the compiler backend of Agda lacks such sophistication so far...


On 22.10.2013 16:00, agda newb wrote:
> Hello, i'm really new to agda and dependently typed languages but i'm really impressed by it.
> Just want to suggest something like "optimization trade" idea - you give proofs to compiler and compiler gives you optimizations.
> In dependently typed languges it should be easy to provide proofs for various things, set of these things includes proofs for various optimizations
> which can be safely performed on proven code.
> E.g:
> Prove that you natural numbers definition can't go out of certain bounds,
> write something like this {#- OPTIMIZATION NO_BIGINT MyNat #-} and compiler will throw away bigint support for numbers.
> That bigint example is quite silly but i think it can help to get the idea i'm trying share.
> What do you think about it?
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de

More information about the Agda mailing list