The &quot;obvious&quot; way to write the result would be (stealing some syntax made up by ski on #haskell):<div><br></div><div>fromInt :: Int -&gt; (exists n. (Nat n) *&gt; n)</div><div>fromInt = ...</div><div><br></div><div>
meaning, &quot;at compile time we don&#39;t know the type of the result of fromInt, because it depends on a runtime value, but we&#39;ll tell you it&#39;s _some_ type (an existential) with a Nat instance&quot;.</div><div>
<br></div><div>Now, GHC haskell doesn&#39;t support existentials like that (you can make a custom data type that wraps them) but you can invert your thinking a bit and ask yourself _who_ can consume such an existential. The only kinds of functions that can deal with an arbitrary type like that (with a Nat instance) are those that are polymorphic in it. So instead of Int -&gt; (exists n. (Nat n) *&gt; n), we flip the existential and make a continuation and say Int -&gt; (forall n. (Nat n) =&gt; n -&gt; r) -&gt; r, meaning we take the Int, and a consumer of an arbitrary type-level natural, and return what the consumer returns on our computed type-level natural. We&#39;re forced to return exactly the value that the continuation returns because we know nothing at all about the `r` type variable.</div>
<div><br></div><div>Hope this helps!</div><div>Dan<br><br><div class="gmail_quote">On Fri, Nov 19, 2010 at 9:09 AM, Arnaud Bailly <span dir="ltr">&lt;<a href="mailto:arnaud.oqube@gmail.com">arnaud.oqube@gmail.com</a>&gt;</span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">Thanks a lot for the explanation. Summarizing: You can&#39;t calculate an<br>
exact type, but you don&#39;t care if the type of the continuation is<br>
properly set in order to &quot;hide&quot; the exact type of n? Am I right?<br>
<font color="#888888"><br>
Arnaud<br>
</font><div><div></div><div class="h5"><br>
On Fri, Nov 19, 2010 at 9:24 AM, Miguel Mitrofanov<br>
&lt;<a href="mailto:miguelimo38@yandex.ru">miguelimo38@yandex.ru</a>&gt; wrote:<br>
&gt;  A continuation.<br>
&gt;<br>
&gt; You can&#39;t know, what type your &quot;fromInt n&quot; should be, but you&#39;re not going<br>
&gt; to just leave it anyway, you&#39;re gonna do some calculations with it,<br>
&gt; resulting in something of type r. So, your calculation is gonna be of type<br>
&gt; (forall n. Nat n =&gt; n -&gt; r). So, if you imagine for a moment that &quot;fromInt&quot;<br>
&gt; is somehow implemented, what you&#39;re gonna do with it is something like<br>
&gt;<br>
&gt; calculate :: Int -&gt; r<br>
&gt; calculate i = let n = fromInt i in k n<br>
&gt;<br>
&gt; where k is of type (forall n. Nat n =&gt; n -&gt; r). Now we capture this pattern<br>
&gt; in a function:<br>
&gt;<br>
&gt; genericCalculate :: Int -&gt; (forall n. Nat n =&gt; n -&gt; r) -&gt; r<br>
&gt; genericCalculate i k = let n = fromInt i in k n<br>
&gt;<br>
&gt; Going back to reality, fromInt can&#39;t be implemented, but genericCalculate<br>
&gt; probably can, since it doesn&#39;t involve calculating a type.<br>
&gt;<br>
&gt; 19.11.2010 10:25, Arnaud Bailly пишет:<br>
&gt;&gt;<br>
&gt;&gt; Just after hitting the button send, it appeared to me that fromInt was<br>
&gt;&gt; not obvious at all, and probably impossible.<br>
&gt;&gt; Not sure I understand your answer though: What would be the second<br>
&gt;&gt; parameter (forall n . (Nat n) =&gt;  n -&gt;  r) -&gt;  r) ?<br>
&gt;&gt;<br>
&gt;&gt; Thanks<br>
&gt;&gt; Arnaud<br>
&gt;&gt;<br>
&gt;&gt; On Fri, Nov 19, 2010 at 1:07 AM, Daniel Peebles&lt;<a href="mailto:pumpkingod@gmail.com">pumpkingod@gmail.com</a>&gt;<br>
&gt;&gt;  wrote:<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; The best you can do with fromInt is something like Int -&gt;  (forall n.<br>
&gt;&gt;&gt; (Nat n)<br>
&gt;&gt;&gt; =&gt;  n -&gt;  r) -&gt;  r, since the type isn&#39;t known at compile time.<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; On Thu, Nov 18, 2010 at 2:52 PM, Arnaud Bailly&lt;<a href="mailto:arnaud.oqube@gmail.com">arnaud.oqube@gmail.com</a>&gt;<br>
&gt;&gt;&gt; wrote:<br>
&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt; Thanks a lot, that works perfectly fine!<br>
&gt;&gt;&gt;&gt; Did not know this one...<br>
&gt;&gt;&gt;&gt; BTW, I would be interested in the fromInt too.<br>
&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt; Arnaud<br>
&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt; On Thu, Nov 18, 2010 at 8:22 PM, Erik Hesselink&lt;<a href="mailto:hesselink@gmail.com">hesselink@gmail.com</a>&gt;<br>
&gt;&gt;&gt;&gt; wrote:<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; On Thu, Nov 18, 2010 at 20:17, Arnaud Bailly&lt;<a href="mailto:arnaud.oqube@gmail.com">arnaud.oqube@gmail.com</a>&gt;<br>
&gt;&gt;&gt;&gt;&gt; wrote:<br>
&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt; Hello,<br>
&gt;&gt;&gt;&gt;&gt;&gt; I am trying to understand and use the Nat n type defined in the<br>
&gt;&gt;&gt;&gt;&gt;&gt; aforementioned article. Unfortunately, the given code does not compile<br>
&gt;&gt;&gt;&gt;&gt;&gt; properly:<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; [snip]<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt; instance (Nat n) =&gt;  Nat (Succ n) where<br>
&gt;&gt;&gt;&gt;&gt;&gt;  toInt   _ = 1 + toInt (undefined :: n)<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; [snip]<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt; And here is the error:<br>
&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt; Naturals.hs:16:18:<br>
&gt;&gt;&gt;&gt;&gt;&gt;    Ambiguous type variable `n&#39; in the constraint:<br>
&gt;&gt;&gt;&gt;&gt;&gt;      `Nat n&#39; arising from a use of `toInt&#39; at Naturals.hs:16:18-39<br>
&gt;&gt;&gt;&gt;&gt;&gt;    Probable fix: add a type signature that fixes these type<br>
&gt;&gt;&gt;&gt;&gt;&gt; variable(s)<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; You need to turn on the ScopedTypeVariables extension (using {-#<br>
&gt;&gt;&gt;&gt;&gt; LANGUAGE ScopedTypeVariables #-} at the top of your file, or<br>
&gt;&gt;&gt;&gt;&gt; -XScopedTypeVariables at the command line). Otherwise, the &#39;n&#39; in the<br>
&gt;&gt;&gt;&gt;&gt; class declaration and in the function definition are different, and<br>
&gt;&gt;&gt;&gt;&gt; you want them to be the same &#39;n&#39;.<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; Erik<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt; _______________________________________________<br>
&gt;&gt;&gt;&gt; Haskell-Cafe mailing list<br>
&gt;&gt;&gt;&gt; <a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
&gt;&gt;&gt;&gt; <a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
&gt;&gt;&gt;<br>
&gt;&gt; _______________________________________________<br>
&gt;&gt; Haskell-Cafe mailing list<br>
&gt;&gt; <a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
&gt;&gt; <a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
&gt;<br>
&gt; _______________________________________________<br>
&gt; Haskell-Cafe mailing list<br>
&gt; <a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
&gt; <a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
&gt;<br>
_______________________________________________<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></div>