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><div class="gmail_quote"><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.</blockquote><div><br></div><div>Yeah, that makes sense, and probably isn't worth it in most cases. I just asked the people in #ghc on IRC and they said there wasn't an easy way to do this in GHC (especially if you have unboxed fields in your constructors), and it wouldn't be a simple change either. It probably isn't even a big win in most cases, but it'd be nice to do. Maybe someday Haskell itself will implement that optimization for multiple GADT matches, but people don't seem terribly interested.</div>
<div><br></div><div><br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;"><div class="im">
<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?</blockquote>
<div><br></div><div>Yeah, that makes sense, and sounds good.</div><div><br></div><div>Thanks,</div><div>Dan</div></div>