[Agda] Agda compiler optimizations

[Andreas Abel]

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...

Cheers,
Andreas

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
http://www2.tcs.ifi.lmu.de/~abel/