April 2003 - Hugs-Users

RE: Existentials
by Simon Marlow 17 Apr '03

17 Apr '03

> > Does anyone have any opinions on this topic? It's a small > point, but > > one that bites quite frequently. It might even be possible > to arrange > > that 'forall' and 'exists' were only keywords in types, and not in > > terms, but I'm not sure it's worth the bother. > > 'forall' is already a special keyword that only applies > inside types, in both Hugs and GHC. Oops, I lie. Not in Hugs, only in GHC. Cheers, Simon

1 0

RE: Existentials
by Simon Marlow 17 Apr '03

17 Apr '03

> Does anyone have any opinions on this topic? It's a small point, but > one that bites quite frequently. It might even be possible to arrange > that 'forall' and 'exists' were only keywords in types, and not in > terms, but I'm not sure it's worth the bother. 'forall' is already a special keyword that only applies inside types, in both Hugs and GHC. Cheers, Simon

1 0

RE: Existentials
by Simon Peyton-Jones 17 Apr '03

17 Apr '03

| data T = Foo (forall a. Enum a => (a->a)) | | could indeed be local universal quantification. You can construct a | Foo with any function of type (Enum=>a->a), e.g. (Foo succ) is ok, | (Foo id) is not. When you pattern-match on the constructor, you get | back the original universal type, e.g. the following is valid: | | f :: T -> (Int,Bool,Char) | f (Foo g) = (g 0, g False, g 'a') | | It appears that ghc, Hugs, and nhc98 do not support local universals, | although hbc does. GHC and Hugs both do. In fact, GHC supports arbitrary-rank universal quantification. Simon

2 1

Existentials
by Simon Peyton-Jones 17 Apr '03

17 Apr '03

Dear GHC users, Hugs users, and Hugs implementors Many of you have grown to love existential data types, which we current write like this: data T = forall a. Foo a (a -> Int) Mark and I chose 'forall' rather than 'exists' to save grabbing another keyword from the programmer. And indeed, the type of the constructor Foo is Foo :: forall a. a -> (a->Int) -> T But every single time I explain this to someone, I find I have to make excuses for using the term 'forall'. I say "it really means 'exists', but we didn't want to lose another keyword". I have gradually concluded that our decision was a mistake. (In fairness to Mark, I think I was the primary advocate for it.) I reckon that we should Allow 'exists' Deprecate 'forall' (for defining existentials, that is) Eventually allow only 'exists' Does anyone have any opinions on this topic? It's a small point, but one that bites quite frequently. It might even be possible to arrange that 'forall' and 'exists' were only keywords in types, and not in terms, but I'm not sure it's worth the bother. I don't think it affects NHC, because it's not H98 anyway. Simon

5 4

Re: Existentials
by Hans Aberg 17 Apr '03

17 Apr '03

At 09:02 +0100 2003/04/17, Simon Peyton-Jones wrote: > Allow 'exists' > Deprecate 'forall' (for defining existentials, that is) > Eventually allow only 'exists' > > >Does anyone have any opinions on this topic? It's a small point, but >one that bites quite frequently. I have to come to think about this type of questions, but in another context, namely, when I was implementing a version of Prolog in the form of a proof-verification system building on metamathematics (= metalogic) rather than the standard logic. See for example, Elliott Mendelson, "Introduction to Mathematical Logic". You might pick down a program called "Qu-Prolog" to get an input on similar metalogical ideas in the form of a generalized Prolog system for bound variables: Qu-Prolog: http://www.svrc.it.uq.edu.au/pages/QuProlog_release.html Earlier versions http://svrc.it.uq.edu.au/Bibliography/svrc-tr.html?00-20 http://svrc.it.uq.edu.au/Bibliography/svrc-tr.html?00-21 Ergo http://www.svrc.it.uq.edu.au/pages/Ergo_release.html In such a context, it looks as though the natural extension of the type theory is axiomatic set theory. So I am therefore inclined to think that one should do whatever is correct in math, in order to pave the way for a natural development. As for naming conventions, I favor a naming without prepositions and endings, if possible. For example, "+" might be called "addition", even though "a + b" is read "a added to b". So one might use the words "all" and "exist" simply. At 10:05 +0200 2003/04/17, Doaitse Swierstra wrote: >I think that (in line with the other type notation conventions where >you do not have to be explicit) you should not be forced to write >anything at all, but I am sure I will remain a minority ;-} Actually, in metamathematics, there is a difference between quantified and unquantified formulas (variables with "all"). >Many of you have grown to love existential data types, which we current >write like this: > > data T = forall a. Foo a (a -> Int) > >Mark and I chose 'forall' rather than 'exists' to save grabbing another >keyword from the programmer. And indeed, the type of the constructor >Foo is > Foo :: forall a. a -> (a->Int) -> T > >But every single time I explain this to someone, I find I have to make >excuses for using the term 'forall'. I say "it really means 'exists', >but we didn't want to lose another keyword". A mathematical formulation of T is perhaps: T := V_{a in I} a x Hom(a, Int) where V sands for the disjoint union (= coproduct in the category of sets). So one computer approximating analogue might then be "exist". Hans Aberg

1 0

Say�n hugs-users ,Baskuda.Com`da Bebek / Oyuncak Kategorisi A��ld�!
by Baskuda-4435 16 Apr '03

16 Apr '03

1 0

Help!!
by Amy Barnes 16 Apr '03

16 Apr '03

Finally worked out my problem was not that I didn't know to load hugs, I have a file missing - [localhost:~] amy% hugs dyld: hugs can't open library: /usr/lib/libncurses.5.dylib (No such file or directory, errno = 2) Does anyone know what this file is or how I can obtain it? Thank you all again for your help. Kind regards, Amy Barnes

2 1

Question about using higher order polymorphism.
by Chiyan Chen 16 Apr '03

16 Apr '03

Hi, I am a ph.d student working in the area of typed programming langauges. And I am a happy Haskell user. Recently I am working on something that involves some advanced Haskell features. So I write to this mailing list to ask for help. My question is, in which version of Haskell can I use higher order polymorphism features (including first class polymorphic and first class existential types), and how to use them (what's the syntax). Is there any special packages or libraries that I need to install for using these features. For example, how should I define the following types: data T a b = TC (exists c. (a -> c, c -> b)) data B = BC (forall a. a -> a -> a) or more complex: data T b = TC (exist c. forall b. (a -> c, c -> b)) Thank you for you help. -- Chiyan Chen

2 1

Waiting to hear from you.
by Dr.Williams Okun. 06 Apr '03

06 Apr '03

Dear Sir, REQUEST ASSISTANCE/PARTNERSHIP . I am a member of a contract award and review committee .A contract already executed by a foreign firm in Africa in 1999 was over invoiced by us to the tune of $8,600,000.00 (Eight million six hundred thousand United states dollars). In the light of the above, I ask for your assistance in the transfer of this excess floating fund in a suspence account into a foreign account you may wish to provide, for it was a category "A" contract, (strictly reserved for foreign contractors) this informed my request, and also that I am forbidden by my government to run any foreign account. After the sucessful transfer, 20% of the total sum will go to you for your assistance. 5% of the total sum will be set aside to compensate for any incidental expenses incured by both parties. More details will be given in the course of correspondence. Your confidentiality is highly required since I am still in active service . Thank you for your anticipated co-operation. Regards, Dr.Williams Okun. TELEPHONE:234-1-776-3350. FAX:234-1-759-7912. You can contact me on my home email on. drokunwill(a)hknetmail.com

1 0

HEllo?
by ♡이라 불리우는 마음의 병.. 01 Apr '03

01 Apr '03

1 0