
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 instance (Nat n) => Nat (Succ n) where toInt _ = 1 + toInt (undefined :: n) type One = Succ Zero type Two = Succ One And here is the error: D:\projets\sequencer>ghc Naturals.hs Naturals.hs:16:18: Ambiguous type variable `n' in the constraint: `Nat n' arising from a use of `toInt' at Naturals.hs:16:18-39 Probable fix: add a type signature that fixes these type variable(s) I use 6.12.3 on Windows XP. I am most probably missing an option but does not know which one. Thanks in advance for any advice, Arnaud

On Thu, Nov 18, 2010 at 20:17, Arnaud Bailly
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 + toInt (undefined :: n)
[snip]
And here is the error:
Naturals.hs:16:18: Ambiguous type variable `n' in the constraint: `Nat n' arising from a use of `toInt' at Naturals.hs:16:18-39 Probable fix: add a type signature that fixes these type variable(s)
You need to turn on the ScopedTypeVariables extension (using {-# LANGUAGE ScopedTypeVariables #-} at the top of your file, or -XScopedTypeVariables at the command line). Otherwise, the 'n' in the class declaration and in the function definition are different, and you want them to be the same 'n'. Erik

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
On Thu, Nov 18, 2010 at 20:17, Arnaud Bailly
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 + toInt (undefined :: n)
[snip]
And here is the error:
Naturals.hs:16:18: Ambiguous type variable `n' in the constraint: `Nat n' arising from a use of `toInt' at Naturals.hs:16:18-39 Probable fix: add a type signature that fixes these type variable(s)
You need to turn on the ScopedTypeVariables extension (using {-# LANGUAGE ScopedTypeVariables #-} at the top of your file, or -XScopedTypeVariables at the command line). Otherwise, the 'n' in the class declaration and in the function definition are different, and you want them to be the same 'n'.
Erik

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
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
wrote: On Thu, Nov 18, 2010 at 20:17, Arnaud Bailly
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 + toInt (undefined :: n)
[snip]
And here is the error:
Naturals.hs:16:18: Ambiguous type variable `n' in the constraint: `Nat n' arising from a use of `toInt' at Naturals.hs:16:18-39 Probable fix: add a type signature that fixes these type variable(s)
You need to turn on the ScopedTypeVariables extension (using {-# LANGUAGE ScopedTypeVariables #-} at the top of your file, or -XScopedTypeVariables at the command line). Otherwise, the 'n' in the class declaration and in the function definition are different, and you want them to be the same 'n'.
Erik
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Hi there, I just put an answer two this in beginners@haskell.org. It was not on purpose to move the topic. It's just that questions I feel I can answer are usually beginner level questions and so I'm not often writing in the cafe itself. It would make my life a little bit more easy if the mailing lists on haskell.org would add a Reply-To: header automatically to each message containing the address of the mailing list, the message was sent to. Usually that's the place where others would want to sent the answers to, I would suppose. Is there a reason that that's not the case? Am I missing something? Or am I supposed to install a more cleaver mail client which can do that for me? Is there one? Probably written in Haskell ;-) Cheers, Bastian On Nov 19, 2010, at 1:07, Daniel Peebles wrote:
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
wrote: 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
wrote: On Thu, Nov 18, 2010 at 20:17, Arnaud Bailly
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 + toInt (undefined :: n)
[snip]
And here is the error:
Naturals.hs:16:18: Ambiguous type variable `n' in the constraint: `Nat n' arising from a use of `toInt' at Naturals.hs:16:18-39 Probable fix: add a type signature that fixes these type variable(s)
You need to turn on the ScopedTypeVariables extension (using {-# LANGUAGE ScopedTypeVariables #-} at the top of your file, or -XScopedTypeVariables at the command line). Otherwise, the 'n' in the class declaration and in the function definition are different, and you want them to be the same 'n'.
Erik
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Hi Bastian, I generally observe the pattern that non-technical mailing lists tend to set this header to help the user, while technical mailing list assume (rightfully, IMHO) that the readers are fine without Reply-To. The reasons against setting that I recall at the moment are: * Mails meant to be send privately but accidentally sent to the list are worse than mails meant to be public but sent privately. * Users who send to the list with a Reply-To header set do not want that header to be lost. * With some clients, the Reply-To-All feature does not always work as expected when there is a Reply-To-Header. Most clients have a Reply-To-List feature (Evolution on Ctrl-L) that works fine, once you get used to it. Greetings, Joachim Am Freitag, den 19.11.2010, 04:55 +0100 schrieb Bastian Erdnüß:
Hi there,
I just put an answer two this in beginners@haskell.org. It was not on purpose to move the topic. It's just that questions I feel I can answer are usually beginner level questions and so I'm not often writing in the cafe itself.
It would make my life a little bit more easy if the mailing lists on haskell.org would add a Reply-To: header automatically to each message containing the address of the mailing list, the message was sent to. Usually that's the place where others would want to sent the answers to, I would suppose.
Is there a reason that that's not the case? Am I missing something? Or am I supposed to install a more cleaver mail client which can do that for me? Is there one? Probably written in Haskell ;-)
Cheers, Bastian
On Nov 19, 2010, at 1:07, Daniel Peebles wrote:
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
wrote: 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
wrote: On Thu, Nov 18, 2010 at 20:17, Arnaud Bailly
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 + toInt (undefined :: n)
[snip]
And here is the error:
Naturals.hs:16:18: Ambiguous type variable `n' in the constraint: `Nat n' arising from a use of `toInt' at Naturals.hs:16:18-39 Probable fix: add a type signature that fixes these type variable(s)
You need to turn on the ScopedTypeVariables extension (using {-# LANGUAGE ScopedTypeVariables #-} at the top of your file, or -XScopedTypeVariables at the command line). Otherwise, the 'n' in the class declaration and in the function definition are different, and you want them to be the same 'n'.
Erik
-- Joachim "nomeata" Breitner mail: mail@joachim-breitner.de | ICQ# 74513189 | GPG-Key: 4743206C JID: nomeata@joachim-breitner.de | http://www.joachim-breitner.de/ Debian Developer: nomeata@debian.org

Hi Bastian, Bastian Erdnüß wrote:
It would make my life a little bit more easy if the mailing lists on haskell.org would add a Reply-To: header automatically to each message containing the address of the mailing list, the message was sent to. Usually that's the place where others would want to sent the answers to, I would suppose.
The mailing lists on haskell.org set the List-Post: header to the adress of the list, and many mail clients use this information to allow "reply to list" somehow. If your client doesn't, you can manually work around the problem by "reply to all" and possibly deleting the email adress of the original sender. I use Mozilla Thunderbird 3.1.6, and I have configured it to show a button "reply to list" between "reply to all" and "forward". Tillmann

On Nov 19, 2010, at 13:54, Tillmann Rendel wrote:
Hi Bastian,
Bastian Erdnüß wrote:
It would make my life a little bit more easy if the mailing lists on haskell.org would add a Reply-To: header automatically to each message containing the address of the mailing list, the message was sent to. Usually that's the place where others would want to sent the answers to, I would suppose.
The mailing lists on haskell.org set the List-Post: header to the adress of the list, and many mail clients use this information to allow "reply to list" somehow. If your client doesn't, you can manually work around the problem by "reply to all" and possibly deleting the email adress of the original sender.
I see, the Reply-To header is evil.
I use Mozilla Thunderbird 3.1.6, and I have configured it to show a button "reply to list" between "reply to all" and "forward".
I use Apple Mail and at least I have a reply to all button. I just think that pollutes the others mailboxes (esp. yours, right now). I have to check if one can teach my mail client somehow a reply to list button. That with the List-Post header was a valuable information, thanks. Bastian

On Fri, 2010-11-19 at 04:55 +0100, Bastian Erdnüß wrote:
Hi there,
I just put an answer two this in beginners@haskell.org. It was not on purpose to move the topic. It's just that questions I feel I can answer are usually beginner level questions and so I'm not often writing in the cafe itself.
It would make my life a little bit more easy if the mailing lists on haskell.org would add a Reply-To: header automatically to each message containing the address of the mailing list, the message was sent to. Usually that's the place where others would want to sent the answers to, I would suppose.
Is there a reason that that's not the case? Am I missing something? Or am I supposed to install a more cleaver mail client which can do that for me? Is there one? Probably written in Haskell ;-)
Cheers, Bastian
On
Inserting the Reply-To header is against the RFC (if you like I can find exact quote). Reply-To is a header marking where *author* of message wants to receive replies. There are many reasons why you want to reply privately - for example you want to say about crossing the rules of netiquette etc., disclose some information not intended for public view (remote code execution bug) etc. You press "reply to author" button and... oops. it wasn't suppose to go public. There is a specialized header meant to specify mailing list which should and is be used. Regards PS. Probably it varies from ML to ML along with top and bottom posting along with 72-character limit in line.

I personnally use most of the time gmail, so I don't have access to a
Reply-To-List feature (or do I?).
I usually do Reply-to-all which I think is as I guess most mailers
remove duplicate mails. Am I right?
Arnaud
On Fri, Nov 19, 2010 at 3:16 PM, Maciej Piechotka
On Fri, 2010-11-19 at 04:55 +0100, Bastian Erdnüß wrote:
Hi there,
I just put an answer two this in beginners@haskell.org. It was not on purpose to move the topic. It's just that questions I feel I can answer are usually beginner level questions and so I'm not often writing in the cafe itself.
It would make my life a little bit more easy if the mailing lists on haskell.org would add a Reply-To: header automatically to each message containing the address of the mailing list, the message was sent to. Usually that's the place where others would want to sent the answers to, I would suppose.
Is there a reason that that's not the case? Am I missing something? Or am I supposed to install a more cleaver mail client which can do that for me? Is there one? Probably written in Haskell ;-)
Cheers, Bastian
On
Inserting the Reply-To header is against the RFC (if you like I can find exact quote). Reply-To is a header marking where *author* of message wants to receive replies.
There are many reasons why you want to reply privately - for example you want to say about crossing the rules of netiquette etc., disclose some information not intended for public view (remote code execution bug) etc.
You press "reply to author" button and... oops. it wasn't suppose to go public.
There is a specialized header meant to specify mailing list which should and is be used.
Regards
PS. Probably it varies from ML to ML along with top and bottom posting along with 72-character limit in line.
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

On Fri, 2010-11-19 at 15:25 +0100, Arnaud Bailly wrote:
I personnally use most of the time gmail, so I don't have access to a Reply-To-List feature (or do I?). I usually do Reply-to-all which I think is as I guess most mailers remove duplicate mails. Am I right?
Arnaud
As message have the same Message-ID the servers have to (or at least should - I'm too lazy right now to check the RFC) considered it 'the same' message (i.e. say - oh. I've already received this message). I tend to use reply-to-all or reply-to-list if the latter is present. Regards PS. Please note that sometimes people do not subscribe to receive messages. For example I asked a few times on various mailing lists for help when I was not interested in general discussion on topic asking to add me to CC. If the mailing list replaced Reply-To header it would required additional effort for responders instead of just pressing reply-to-all.

If the mailing list replaced Reply-To header it would required additional effort for responders instead of just pressing reply-to- all.
If the list were to add a "Reply-To:" header, but only in the case where one was not already present, that would seem to me to be ideal. (None of the internet polemics against Reply-To that I have seen, have considered this modest suggestion.) In the past, I have carefully used the Reply-To header to direct responses to a particular mailing list of many (e.g. when cross- posting an announcement). Yet because there is a culture of "Reply- To: is bad", and most MUAs do not have a "ReplyToList" option, most respondents end up pushing "Reply to all", which ignores my setting of "Reply-To:", and spams more people than necessary. Regards, Malcolm

On 2010-11-21 08:24 +0000, Malcolm Wallace wrote:
If the list were to add a "Reply-To:" header, but only in the case where one was not already present, that would seem to me to be ideal. (None of the internet polemics against Reply-To that I have seen, have considered this modest suggestion.)
This still breaks the reply-to-author feature.
In the past, I have carefully used the Reply-To header to direct responses to a particular mailing list of many (e.g. when cross- posting an announcement). Yet because there is a culture of "Reply- To: is bad", and most MUAs do not have a "ReplyToList" option, most respondents end up pushing "Reply to all", which ignores my setting of "Reply-To:", and spams more people than necessary.
MUAs will honour the Reply-To header when using the reply-to-all function: the problem is that Reply-To does not mean what you think it means. The header indicates where *you* want to receive replies. So the reply-to-all function will reply to *you* (by using the value in Reply-To), and to everyone else by copying the To and Cc lists. There is another header, Mail-Followup-To, which tells MUAs to also drop the To and CC lists. I know several posters to this very list use it. However, it needs to be used with care because it can fragment cross- list discussions and/or prevent non-subscribers from receiving messages. -- Nick Bowler, Elliptic Technologies (http://www.elliptictech.com/)

Hi, Nick Bowler wrote:
There is another header, Mail-Followup-To, which tells MUAs to also drop the To and CC lists.
Interesting. So is it a good idea to use Mail-Followup-To to move a discussion from one list to another? To: haskell@haskell.org CC: haskell-cafe@haskell.org Mail-Followup-To: haskell-cafe@haskell.org Subject: Foo on the iPhone (was: [Haskell] [ANN] Foo released!) Or should I rather swap To and CC? Or leave out haskell@... completely? Tillmann

On Sun, 2010-11-21 at 08:24 +0000, Malcolm Wallace wrote:
If the mailing list replaced Reply-To header it would required additional effort for responders instead of just pressing reply-to- all.
If the list were to add a "Reply-To:" header, but only in the case where one was not already present, that would seem to me to be ideal. (None of the internet polemics against Reply-To that I have seen, have considered this modest suggestion.)
Except... I don't use Reply-To because it defaults to sender so it will still be breaking the RFC - in most cases (as most people don't set the Reply-To header). Regards

Reply-to munging has come up many times on this list (and others).
See this page for information on why many people do not like Reply-to
munging:
http://marc.merlins.org/netrants/listreplyto.html
- jeremy
On Thu, Nov 18, 2010 at 9:55 PM, Bastian Erdnüß
Hi there,
I just put an answer two this in beginners@haskell.org. It was not on purpose to move the topic. It's just that questions I feel I can answer are usually beginner level questions and so I'm not often writing in the cafe itself.
It would make my life a little bit more easy if the mailing lists on haskell.org would add a Reply-To: header automatically to each message containing the address of the mailing list, the message was sent to. Usually that's the place where others would want to sent the answers to, I would suppose.
Is there a reason that that's not the case? Am I missing something? Or am I supposed to install a more cleaver mail client which can do that for me? Is there one? Probably written in Haskell ;-)
Cheers, Bastian
On Nov 19, 2010, at 1:07, Daniel Peebles wrote:
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
wrote: 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
wrote: On Thu, Nov 18, 2010 at 20:17, Arnaud Bailly
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 + toInt (undefined :: n)
[snip]
And here is the error:
Naturals.hs:16:18: Ambiguous type variable `n' in the constraint: `Nat n' arising from a use of `toInt' at Naturals.hs:16:18-39 Probable fix: add a type signature that fixes these type variable(s)
You need to turn on the ScopedTypeVariables extension (using {-# LANGUAGE ScopedTypeVariables #-} at the top of your file, or -XScopedTypeVariables at the command line). Otherwise, the 'n' in the class declaration and in the function definition are different, and you want them to be the same 'n'.
Erik
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

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
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
wrote: 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
wrote: On Thu, Nov 18, 2010 at 20:17, Arnaud Bailly
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 + toInt (undefined :: n)
[snip]
And here is the error:
Naturals.hs:16:18: Ambiguous type variable `n' in the constraint: `Nat n' arising from a use of `toInt' at Naturals.hs:16:18-39 Probable fix: add a type signature that fixes these type variable(s)
You need to turn on the ScopedTypeVariables extension (using {-# LANGUAGE ScopedTypeVariables #-} at the top of your file, or -XScopedTypeVariables at the command line). Otherwise, the 'n' in the class declaration and in the function definition are different, and you want them to be the same 'n'.
Erik
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

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 that "fromInt" is somehow implemented, what you're gonna do with it is something like calculate :: Int -> r calculate i = let n = fromInt i in k n where k is of type (forall n. Nat n => n -> r). Now we capture this pattern in a function: genericCalculate :: Int -> (forall n. Nat n => n -> r) -> r genericCalculate i k = let n = fromInt i in k n Going back to reality, fromInt can't be implemented, but genericCalculate probably can, since it doesn't involve calculating a type. 19.11.2010 10:25, Arnaud Bailly пишет:
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
wrote: 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
wrote: 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
wrote: On Thu, Nov 18, 2010 at 20:17, Arnaud Bailly
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 + toInt (undefined :: n) [snip]
And here is the error:
Naturals.hs:16:18: Ambiguous type variable `n' in the constraint: `Nat n' arising from a use of `toInt' at Naturals.hs:16:18-39 Probable fix: add a type signature that fixes these type variable(s) You need to turn on the ScopedTypeVariables extension (using {-# LANGUAGE ScopedTypeVariables #-} at the top of your file, or -XScopedTypeVariables at the command line). Otherwise, the 'n' in the class declaration and in the function definition are different, and you want them to be the same 'n'.
Erik
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

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
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 that "fromInt" is somehow implemented, what you're gonna do with it is something like
calculate :: Int -> r calculate i = let n = fromInt i in k n
where k is of type (forall n. Nat n => n -> r). Now we capture this pattern in a function:
genericCalculate :: Int -> (forall n. Nat n => n -> r) -> r genericCalculate i k = let n = fromInt i in k n
Going back to reality, fromInt can't be implemented, but genericCalculate probably can, since it doesn't involve calculating a type.
19.11.2010 10:25, Arnaud Bailly пишет:
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
wrote: 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
wrote: 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
wrote: On Thu, Nov 18, 2010 at 20:17, Arnaud Bailly
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 + toInt (undefined :: n)
[snip]
And here is the error:
Naturals.hs:16:18: Ambiguous type variable `n' in the constraint: `Nat n' arising from a use of `toInt' at Naturals.hs:16:18-39 Probable fix: add a type signature that fixes these type variable(s)
You need to turn on the ScopedTypeVariables extension (using {-# LANGUAGE ScopedTypeVariables #-} at the top of your file, or -XScopedTypeVariables at the command line). Otherwise, the 'n' in the class declaration and in the function definition are different, and you want them to be the same 'n'.
Erik
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

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_ type
(an existential) with a Nat instance".
Now, GHC haskell doesn'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 -> (exists
n. (Nat n) *> n), we flip the existential and make a continuation and say
Int -> (forall n. (Nat n) => n -> r) -> 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're forced to return exactly
the value that the continuation returns because we know nothing at all about
the `r` type variable.
Hope this helps!
Dan
On Fri, Nov 19, 2010 at 9:09 AM, Arnaud Bailly
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
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 that "fromInt" is somehow implemented, what you're gonna do with it is something like
calculate :: Int -> r calculate i = let n = fromInt i in k n
where k is of type (forall n. Nat n => n -> r). Now we capture this
On Fri, Nov 19, 2010 at 9:24 AM, Miguel Mitrofanov
wrote: pattern in a function:
genericCalculate :: Int -> (forall n. Nat n => n -> r) -> r genericCalculate i k = let n = fromInt i in k n
Going back to reality, fromInt can't be implemented, but genericCalculate probably can, since it doesn't involve calculating a type.
19.11.2010 10:25, Arnaud Bailly пишет:
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
wrote: 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
wrote: 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
wrote: On Thu, Nov 18, 2010 at 20:17, Arnaud Bailly
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 + toInt (undefined :: n)
[snip]
> And here is the error: > > Naturals.hs:16:18: > Ambiguous type variable `n' in the constraint: > `Nat n' arising from a use of `toInt' at Naturals.hs:16:18-39 > Probable fix: add a type signature that fixes these type > variable(s)
You need to turn on the ScopedTypeVariables extension (using {-# LANGUAGE ScopedTypeVariables #-} at the top of your file, or -XScopedTypeVariables at the command line). Otherwise, the 'n' in the class declaration and in the function definition are different, and you want them to be the same 'n'.
Erik
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

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
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_ type (an existential) with a Nat instance". Now, GHC haskell doesn'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 -> (exists n. (Nat n) *> n), we flip the existential and make a continuation and say Int -> (forall n. (Nat n) => n -> r) -> 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're forced to return exactly the value that the continuation returns because we know nothing at all about the `r` type variable. Hope this helps! Dan
On Fri, Nov 19, 2010 at 9:09 AM, Arnaud Bailly
wrote: 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
wrote: 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 that "fromInt" is somehow implemented, what you're gonna do with it is something like
calculate :: Int -> r calculate i = let n = fromInt i in k n
where k is of type (forall n. Nat n => n -> r). Now we capture this pattern in a function:
genericCalculate :: Int -> (forall n. Nat n => n -> r) -> r genericCalculate i k = let n = fromInt i in k n
Going back to reality, fromInt can't be implemented, but genericCalculate probably can, since it doesn't involve calculating a type.
19.11.2010 10:25, Arnaud Bailly пишет:
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
wrote: 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
wrote: 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
wrote: > > On Thu, Nov 18, 2010 at 20:17, Arnaud Bailly > 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 + toInt (undefined :: n) > > [snip] > >> And here is the error: >> >> Naturals.hs:16:18: >> Ambiguous type variable `n' in the constraint: >> `Nat n' arising from a use of `toInt' at Naturals.hs:16:18-39 >> Probable fix: add a type signature that fixes these type >> variable(s) > > You need to turn on the ScopedTypeVariables extension (using {-# > LANGUAGE ScopedTypeVariables #-} at the top of your file, or > -XScopedTypeVariables at the command line). Otherwise, the 'n' in > the > class declaration and in the function definition are different, and > you want them to be the same 'n'. > > Erik > _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
participants (11)
-
Arnaud Bailly
-
Bastian Erdnüß
-
Daniel Peebles
-
Erik Hesselink
-
Jeremy Shaw
-
Joachim Breitner
-
Maciej Piechotka
-
Malcolm Wallace
-
Miguel Mitrofanov
-
Nick Bowler
-
Tillmann Rendel