Nominolo on IRC pointed out that in some cases, GHC does already optimize this, if you can convince it that only one constructor is possible even at the core level: <a href="http://hpaste.org/40909/impossible_constructor_cases_o">http://hpaste.org/40909/impossible_constructor_cases_o</a><div>
<br></div><div>You can see that the generated core only has one pattern match and that the cmm from it doesn't check the tag.<br><div><br></div><div>However, in a quick sized vector example I tried, with a zip over it, it wasn't so smart and the core did contain matches between Cons and Nil, with the associated pattern match error generation code and double tag check. This was on GHC 7 RC1.</div>
<div><br></div><div>But maybe GHC could be made smarter about these things, or the Haskell codegen could craft GADTs that GHC is able to optimize suitably.</div><div><br></div><div>Anyway, not a big deal I guess :)</div><div>
<br><div class="gmail_quote">On Tue, Oct 26, 2010 at 3:01 PM, Andreas Abel <span dir="ltr"><<a href="mailto:andreas.abel@ifi.lmu.de">andreas.abel@ifi.lmu.de</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
<div class="im">On Oct 26, 2010, at 8:12 PM, Daniel Peebles wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
This is great news! Have you considered any optimizations along the lines of "Inductive Families Need Not Store Their Indices" too?<br>
It seems like compilation to Haskell/GHC would be a problem there, as there's no real way of avoiding a tag check on constructors. Or maybe we can convince the GHC folks to provide a backdoor of sorts there for it?<br>
</blockquote>
<br></div>
Some of these optimizations can be carried out without having the possibility to "jump over" a tag. For the others, one would have to encode data types constructorless, like in PiSigma, but this does not give nice Haskell code.<br>
<br>
data VecTag = VNil | VCons<br>
<br>
type Vec a = (VecTag, a)<br>
<br>
vnil :: Vec a<br>
vnil = (VNil, unsafeCoerce ())<br>
<br>
vcons :: a -> Vec a -> Vec a<br>
vcons a v = (VCons, unsafeCoerce (a,v))<br>
<br>
vhead :: Vec a -> a<br>
vhead (tag, t) = fst (unsafeCoerce t) -- jumps over VCons tag<br>
<br>
There is a lot of unsafeCoerce, seems like a high price to pay.<div class="im"><br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Anyway, I'm really excited about this development. Do you plan on keeping development "open" (with a public repository) and possibly accepting small contributions from external developers?<br>
</blockquote>
<br></div>
Sure, the plan is that this takes place in the Agda repository. Probably, the initial development won't be open, to get started, and because it is a student final project, but then it is public an open to all kinds of contributions. Was this what you were thinking?<br>
<br>
Cheers,<br><font color="#888888">
Andreas</font><div><div></div><div class="h5"><br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
On Tue, Oct 26, 2010 at 1:21 PM, Andreas Abel <<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a>> wrote:<br>
To my fellow Agda developers I'd like to announce that I plan to work on the compilation to Haskell. This is to avoid the duplication of efforts. I have two students who are interested to implement an improved compiler for Agda, probably they will start working beginning of next year.<br>
<br>
My plans are:<br>
- typed compilation (that will remove the bulk of unsafeCoerce applications)<br>
- useless code analyses (that will hopefully remove the bulk of static code)<br>
<br>
The useless code analyses have been described by Edwin Brady and colleagues:<br>
<br>
- "forcing" analysis: removing redundant constructor arguments<br>
- "collapsing" analysis (aka token type analysis): detecting unit types<br>
- identity analysis: eliminating applications of traversal functions that amount to the identity<br>
<br>
The output will be Haskell source, unless someone integrates external core into GHC in the meantime.<br>
I am tending towards a "pretty" Haskell output that is callable from other Haskell modules. That may encourage Haskell programmers to write parts of their projects in Agda even when they want to stick to Haskell as the main platform.<br>
<br>
Comments welcome.<br>
<br>
Cheers,<br>
Andreas<br>
<br>
<br>
</blockquote>
<br>
Andreas Abel <>< Du bist der geliebte Mensch.<br>
<br>
Theoretical Computer Science, University of Munich<br>
Oettingenstr. 67, D-80538 Munich, GERMANY<br>
<br>
<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a><br>
<a href="http://www2.tcs.ifi.lmu.de/~abel/" target="_blank">http://www2.tcs.ifi.lmu.de/~abel/</a><br>
<br>
<br>
<br>
</div></div></blockquote></div><br></div></div>