Re: [Haskell-cafe] Reply-To: Header in Mailinglists (was: About Fun with type functions example)
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 beginn...@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
arnaud.oq...@gmail.comwrote:
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 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: m...@joachim-breitner.de | ICQ# 74513189 | GPG-Key: 4743206C
JID: nome...@joachim-breitner.de | http://www.joachim-breitner.de/
Debian Developer: nome...@debian.org
signature.asc
Description: This is a digitally signed message part
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] About Fun with type functions example
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 Peeblespumpkin...@gmail.com 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 Baillyarnaud.oq...@gmail.com
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 Hesselinkhessel...@gmail.com
wrote:
On Thu, Nov 18, 2010 at 20:17, Arnaud Baillyarnaud.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 + 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] Re: borked windows environment, want to start over
On 11/18/2010 5:02 PM, Michael Litchard wrote: On Tue, Nov 16, 2010 at 4:39 PM, Michael Litchard mich...@schmong.org wrote: I think I may have borked things good using cygwin. I want to remove it and do a clean install of haskell platform w/out cygwin. What do I need to do to make sure all configuration files have been removed? Hmm, I wasn't precise enough in my question. My concern is there are configuration files related to the windows haskell-platform install that I don't know about , that need to be removed prior to doing a clean install. Or is it just a matter of doing a standard windows uninstall, will that take care of things? As for Cygwin interacting with your native Windows Haskell Platform installation, I think the only thing you have to worry about is if you manually added your Cygwin bin directories to the Windows %PATH% (this won't be done by the Cygwin installer, it's something you would have had to do yourself). That can cause Cabal to get confused, in my experience, depending on the precedence of your Cygwin path entries. Cygwin is generally pretty good about not messing with the host Windows environment... deleting the c:\cygwin directory and removing any (Windows) %PATH% entries is generally sufficient to fully uninstall it. If you created any cygwin-based Windows services (sshd, etc.) you'll have to delete those too, and there are a couple registry keys you could delete if you want, but aside from %PATH% there's nothing that should really mess with Haskell Platform... When you say you may have borked things good with cygwin, what specific problem(s) are you referring to? -- Mark Shroyer http://markshroyer.com/contact/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Problem with linking HDBC-ODBC
Hi Yesterday I upgraded to the new version of hdbc-odbc (2.2.3.1.). Then I rebuilt my own project, but the linker gives an error: . . . [88 of 90] Compiling CC ( CC.hs, C:\eclipseworkspace_fp1\ampersand\out\CC.o ) [89 of 90] Compiling Parser ( Parser.hs, C:\eclipseworkspace_fp1\ampersand\out\Parser.o ) [90 of 90] Compiling Main ( Main.hs, C:\eclipseworkspace_fp1\ampersand\out\Main.o ) Linking C:\eclipseworkspace_fp1\ampersand\bin\adl.exe ... C:\Documents and Settings\nl22118\Application Data\cabal\HDBC-odbc-2.2.3.1\ghc-6.12.3/libHSHDBC-odbc-2.2.3.1.a(Statement.o):fake:(.text+0x1a3d): undefined reference to `SQLNumParams' C:\Documents and Settings\nl22118\Application Data\cabal\HDBC-odbc-2.2.3.1\ghc-6.12.3/libHSHDBC-odbc-2.2.3.1.a(Statement.o):fake:(.text+0x3961): undefined reference to `SQLNumParams' collect2: ld returned 1 exit status Is there anything I do wrong? My environment is a windows machine. I use the haskell-platform. I upgraded to the current version of hdbc-odbc using cabal install. Any suggestions are welcome. -- View this message in context: http://haskell.1045720.n5.nabble.com/Problem-with-linking-HDBC-ODBC-tp3272152p3272152.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Reply-To: Header in Mailinglists
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: a simple question about types
Thank you for these excellent explanations. Best regards, Jerz -- View this message in context: http://haskell.1045720.n5.nabble.com/a-simple-question-about-types-tp3269519p3272344.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] About Fun with type functions example
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 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 Peeblespumpkin...@gmail.com
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 Baillyarnaud.oq...@gmail.com
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 Hesselinkhessel...@gmail.com
wrote:
On Thu, Nov 18, 2010 at 20:17, Arnaud Baillyarnaud.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 + 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
[Haskell-cafe] Re: Reply-To: Header in Mailinglists (was: About Fun with type functions example)
On Fri, 2010-11-19 at 04:55 +0100, Bastian Erdnüß wrote: Hi there, I just put an answer two this in beginn...@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. signature.asc Description: This is a digitally signed message part ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Reply-To: Header in Mailinglists (was: About Fun with type functions example)
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 uzytkown...@gmail.com wrote: On Fri, 2010-11-19 at 04:55 +0100, Bastian Erdnüß wrote: Hi there, I just put an answer two this in beginn...@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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] About Fun with type functions example
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 arnaud.oq...@gmail.comwrote:
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 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 Peeblespumpkin...@gmail.com
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 Baillyarnaud.oq...@gmail.com
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 Hesselinkhessel...@gmail.com
wrote:
On Thu, Nov 18, 2010 at 20:17, Arnaud Baillyarnaud.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 + 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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Reply-To: Header in Mailinglists (was: About Fun with type functions example)
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üß earth...@web.de wrote:
Hi there,
I just put an answer two this in beginn...@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 arnaud.oq...@gmail.comwrote:
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 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
Re: [Haskell-cafe] About Fun with type functions example
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 #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 arnaud.oq...@gmail.com
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
miguelim...@yandex.ru 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 Peeblespumpkin...@gmail.com
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 Baillyarnaud.oq...@gmail.com
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 Hesselinkhessel...@gmail.com
wrote:
On Thu, Nov 18, 2010 at 20:17, Arnaud Baillyarnaud.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 + 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
___
Haskell-Cafe mailing list
Re: [Haskell-cafe] Re: [Haskell] intent-typing
That was a great explanation of phantom types and type-families. I'm just getting started on understand type families and I was wondering why you didn't use data families in the truth table structure: type family Join a b type instance Join Safe Safe = Safe type instance Join Safe Unsafe = Unsafe type instance Join Unsafe Safe = Unsafe type instance Join Unsafe Unsafe = Unsafe My understanding is that since 'type' just produces a type synonym and the last three type instances are Unsafe, they are equivalent. Wouldn't it be better to have data instance Join Safe Unsafe ... so that the compiler can distinguish between Join Unsafe Safe, Join Safe Unsafe and Join Unsafe Unsafe ? -deech 2010/11/16 Tillmann Rendel ren...@informatik.uni-marburg.de: Hi, Marcus Sundman wrote: Hi, how would one go about implementing (or using if it's supported out-of-the-box) intent-typing* for haskell? A basic technique is to use newtype declarations to declare separate types for separate intents. module StringSafety ( SafeString () , UnsafeString () , quote , considerUnsafe ) where newtype SafeString = SafeString String newtype UnsafeString = UnsafeString String considerUnsafe :: String - UnsafeString considerUnsafe s = UnsafeString s quote :: UnsafeString - SafeString quote (UnsafeString s) = SafeString s' where s' = ... s ... This module does not export the SafeString and UnsafeString constructors, so we can be sure that no other code in the program can invent SafeStrings which are not really safe. Every string can be safely treated as unsafe, however, so we export a function considerUnsafe which does so. Now, if we type our interface to the outside world as getInput :: ... - UnsafeString sendOutput :: SafeString - ... we can be sure that a return value from getInput needs to pass through quote on its way to sendOutput, because quote is the only way to produce a SafeString. This guarantuees safety. It has, however, a practical problem: We can't use the usual String functions on UnsafeString or SafeString values. For instance, we can't concatenate two UnsafeStrings using (++). A naive solution would be to provide separate (++) functions for unsafe and safe strings: append_safe :: SafeString - SafeString - SafeString append_safe (SafeString x) (SafeString y) = SafeString (x ++ y) append_unsafe :: SafeString - SafeString - SafeString append_unsafe (UnsafeString x) (UnsafeString y) = UnsafeString (x ++ y) Note that at least append_safe needs to be implemented in and exported from the StringSafety module. That is a good thing, because this function needs to be carefully checked for safety. The programmer needs to prove (or unit-test, or at least think about) the following theorem: If a and b are safe strings, so is a ++ b. After this fact has been established, other modules are free to use append_safe however they like without possibly compromising safety. Now, the above approach should work, but is still rather impractical: We need to copy the definitions of all String functions for unsafe and safe strings. However, since the bodies of all these copies are actually identical, so we can use parametric polymorphism to abstract over the difference between UnsafeString and SafeString. One way to achieve this is to use phantom types. With phantom types, we declare only a single newtype for both safe and unsafe strings, but we annotate that type with an additional flag to distinguish safe from unsafe uses. module StringSafety ( AnnotatedString () , Safe () , Unsafe () , quote , considerUnsafe , append ) where data Safe = Safe data Unsafe = Unsafe newtype AnnotatedString safety = AnnotatedString String considerUnsafe :: String - AnnotatedString Unsafe considerUnsafe s = AnnotatedString s quote :: AnnotatedString Unsafe - AnnotatedString Safe quote (AnnotatedString s) = AnnotatedString s' where s' = ... s ... append :: AnnotatedString a - AnnotatedString a - AnnotatedString a append (AnnotatedString x) (AnnotatedString y) = AnnotatedString (x ++ y) Note that AnnotatedString does not really use its type parameter safety: That's why it is called a phantom type. The data constructor AnnotatedString can be freely used to convert between safe and unsafe strings, so we better not export it from the module. Inside the module, uses of the data constructor gives rise to proof obligations as above. So the programmer needs to reason that the following is true to justify the implementation and export of append: If x and y have the same safety level, then (x ++ y) has again that same safety level. So now, we still have to write a wrapper around each string operation, but at least we need to write only one
[Haskell-cafe] Impredicative Types
Hey everyone! I haven't had a chance to try out GHC 7 myself, but I saw in the documentation that Impredicative Types are still supported. Is this true? I thought that they were on their way out because they overcomplicated type checking; has this plan been changed? Cheers, Greg ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
RE: [Haskell-cafe] Impredicative Types
Yes, impredicative types are still in, but in a simpler form than before, along the lines of QML http://research.microsoft.com/en-us/um/people/crusso/qml/ I have been too busy with getting the new type checker working to describe or document it. Notably, I have not yet added syntax for QML's rigid type annotations, which leads to a loss of expressive power. too much to do! Bottom line: if you are interested in impredicative polymorphism, let me know. A good way to do so would be to register your interest on http://hackage.haskell.org/trac/ghc/ticket/4295 Just add your email address to the cc list, *and* write a comment giving an example of how you are using impredicative poly, and pointing to any further info. That'll help motivate me to do the remaining work! Thanks Simon | -Original Message- | From: haskell-cafe-boun...@haskell.org [mailto:haskell-cafe-boun...@haskell.org] | On Behalf Of Gregory Crosswhite | Sent: 19 November 2010 19:23 | To: Haskell Cafe | Subject: [Haskell-cafe] Impredicative Types | | Hey everyone! I haven't had a chance to try out GHC 7 myself, but I saw | in the documentation that Impredicative Types are still supported. Is | this true? I thought that they were on their way out because they | overcomplicated type checking; has this plan been changed? | | Cheers, | Greg | ___ | 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
Re: [Haskell-cafe] Impredicative Types
Awesome, thank you. :-) One more question out of pure curiosity, if you have the time: What is allowing you to keep them in? I thought that the problem was that they made a mess that touched every party of the type checker rather than being centralized in one place. Was there a trick you discovered that now allows you to support them without creating such a mess? Cheers, Greg On 11/19/10 11:45 AM, Simon Peyton-Jones wrote: Yes, impredicative types are still in, but in a simpler form than before, along the lines of QML http://research.microsoft.com/en-us/um/people/crusso/qml/ I have been too busy with getting the new type checker working to describe or document it. Notably, I have not yet added syntax for QML's rigid type annotations, which leads to a loss of expressive power. too much to do! Bottom line: if you are interested in impredicative polymorphism, let me know. A good way to do so would be to register your interest on http://hackage.haskell.org/trac/ghc/ticket/4295 Just add your email address to the cc list, *and* write a comment giving an example of how you are using impredicative poly, and pointing to any further info. That'll help motivate me to do the remaining work! Thanks Simon | -Original Message- | From: haskell-cafe-boun...@haskell.org [mailto:haskell-cafe-boun...@haskell.org] | On Behalf Of Gregory Crosswhite | Sent: 19 November 2010 19:23 | To: Haskell Cafe | Subject: [Haskell-cafe] Impredicative Types | | Hey everyone! I haven't had a chance to try out GHC 7 myself, but I saw | in the documentation that Impredicative Types are still supported. Is | this true? I thought that they were on their way out because they | overcomplicated type checking; has this plan been changed? | | Cheers, | Greg | ___ | 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
RE: [Haskell-cafe] Impredicative Types
read the QML paper! that's the trick. simpler, but with a heavier annotation burden than the more sophisticated approaches | -Original Message- | From: Gregory Crosswhite [mailto:gcr...@phys.washington.edu] | Sent: 19 November 2010 19:59 | To: Simon Peyton-Jones | Cc: Haskell Cafe; glasgow-haskell-us...@haskell.org | Subject: Re: [Haskell-cafe] Impredicative Types | | Awesome, thank you. :-) One more question out of pure curiosity, if | you have the time: What is allowing you to keep them in? I thought | that the problem was that they made a mess that touched every party of | the type checker rather than being centralized in one place. Was there | a trick you discovered that now allows you to support them without | creating such a mess? | | Cheers, | Greg | | On 11/19/10 11:45 AM, Simon Peyton-Jones wrote: | Yes, impredicative types are still in, but in a simpler form than before, along the | lines of QML | http://research.microsoft.com/en-us/um/people/crusso/qml/ | | I have been too busy with getting the new type checker working to describe or | document it. Notably, I have not yet added syntax for QML's rigid type annotations, | which leads to a loss of expressive power. | | too much to do! | | Bottom line: if you are interested in impredicative polymorphism, let me know. A | good way to do so would be to register your interest on | http://hackage.haskell.org/trac/ghc/ticket/4295 | Just add your email address to the cc list, *and* write a comment giving an example | of how you are using impredicative poly, and pointing to any further info. That'll help | motivate me to do the remaining work! | | Thanks | | Simon | | | -Original Message- | | From: haskell-cafe-boun...@haskell.org [mailto:haskell-cafe- | boun...@haskell.org] | | On Behalf Of Gregory Crosswhite | | Sent: 19 November 2010 19:23 | | To: Haskell Cafe | | Subject: [Haskell-cafe] Impredicative Types | | | | Hey everyone! I haven't had a chance to try out GHC 7 myself, but I saw | | in the documentation that Impredicative Types are still supported. Is | | this true? I thought that they were on their way out because they | | overcomplicated type checking; has this plan been changed? | | | | Cheers, | | Greg | | ___ | | 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] GitIt
The other day, I did a slightly foolish thing. I uttered the command cabal install gitit Actually, while I was foolish, it actually worked better than you'd think. It wanted to install several thousand billion packages, but all of them compiled without issue. Well, all except one. You see, for reasons that I have yet to determine, cabal is *convinced* that gitit transitively requires the unix package. Astonishingly, this doesn't work on Windows. :-P Question: Why does 90% of the network-related stuff on Hackage require the unix package? What's in there that's so network-related? I don't understand. We've *got* a portable network package that works on all platforms, so...? Anyway, on further investigation, it appears that the culprit is cautious-file. If a certain CPP flag it set, unix gets added to the Build-Depends: field. Except... I didn't set any CPP flags! What the hell? So I manually edit the package description (!), and now it builds and installs perfectly happily. So now I tell cabal to install gitit again... and it immediately tries to install unix, even though the only package that (it thinks) requires unix is already installed? Wuh? So I unpack gitit and tell cabal to build it. Building takes about 30 seconds. *Linking* takes about 4 minutes (??!) And then it fails due to some missing symbols. (No, I don't remember off the top of my head what they were.) At this point, I am completely lost. Does anybody have any ideas on how I can make GitIt work, short of installing Linux? I've searched and searched and I can't see a pre-built binary anywhere. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Impredicative Types
On 19/11/2010 08:09 PM, Simon Peyton-Jones wrote: read the QML paper! that's the trick. simpler, but with a heavier annotation burden than the more sophisticated approaches Use the Force, read the... citation? Hmm, doesn't have quite the same ring, does it? Use the Force, read the symposium? Well, whatever. I still think it's cool that Haskell generates this much published literature... ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Reply-To: Header in Mailinglists
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___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Impredicative Types
On 11/19/10 12:22 PM, Andrew Coppin wrote: Use the Force I tried, but I'm not yet strong enough in the Force to read citations with my eyes closed. :-( (PS: Thanks for pointing me to the paper, Simon!) Cheers, Greg ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] GitIt
Two possible fixes come to mind: 1) In the .cabal file for cautious-file, it says: Flag posix description: Use POSIX-specific features default: True You can use cabal install -fposix cautious-file to explicitly turn on POSIX support, and cabal install -f-posix cautious-file to explicitly turn it off. (From above, the default is the former.) So you can probably get this working with: cabal install cautious-file -f-posix; cabal install gitit Incidentally, it would be better for the .cabal file to detect that automatically with if os(windows), as e.g. Haskeline does. 2) If you have a local, edited installation of a package with the same version number as the one on Hackage, then it seems to confuse cabal install. (This may be a bug; I'm not sure.) Workaround is to bump the version in your local installation, e.g. from 0.1.5 to 0.1.5.0.0.0.1.; then cabal install won't try to rebuild it. Hope that helps, -Judah On Fri, Nov 19, 2010 at 12:20 PM, Andrew Coppin andrewcop...@btinternet.com wrote: The other day, I did a slightly foolish thing. I uttered the command cabal install gitit Actually, while I was foolish, it actually worked better than you'd think. It wanted to install several thousand billion packages, but all of them compiled without issue. Well, all except one. You see, for reasons that I have yet to determine, cabal is *convinced* that gitit transitively requires the unix package. Astonishingly, this doesn't work on Windows. :-P Question: Why does 90% of the network-related stuff on Hackage require the unix package? What's in there that's so network-related? I don't understand. We've *got* a portable network package that works on all platforms, so...? Anyway, on further investigation, it appears that the culprit is cautious-file. If a certain CPP flag it set, unix gets added to the Build-Depends: field. Except... I didn't set any CPP flags! What the hell? So I manually edit the package description (!), and now it builds and installs perfectly happily. So now I tell cabal to install gitit again... and it immediately tries to install unix, even though the only package that (it thinks) requires unix is already installed? Wuh? So I unpack gitit and tell cabal to build it. Building takes about 30 seconds. *Linking* takes about 4 minutes (??!) And then it fails due to some missing symbols. (No, I don't remember off the top of my head what they were.) At this point, I am completely lost. Does anybody have any ideas on how I can make GitIt work, short of installing Linux? I've searched and searched and I can't see a pre-built binary anywhere. ___ 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
Re: [Haskell-cafe] GitIt
On 19/11/2010 08:32 PM, Judah Jacobson wrote: Two possible fixes come to mind: 1) In the .cabal file for cautious-file, it says: Flag posix description: Use POSIX-specific features default: True Ah. I hadn't seen this bit. Yes, what's probably happened is that I altered the build dependencies, but the CPP flag was still turned on by default, resulting in a borked binary being built. You can use cabal install -fposix cautious-file to explicitly turn on POSIX support, and cabal install -f-posix cautious-file to explicitly turn it off. (From above, the default is the former.) Right. Yes, if I explicitly turn off POSIX support, that'll probably fix it. (I didn't know what the correct flag was to do that.) Incidentally, it would be better for the .cabal file to detect that automatically with if os(windows), as e.g. Haskeline does. Tell it to whoever maintains cautious-file. ;-) 2) If you have a local, edited installation of a package with the same version number as the one on Hackage, then it seems to confuse cabal install. (This may be a bug; I'm not sure.) It sure sounds like a bug to me... (And presumably a bug specifically with cabal-install, not the cabal library itself?) Workaround is to bump the version in your local installation, e.g. from 0.1.5 to 0.1.5.0.0.0.1.; then cabal install won't try to rebuild it. Ooo, yeah, but only if the package depending on cautious-file doesn't exactly pin down the required version number. ;-) Hope that helps, -Judah Yes, I think I know how to fix this now. PS. You have *no idea* how many different MD5 implementations I saw being compiled during this exercise...! ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Musings on type systems
OK, so how do types actually work? Musing on this for a moment, it seems that declaring a variable to have a certain type constrains the possible values that the variable can have. You could say that a type is some sort of set, and that by issuing a type declaration, the compiler statically guarantees that the variable's value will always be an element of this set. Now here's an interesting thought. Haskell has algebraic data types. Algebraic because they are sum types of product types (or, equivilently, product types of sum types). Now I don't actually know what those terms mean, but proceeding by logical inferrence, it seems that Either X Y defines a set that could be described as the union or sum of the types X and Y. So is Either what is meant by a sum type? Similarly, (X, Y) is a set that could be considered the Cartesian product of the sets X and Y. It even has product in the name. So is this a product type? So not only do we have types which denote sets of possible values, but we have operators for constructing new sets from existing ones. (Mostly just applying type constructors to arguments.) Notionally (-) is just another type constructor, so functions aren't fundamentally different to any other types - at least, as far as the type system goes. Now, what about type variables? What do they do? Well now, that seems to be slightly interesting, since a type variable holds an entire type (whereas normal program variables just hold a single value), and each occurrance of the same variable is statically guaranteed to hold the same thing at all times. It's sort of like how every instance of a normal program variable holds the same value, except that you don't explicitly say what that value is; the compiler infers it. So what about classes? Well, restricting ourselves to single-parameter classes, it seems to me that a class is like a *set of types*. Now, interestingly, an enumeration type is a set of values where you explicitly list all possible values. But once defined, it is impossible to add new values to the set. You could say this is a closed set. A type, on the other hand, is an open set of types; you can add new types at any time. I honestly can't think of a useful intuition for MPTCs right now. Now what happens if you add associated types? For example, the canonical class Container c where type Element c :: * We already have type constructor functions such as Maybe with takes a type and constructs a new type. But here we seem to have a general function, Element, which takes some type and returns a new, arbitrary, type. And we define it by a series of equations: instance Container [x] where Element [x] = x instance Container ByteString where Element ByteString = Word8 instance (Ord x) = Container (Set x) where Element (Set x) = x instance Container IntSet where Element IntSet = Int ... Further, the inputs to this function are statically guaranteed to be types from the set (class) Container. So it's /almost/ like a regular value-level function, just with weird definition syntax. Where *the hell* do GADTs fit in here? Well, they're usually used with phantom types, so I guess we need to figure out where phantom types fit in. To the type checker, Foo Int and Foo Bool are two totally seperate types. In the phantom type case, the set of possible values for both types are actually identical. So really we just have two names for the same set. The same thing goes for a type alias (the type keyword). It's not quite the same as a newtype, since then the value expressions do actually change. So it seems that a GADT is an ADT where the elements of the set are assigned to sets of different names, or the elements are partitioned into disjoint sets with different names. Hmm, interesting. At the same type, values have types, and types have kinds. As best as I can tell, kinds exist only to distinguish between /types/ and /type functions/. For type constructors, this is the whole story. But for associated types, it's more complicated. For example, Element :: * - *, however the type argument is statically guaranteed to belong to the Container set (class). In other news... my head hurts! _ So what would happen if some crazy person decided to make the kind system more like the type system? Or make the type system more like the value system? Do we end up with another layer to our cake? Is it possible to generalise it to an infinite number of layers? Or to a circular hierachy? Is any of this /useful/ in any way? Have aliens contacted Earth in living member? OK, I should probably stop typing now. [So you see what I did there?] Also, I have a sinking feeling that if anybody actually replies to this email, I'm not going to comprehend a single word of what they're talking about... ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org
Re: [Haskell-cafe] Musings on type systems
There's a lot of interesting material on this stuff if you start poking around :) http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ might be a good introduction. I'd consider typeclasses to be sets of types, as you said, but more generally, a relation of types. In that view, an MPTC is just an n-ary relation over types. Yes, you can get arbitrarily deep on the hierarchy of types and kinds. Agda does this, and even lets you define things that are polymorphic on the universe level. If you do read through TTFP, you might want to follow along with Agda, as it fits quite nicely. On Fri, Nov 19, 2010 at 4:05 PM, Andrew Coppin andrewcop...@btinternet.comwrote: OK, so how do types actually work? Musing on this for a moment, it seems that declaring a variable to have a certain type constrains the possible values that the variable can have. You could say that a type is some sort of set, and that by issuing a type declaration, the compiler statically guarantees that the variable's value will always be an element of this set. Now here's an interesting thought. Haskell has algebraic data types. Algebraic because they are sum types of product types (or, equivilently, product types of sum types). Now I don't actually know what those terms mean, but proceeding by logical inferrence, it seems that Either X Y defines a set that could be described as the union or sum of the types X and Y. So is Either what is meant by a sum type? Similarly, (X, Y) is a set that could be considered the Cartesian product of the sets X and Y. It even has product in the name. So is this a product type? So not only do we have types which denote sets of possible values, but we have operators for constructing new sets from existing ones. (Mostly just applying type constructors to arguments.) Notionally (-) is just another type constructor, so functions aren't fundamentally different to any other types - at least, as far as the type system goes. Now, what about type variables? What do they do? Well now, that seems to be slightly interesting, since a type variable holds an entire type (whereas normal program variables just hold a single value), and each occurrance of the same variable is statically guaranteed to hold the same thing at all times. It's sort of like how every instance of a normal program variable holds the same value, except that you don't explicitly say what that value is; the compiler infers it. So what about classes? Well, restricting ourselves to single-parameter classes, it seems to me that a class is like a *set of types*. Now, interestingly, an enumeration type is a set of values where you explicitly list all possible values. But once defined, it is impossible to add new values to the set. You could say this is a closed set. A type, on the other hand, is an open set of types; you can add new types at any time. I honestly can't think of a useful intuition for MPTCs right now. Now what happens if you add associated types? For example, the canonical class Container c where type Element c :: * We already have type constructor functions such as Maybe with takes a type and constructs a new type. But here we seem to have a general function, Element, which takes some type and returns a new, arbitrary, type. And we define it by a series of equations: instance Container [x] where Element [x] = x instance Container ByteString where Element ByteString = Word8 instance (Ord x) = Container (Set x) where Element (Set x) = x instance Container IntSet where Element IntSet = Int ... Further, the inputs to this function are statically guaranteed to be types from the set (class) Container. So it's /almost/ like a regular value-level function, just with weird definition syntax. Where *the hell* do GADTs fit in here? Well, they're usually used with phantom types, so I guess we need to figure out where phantom types fit in. To the type checker, Foo Int and Foo Bool are two totally seperate types. In the phantom type case, the set of possible values for both types are actually identical. So really we just have two names for the same set. The same thing goes for a type alias (the type keyword). It's not quite the same as a newtype, since then the value expressions do actually change. So it seems that a GADT is an ADT where the elements of the set are assigned to sets of different names, or the elements are partitioned into disjoint sets with different names. Hmm, interesting. At the same type, values have types, and types have kinds. As best as I can tell, kinds exist only to distinguish between /types/ and /type functions/. For type constructors, this is the whole story. But for associated types, it's more complicated. For example, Element :: * - *, however the type argument is statically guaranteed to belong to the Container set (class). In other news... my head hurts! _ So what would happen if some crazy person decided to make the kind system more like
Re: [Haskell-cafe] Musings on type systems
TAPL is also a great book for getting up to speed on type theory: http://www.cis.upenn.edu/~bcpierce/tapl/ I am no type theorist, and I nonetheless found it very approachable. I've never read TTFP; I will have to check that out. (-: On Nov 19, 2010, at 4:31 PM, Daniel Peebles wrote: There's a lot of interesting material on this stuff if you start poking around :) http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ might be a good introduction. I'd consider typeclasses to be sets of types, as you said, but more generally, a relation of types. In that view, an MPTC is just an n-ary relation over types. Yes, you can get arbitrarily deep on the hierarchy of types and kinds. Agda does this, and even lets you define things that are polymorphic on the universe level. If you do read through TTFP, you might want to follow along with Agda, as it fits quite nicely. On Fri, Nov 19, 2010 at 4:05 PM, Andrew Coppin andrewcop...@btinternet.com wrote: OK, so how do types actually work? Musing on this for a moment, it seems that declaring a variable to have a certain type constrains the possible values that the variable can have. You could say that a type is some sort of set, and that by issuing a type declaration, the compiler statically guarantees that the variable's value will always be an element of this set. Now here's an interesting thought. Haskell has algebraic data types. Algebraic because they are sum types of product types (or, equivilently, product types of sum types). Now I don't actually know what those terms mean, but proceeding by logical inferrence, it seems that Either X Y defines a set that could be described as the union or sum of the types X and Y. So is Either what is meant by a sum type? Similarly, (X, Y) is a set that could be considered the Cartesian product of the sets X and Y. It even has product in the name. So is this a product type? So not only do we have types which denote sets of possible values, but we have operators for constructing new sets from existing ones. (Mostly just applying type constructors to arguments.) Notionally (-) is just another type constructor, so functions aren't fundamentally different to any other types - at least, as far as the type system goes. Now, what about type variables? What do they do? Well now, that seems to be slightly interesting, since a type variable holds an entire type (whereas normal program variables just hold a single value), and each occurrance of the same variable is statically guaranteed to hold the same thing at all times. It's sort of like how every instance of a normal program variable holds the same value, except that you don't explicitly say what that value is; the compiler infers it. So what about classes? Well, restricting ourselves to single- parameter classes, it seems to me that a class is like a *set of types*. Now, interestingly, an enumeration type is a set of values where you explicitly list all possible values. But once defined, it is impossible to add new values to the set. You could say this is a closed set. A type, on the other hand, is an open set of types; you can add new types at any time. I honestly can't think of a useful intuition for MPTCs right now. Now what happens if you add associated types? For example, the canonical class Container c where type Element c :: * We already have type constructor functions such as Maybe with takes a type and constructs a new type. But here we seem to have a general function, Element, which takes some type and returns a new, arbitrary, type. And we define it by a series of equations: instance Container [x] where Element [x] = x instance Container ByteString where Element ByteString = Word8 instance (Ord x) = Container (Set x) where Element (Set x) = x instance Container IntSet where Element IntSet = Int ... Further, the inputs to this function are statically guaranteed to be types from the set (class) Container. So it's /almost/ like a regular value-level function, just with weird definition syntax. Where *the hell* do GADTs fit in here? Well, they're usually used with phantom types, so I guess we need to figure out where phantom types fit in. To the type checker, Foo Int and Foo Bool are two totally seperate types. In the phantom type case, the set of possible values for both types are actually identical. So really we just have two names for the same set. The same thing goes for a type alias (the type keyword). It's not quite the same as a newtype, since then the value expressions do actually change. So it seems that a GADT is an ADT where the elements of the set are assigned to sets of different names, or the elements are partitioned into disjoint sets with different names. Hmm, interesting. At the same type, values have types, and types have kinds. As best as I can tell, kinds exist only to distinguish between /types/ and / type
Re: [Haskell-cafe] Musings on type systems
On 10-11-19 04:39 PM, Matthew Steele wrote: TAPL is also a great book for getting up to speed on type theory: http://www.cis.upenn.edu/~bcpierce/tapl/ I am no type theorist, and I nonetheless found it very approachable. TAPL is surprisingly easy-going. It is long (many pages and many chapters, each chapter short), but it is the good kind of long: long but gradual ramp to get you to the hard stuff. Its first chapter explains convincingly why you should care about types to begin with (summary: a lightweight formal method). But it is not entirely for Haskell. It covers subtyping, and it doesn't cover type classes. It is also too bulky to be mobile (because it's long). ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] RegEx versus (Parsec, TagSoup, others...)
-BEGIN PGP SIGNED MESSAGE- Hash: SHA1 On 11/13/10 09:19 , Brent Yorgey wrote: On Fri, Nov 12, 2010 at 03:56:26PM -0800, Michael Litchard wrote: a Perl perspective. I let him into what I was doing, and he opined I should be using pcre. So now I'm second guessing my choices. Why do people choose not to use regex for uri parsing? Never believe anything anyone coming from a Perl perspective says about regular expressions. If a Perl expert tells you that regexps are the way to parse HTML/XML, you can safely conclude they've never actually tried to do it. - -- brandon s. allbery [linux,solaris,freebsd,perl] allb...@kf8nh.com system administrator [openafs,heimdal,too many hats] allb...@ece.cmu.edu electrical and computer engineering, carnegie mellon university KF8NH -BEGIN PGP SIGNATURE- Version: GnuPG v2.0.10 (Darwin) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/ iEYEARECAAYFAkzm93MACgkQIn7hlCsL25V6RACgxWMErR6armLoxyFooERkxnJa +I8Aniag5cRSZ9pdwsDeQ/nedMsxana+ =aiuP -END PGP SIGNATURE- ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Codec.Crypto.RSA question
Hi -cafe, I have a question about Codec.Crypto.RSA: how to enforce that (informally) decrypt . encrypt = id Consider this code: encrypt2 :: String - ByteString encrypt2 = fst . encrypt (mkStdGen n) pubKey encode decrypt2 :: ByteString - String decrypt2 = toString . decrypt privKey Since decrypt2 takes a bytestring which size is a multiple of the modulus, I've guessed that the encrypted bytestring is padded with '\NUL' characters. But then some strange stuff shows up: decrypt2 $ encrypt2 haskell returns \NUL\NUL\NUL\NUL\EOThaskell decrypt2 $ encrypt2 foobar returns \NUL\NUL\NUL\NUL\65533foobar I may use dropWhile to get rid of the NUL-padding, but can I assume that I'll always get a random character between my string and the padding? I tried to pad myself with NUL characters but I got almost the same results (the random char went to the head of the string) -- Cp ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Quasi quotation question
Hello, Is it possible for a quasi quoter to have access to information about haskell identifiers declared before the quasi-quotation? I tried the 'reify' function but without success. Just as in the following exemple: a = 6 x = [$expr|a|] Where the generated haskell code is a= 6 x = a Thank you Regards J-C ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Musings on type systems
On 19 November 2010 22:14, Albert Y. C. Lai tre...@vex.net wrote: On 10-11-19 04:39 PM, Matthew Steele wrote: TAPL is also a great book for getting up to speed on type theory: http://www.cis.upenn.edu/~bcpierce/tapl/ I am no type theorist, and I nonetheless found it very approachable. TAPL is surprisingly easy-going. It is long (many pages and many chapters, each chapter short), but it is the good kind of long: long but gradual ramp to get you to the hard stuff. Its first chapter explains convincingly why you should care about types to begin with (summary: a lightweight formal method). But it is not entirely for Haskell. It covers subtyping, and it doesn't cover type classes. It is also too bulky to be mobile (because it's long). IIRC It Does not deal Hindley-Milner type system at all. i.e. it does not cover ML's type system. Its successor ATTAPL :- http://www.cis.upenn.edu/~bcpierce/attapl/index.html Handles an ML like type systems using constraints. AFAICT This area area of type theory's history is not covered properly in any of the sources I have came across. Aaron ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] DPH and GHC 7.0.1
I was hoping to play around with Data.Parallel.Haskell (dph) but noticed that it seems to have been exiled from ghc 7.0.1 which I just installed. It also doesn't seem to be in cabal. Anybody know how to use dph with 7.0.1 or has it been abandoned or something? ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] DPH and GHC 7.0.1
On 11/19/2010 05:24 PM, Gregory Propf wrote: I was hoping to play around with Data.Parallel.Haskell (dph) but noticed that it seems to have been exiled from ghc 7.0.1 which I just installed. It also doesn't seem to be in cabal. Anybody know how to use dph with 7.0.1 or has it been abandoned or something? It's not abandoned. The library components have been separated from GHC. I'm sure the intent is to put it on Hackage. - Jake ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] DPH and GHC 7.0.1
There were some problems getting DPH to work well with the changes in GHC 7. There is more info in this mail: http://www.haskell.org/pipermail/cvs-ghc/2010-November/057574.html The short summary is that there will be a patch level release of GHC (7.0.2) that works well with DPH and the DPH packages will then be available for installation from Hackage. If you want to play with DPH now you can do so on GHC HEAD. -David On Nov 19, 2010, at 5:26 PM, Jake McArthur wrote: On 11/19/2010 05:24 PM, Gregory Propf wrote: I was hoping to play around with Data.Parallel.Haskell (dph) but noticed that it seems to have been exiled from ghc 7.0.1 which I just installed. It also doesn't seem to be in cabal. Anybody know how to use dph with 7.0.1 or has it been abandoned or something? It's not abandoned. The library components have been separated from GHC. I'm sure the intent is to put it on Hackage. - Jake ___ 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
Re: [Haskell-cafe] Musings on type systems
On Nov 19, 2010, at 6:22 PM, Aaron Gray wrote: IIRC It Does not deal Hindley-Milner type system at all. i.e. it does not cover ML's type system. Its successor ATTAPL :- http://www.cis.upenn.edu/~bcpierce/attapl/index.html Handles an ML like type systems using constraints. TAPL certainly covers the basic ML system -- which is pretty much the typed lambda calculus with first order polymorphism. What it doesn't do is cover type inference (or reconstruction) in any depth, although it does actually sketch at least one algorithm for HM type inference (including constraints) -- see chapter 22. You're right that ATTAPL covers much more in the realm of type inference, as well as plenty else. Cheers, Sterl.___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Quasi quotation question
On Nov 19, 2010, at 6:00 PM, jean-christophe mincke wrote: Hello, Is it possible for a quasi quoter to have access to information about haskell identifiers declared before the quasi-quotation? Nope. There are staging restrictions in place, since you can't sanely use things that haven't been fully defined and typechecked yet. Quasiquotation in fact runs at the renaming stage, before there's been any typechecking of the module yet, so the situation is even more dire. I tried the 'reify' function but without success. Just as in the following exemple: a = 6 x = [$expr|a|] However, in your example, you just want to generate `x = a`. You can do that just fine! Just generate a syntax tree that includes a variable named a. If there's no variable named a, or it has the wrong type, the syntax tree is still generated just fine -- the error just comes at the typechecking phase. It would be generating x = 6 that is impossible. Cheers, Sterl___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Musings on type systems
On 11/19/10 4:05 PM, Andrew Coppin wrote: So what would happen if some crazy person decided to make the kind system more like the type system? Or make the type system more like the value system? Do we end up with another layer to our cake? Is it possible to generalise it to an infinite number of layers? In addition to the Coq and Agda notion of universes you should also look at Tim Sheard's Omega[1], which takes Haskell and then goes all the way up. [1] http://web.cecs.pdx.edu/~sheard/papers/SumSchNotes.ps -- Live well, ~wren ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Musings on type systems
On Fri, Nov 19, 2010 at 1:05 PM, Andrew Coppin andrewcop...@btinternet.com wrote: So is Either what is meant by a sum type? Similarly, (X, Y) [...] is this a product type? Yes, and yes, although more generally speaking data Test = A Int Bool | B Test | C [Test] is a recursive ADT composed of sums (A ...| B... | C...) and products ((Int, Bool), Test, [Test]) Notionally (-) is just another type constructor, so functions aren't fundamentally different to any other types - at least, as far as the type system goes. Sort of, but I think your discussion later gets into exactly why it *is* fundamentally different. Where *the hell* do GADTs fit in here? Well, they're usually used with phantom types, so I guess we need to figure out where phantom types fit in. Well, I find it's better to think of GADTs as types that have extra elements holding proofs about their contents which you can unpack. For example: data Expr a where Prim :: a - Expr a Lam :: (Expr x - Expr y) - Expr (x - y) App :: Expr (x - a) - Expr x - Expr a (The type variables are arbitrary; I chose these specific odd ones for a reason which will shortly become clear) This can be reconstructed as an ADT with existentials and constraints: data Expr a = Prim a | forall x y. (a ~ (x - y)) = Lam (Expr x - Expr y) | forall x. App (Expr x - a) (Expr x) Conceptually, here is what these types look like in memory; [x] is a box in memory holding a pointer to an object of type x Expr a = tag_Prim, [a] or tag_Lam, type x, type y, proof that a = (x - y), [Expr x - Expr y] or tag_App, type x, [Expr x - a], [Expr x] Now, because we have type safety the compiler can actually erase all the types and equality proofs (although in the case of typeclass constraints it keeps the typeclass dictionary pointer around so that it can be used to call functions in the class). To the type checker, Foo Int and Foo Bool are two totally seperate types. In the phantom type case, the set of possible values for both types are actually identical. So really we just have two names for the same set. The same thing goes for a type alias (the type keyword). Not exactly; in the phantom type case, the two sets ARE disjoint in a way; there are no objects that are both Foo Int and Foo Bool (although there may be objects of type forall a. Foo a -- more on that later). Whereas the type keyword really creates two names for the same set. So what would happen if some crazy person decided to make the kind system more like the type system? Or make the type system more like the value system? Do we end up with another layer to our cake? Is it possible to generalise it to an infinite number of layers? Or to a circular hierachy? Is any of this /useful/ in any way? Absolutely! In fact, dependent type systems do exactly this; values can be members of types and vice versa. For example, in a dependently typed language, you can write something like data Vector :: * - Int - * where Nil :: forall a::*. Vector a 0 Cons :: forall a::*, n::Int. a - Vector a n - Vector a (n+1) append :: forall a::*, m::Int, n::Int. Vector a m - Vector a n - Vector a (m+n) append a 0 n Nil v = v append a m n (Cons a as) v = Cons a (append as v) However, - is special here, because it works at both the type level and the value level! That is, (Vector Int :: Int - *) can be applied to the value 5 to create (Vector Int 5), the set of vectors with 5 elements of type Int. And in fact, - is just a generalization of 'forall' that can't refer to the object on it's right hand side: append :: ( forall a :: *. forall m :: Int. forall n :: Int. forall v1 :: Vector a m. forall v2 :: Vector a n. Vector a (m+n) ) Since we don't refer to v1 or v2, we can abbreviate the 'forall' with -: append :: ( forall a :: *. forall m :: Int. forall n :: Int. Vector a m - Vector a n - Vector a (m+n) ) Now, however, you can run arbitrary code at the type level; just create an object with the type Vector Int (fib 5) and the compiler needs to calculate (fib 5) to make sure the length is correct! In compiler circles it's generally considered a bad thing when the compiler doesn't terminate, (one reason: how do I know if the bug is in my code or the compiler?) so these languages tend to force your code (or at least the code that can run at the type level) to terminate. There's another benefit to this: if it's possible that a type-level expression might not terminate, you lose type erasure and have to do the calculation at runtime. Otherwise you can create unsound expressions: cast :: forall a::*, b::*. (a = b) - a - b cast a b p x = x -- note that p is never evaluated, we just require the proof in scope! bottom :: forall a. a bottom a = bottom a -- if we evaluate this, we infinite loop unsound :: forall a::*, b::*. a - b unsound a b x = cast a b (bottom (a=b)) x print (unsound Int String 0) -- BOOM! Headshot to your type-safety. So, these languages
[Haskell-cafe] ANNOUNCE: Multiplate 0.0.1
Multiplate is a lightweight generic library for mutually recursive data types that won't make Conor lose his lunch. Multiplate is an alternative extension of the Uniplate/Compos core design to support mutually recursive datatypes in a way that is as powerful as Compos, almost as easy to use as Uniplate, and more portable than both of them. Multiplate does not require you to rewrite your data type, does not require run-time reflection, does not require GADTs, and does not even require multi-parameter type classes. It only requires rank 3 polymorphism. http://hackage.haskell.org/package/multiplate-0.0.1 A more detailed paper is forthcoming, but the library is available to try right now. -- Russell O'Connor http://r6.ca/ ``All talk about `theft,''' the general counsel of the American Graphophone Company wrote, ``is the merest claptrap, for there exists no property in ideas musical, literary or artistic, except as defined by statute.'' ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Musings on type systems
On 11/19/10 10:05 PM, Ryan Ingram wrote: On Fri, Nov 19, 2010 at 1:05 PM, Andrew Coppin wrote: So is Either what is meant by a sum type? Similarly, (X, Y) [...] is this a product type? Yes and no. Unfortunately there's some discrepancy in the terminology depending on who you ask. In the functional programming world, yes: sum types are when you have a choice of data constructors, a la Either; and product types are when you have multiple arguments in a data constructor, a la tuples.[1] However, in set theory and consequently in much of the research on dependent types, (the dependent generalization of) function types are called ``(dependent) product types'' and (the dependent generalization of) tuples are called ``(dependent) sum types''. There's a convoluted story about why this supposedly makes sense, but it doesn't match functional programmer's terminology nor the category theoretic terminology which is often invoked in type theory. ObTangent: this is much like the discrepancy between what is meant by ``source'' and ``target'' for folks who come from a machine learning background vs people who come from a signal processing background. Thankfully, most of the NLP folks caught in the middle have decided to go with the sensible (ML) definitions. [1] In a lazy language like Haskell we have to be careful about how we phrase this. There are different notions of products[2] depending on how they behave with respect to strictness, and depending on which one you choose you'll change how you have to reason about the types abstractly. This shows up canonically in the difference between domain products and smash products. When Haskell was designed they decided not to have two different versions of products in the language, so the tuples in Haskell aren't either of these two well-behaved kinds of products. This has ramifications when people try to reason about which program transformations are valid without introducing too much or too little laziness. By and large Haskell's tuples and ADTs are good at doing what you mean, but they do complicate the theory. [2] The same is true for different kinds of sums, but that's less problematic to deal with. Notionally (-) is just another type constructor, so functions aren't fundamentally different to any other types - at least, as far as the type system goes. Sort of, but I think your discussion later gets into exactly why it *is* fundamentally different. There are a few different ways to think about functions/arrows, which is why things get a bit strange. In functional programming this is highlighted by the ideas of ``functions as procedures'' vs ``functions as data'' ---even though we like to ignore the differences between those two perspectives. In category theoretic terms, those ideas correlate with morphisms vs exponential objects (or coexponential objects, depending). There's a category theoretic relation between exponentials and products (i.e., tuples) which is where un/currying comes from. But this is also why the Pi- and Sigma-types of dependently typed languages cause such issues. For example, there's an isomorphism between A-(C^B) and (A*B)-C in certain categories, namely curry/uncurry. And there's also an isomorphism between A*B and B*A, namely swapping the elements of a pair. Together these mean, A-(C^B) ~= (A*B)-C ~= (B*A)-C ~= B-(C^A). In Haskell this is obviously true because we have Prelude.flip. However, if we generalize this to dependent functions and dependent pairs then it's no longer true in general, because B may require an A to be in scope in order to be well-kinded; e.g., assuming f : (a:A) - (b: B a) - C a b, then what is the type of swap f? So on the one hand arrows and products are just type constructors like any other, but on the other hand they're not. It's sort of like how zero and one are natural numbers, but they're specialer than the other natural numbers (you need them in order to define the rest of Nat; they have special behavior with respect to basic operations like (+), (*),...; etc). ObTangent: When we dualize things to co-Cartesian closed categories we get the same thing, except it's between sums/coproducts and coexponentials. Where *the hell* do GADTs fit in here? Well, they're usually used with phantom types, so I guess we need to figure out where phantom types fit in. Well, I find it's better to think of GADTs as types that have extra elements holding proofs about their contents which you can unpack. Ultimately, GADTs are just a restricted form of Pi- and Sigma-types. The type argument whose value varies depending on the constructor isn't actually a phantom type. You can think of there being four sorts of type variables. There are the variables for parametric polymorphism where the _same_ variable occurs on both sides of the = defining the type. There are phantom types where the variable only occurs on the left. There are existential types where
Re: [Haskell-cafe] Musings on type systems
On 11/19/10 10:05 PM, Ryan Ingram wrote: Not exactly; in the phantom type case, the two sets ARE disjoint in a way; there are no objects that are both Foo Int and Foo Bool (although there may be objects of type forall a. Foo a -- more on that later). Whereas the type keyword really creates two names for the same set. Only in a way. I'd say there certainly are values that inhabit multiple types. I'll write one right now: []. Oh, here's another: Nothing. Or even: return. Sure, these values are typically the same ones as the ones inhabiting universal types, but there's nothing terribly strange about values inhabiting multiple types. If we were strictly adhering to System F then we would have to explicitly distinguish between Nothing, Nothing @Int, and Nothing @Bool so we wouldn't have the same term belonging to multiple types. But *we don't* strictly adhere to System F, and generally speaking we like to pretend we're in Curry-style languages even when the implementation is Church-style behind the scenes. There are some nice metatheoretical benefits to using Church-style formalisms, but that doesn't mean Church was any more right than Curry. If Church were really right then we wouldn't care so much about doing type inference or about making it require as few annotations as possible, since the right thing would be to annotate the terms in the first place. It's mostly a philosophical issue (albeit with tangible metatheoretical ramifications), but there's value in both perspectives. -- Live well, ~wren ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
