Helllo,<br><br><div class="gmail_quote">On Sat, Jul 30, 2011 at 2:11 AM,  <span dir="ltr">&lt;<a href="mailto:oleg@okmij.org">oleg@okmij.org</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
<div class="im"><br></div>
Second, what is the status of Nat kinds and other type-level data that<br>
Conor was/is working on? Nat kinds and optimized comparison of Nat<br>
kinds would be most welcome. Type level lists are better still<br>
(relieving us from Goedel-encoding type representations).<br>
<br></blockquote><div><br></div><div>I  did some work on adding a Nat kind to GHC, you can find the implementation in the &quot;type-nats&quot; branch of GHC.   The code there introduces a new kind, Nat, and it allows you to write natural numbers in types, using singleton types to link them to the value level.  The constraint solver for the type level naturals in that implementation is a bit flaky, so lately I have been working on an improved decision procedure.  When ready, I hope that the new solver should support more operations, and it should be much easier to make it construct explicit proof objects (e.g., in the style of System FC).</div>
<div>-Iavor</div><div>PS: I am going on vacation next week, so I&#39;ll probably not make much progress on the new solver in August.</div></div>