<div dir="ltr">I heard Idris' author saying during a talk saying that he had once a branch which work even without the `!`.<div>That never got in because it scare users (according to Edwin for no rational reason).</div>
<div><br></div><div>I don't know enough the details, but I think dependent typing (and the Eff system) have probably a big role to play here... I mean Idris can go as far as "inferring implementation" so the type system allow the compiler to "understand" more and probably workaround ambiguity that Haskell might not be able to solve now (or even never).</div>
<div><br></div><div>That's just a very naive view of the problem, which might be as well erroneous so please correct me if I'm wrong.</div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On 20 May 2014 20:20, Evan Laforge <span dir="ltr"><<a href="mailto:qdunkan@gmail.com" target="_blank">qdunkan@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="HOEnZb"><div class="h5">On Tue, May 20, 2014 at 12:09 PM, Kim-Ee Yeoh <<a href="mailto:ky3@atamo.com">ky3@atamo.com</a>> wrote:<br>

><br>
> On Wed, May 21, 2014 at 1:38 AM, Evan Laforge <<a href="mailto:qdunkan@gmail.com">qdunkan@gmail.com</a>> wrote:<br>
>><br>
>> So perhaps the way forward is to find the old proposal (or make a new<br>
>> one, if it's gone), and see if Idris's solution applies to haskell.<br>
><br>
><br>
> Is Idris's solution written up anywhere? Mind sharing the link?<br>
<br>
</div></div>It's briefly documented in the tutorial, see do notation:<br>
<br>
<a href="http://eb.host.cs.st-andrews.ac.uk/writings/idris-tutorial.pdf" target="_blank">http://eb.host.cs.st-andrews.ac.uk/writings/idris-tutorial.pdf</a><br>
<br>
Looks like the key bit is "will lift expr as high as possible within<br>
the current scope".<br>
<div class="HOEnZb"><div class="h5">_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
</div></div></blockquote></div><br><br clear="all"><div><br></div>-- <br><div dir="ltr"><div><b>A\ois</b></div><div><div><a href="http://twitter.com/aloiscochard" target="_blank">http://twitter.com/aloiscochard</a></div>
<div><a href="http://github.com/aloiscochard" target="_blank">http://github.com/aloiscochard</a></div></div></div>
</div>