A continuation.
You can't know, what type your fromInt n should be, but you're not going to just leave it anyway, you're gonna do some calculations with it, resulting in something of type r. So, your calculation is
gonna be of type (forall n. Nat n = n - r). So, if you imagine for a moment
Thanks a lot for the explanation. Summarizing: You can't calculate an
exact type, but you don't care if the type of the continuation is
properly set in order to hide the exact type of n? Am I right?
Arnaud
On Fri, Nov 19, 2010 at 9:24 AM, Miguel Mitrofanov
miguelim...@yandex.ru wrote:
A
The obvious way to write the result would be (stealing some syntax made up
by ski on #haskell):
fromInt :: Int - (exists n. (Nat n) * n)
fromInt = ...
meaning, at compile time we don't know the type of the result of fromInt,
because it depends on a runtime value, but we'll tell you it's _some_
Yes it helps, although I am no type wizard!
Thanks a lot for these insights, it gives me some more ideas.
Best regards
Arnaud
On Fri, Nov 19, 2010 at 5:55 PM, Daniel Peebles pumpkin...@gmail.com wrote:
The obvious way to write the result would be (stealing some syntax made up
by ski on
Hello,
I am trying to understand and use the Nat n type defined in the
aforementioned article. Unfortunately, the given code does not compile
properly:
Here is the code:
module Naturals where
data Zero
data Succ a
class Nat n where
toInt :: n - Int
instance Nat Zero where
toInt _ = 0
On Thu, Nov 18, 2010 at 20:17, Arnaud Bailly arnaud.oq...@gmail.com wrote:
Hello,
I am trying to understand and use the Nat n type defined in the
aforementioned article. Unfortunately, the given code does not compile
properly:
[snip]
instance (Nat n) = Nat (Succ n) where
toInt _ = 1 +
Thanks a lot, that works perfectly fine!
Did not know this one...
BTW, I would be interested in the fromInt too.
Arnaud
On Thu, Nov 18, 2010 at 8:22 PM, Erik Hesselink hessel...@gmail.com wrote:
On Thu, Nov 18, 2010 at 20:17, Arnaud Bailly arnaud.oq...@gmail.com wrote:
Hello,
I am trying to
The best you can do with fromInt is something like Int - (forall n. (Nat n)
= n - r) - r, since the type isn't known at compile time.
On Thu, Nov 18, 2010 at 2:52 PM, Arnaud Bailly arnaud.oq...@gmail.comwrote:
Thanks a lot, that works perfectly fine!
Did not know this one...
BTW, I would be
Just after hitting the button send, it appeared to me that fromInt was
not obvious at all, and probably impossible.
Not sure I understand your answer though: What would be the second
parameter (forall n . (Nat n) = n - r) - r) ?
Thanks
Arnaud
On Fri, Nov 19, 2010 at 1:07 AM, Daniel Peebles
