April 2003 - Glasgow-haskell-users

RE: Existentials
by Simon Marlow 17 Apr '03

17 Apr '03

> "Simon Peyton-Jones" <simonpj(a)microsoft.com> writes: > > > GHC and Hugs both do. In fact, GHC supports arbitrary-rank > universal > > quantification. > > The example I tried failed, so I assumed it wasn't supported. > > $ cat Exists.hs > module Exists where > data T = forall a. Enum a => Foo (a->a) > f :: T -> (Int,Bool,Char) > f (Foo g) = (g 0, g False, g 'a') > $ ghc -fglasgow-exts -c Exists.hs > > Exists.hs:4: > Couldn't match `Int' against `Bool' > Expected type: Int > Inferred type: Bool > In the first argument of `g', namely `False' > In the definition of `f': (g 0, g False, g 'a') You've written an existential constructor. For universal quantification, write it like this: data T = Foo (forall a . Enum a => a -> a) a good illustration of the confusion caused by the dual use of forall, I guess :-) Cheers, Simon

2 1

RE: Setting "-package-conf" via environment variable?
by Simon Peyton-Jones 17 Apr '03

17 Apr '03

We've avoided envt variables (and .ghcrc files) so far, because it's one more thing we have to ask about when responding to bug mail. You can always make yourself a little shell script for my_ghc, or a shell alias. Would that do? Simon | -----Original Message----- | From: glasgow-haskell-users-admin(a)haskell.org [mailto:glasgow-haskell-users-admin@haskell.org] | On Behalf Of Peter Simons | Sent: 12 April 2003 11:18 | To: glasgow-haskell-users(a)haskell.org | | Hi, | | is there any way to provide GHC with a value for "-package-conf" via | an environment variable? I'd like to tell it to use a local package | config file in addition to it's own, but I'd like GHC to find that | "automatically". The users of the installation system should not have | to know about this. | | Any help is appreciated. | | Peter | | _______________________________________________ | Glasgow-haskell-users mailing list | Glasgow-haskell-users(a)haskell.org | http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

2 1

RE: compilation problem in glibc 2.3.2-27.9 RedHat 9
by Simon Marlow 17 Apr '03

17 Apr '03

> recently I've upgraded my RedHat box from 8 to 9. This > immediately gave > rise to a lot of problem due to incompatibility (I guess). > When I try to > compile my haskell library, for example (HaXml), it halted with this > error message > > > /usr/local/lib/ghc-5.02.3/libHSrts.a(RtsFlags.o)(.text+0x1b0): In > function `setupRtsFlags': > : undefined reference to `__ctype_b' > collect2: ld returned 1 exit status > > I then try to recompile my ghc from source, the compilation terminates > with the same error. > > for which I thought it is due to update on static links from glibc > version 2.2 to 2.3. But I think this has already been fixed by some > previous version. > > This problem is resolved until I reverted my glibc package back to > 2.3.2-4.80 Upgrading libc is not in general a safe thing to do when there are static libraries built against the old libc on your system. GHC includes several such static libraries. (It still amazes me that most Linux distributions have a package system with proper dependency tracking but still upgrade libraries without also upgrading everything that might have been broken by the upgrade.) We don't have RedHat 9 RPMs available for GHC 5.04.3 yet, I'm still hoping some kind person will build some... there is one bug in 5.04.3 that shows up with RedHat 9, but a fix was circulated on the bugs list recently. 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. Oops, I lie. Not in Hugs, only in GHC. Cheers, Simon

1 0

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

6 5

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

Re: Existentials
by Matt Fairtlough 17 Apr '03

17 Apr '03

>From: "Simon Peyton-Jones" <simonpj(a)microsoft.com> >To: "GHC users" <glasgow-haskell-users(a)haskell.org>, > >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. looks like it! >(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 would have said it _was_ worth the bother. Both forall and exists are very useful function names, in my opinion. >I don't think it affects NHC, because it's not H98 anyway. > > >Simon > > >_______________________________________________ >Glasgow-haskell-users mailing list >Glasgow-haskell-users(a)haskell.org >http://www.haskell.org/mailman/listinfo/glasgow-haskell-users > ----------------------------------------------------------------------- War in Iraq: NOT in my name. The war is killing civilians in the name of saving them and is likely to cause a huge humanitarian crisis. Join the StWC at http://www.stopwar.org.uk/ and make your opposition known http://www.sheffieldagainstwar.org.uk/ Matt Fairtlough 0114-22-21826 http://www.dcs.shef.ac.uk/~matt/ This signature is long and may not reflect the views of my employers. -----------------------------------------------------------------------

1 0

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

Chipworks Analyzes Process Technology Innovations
by Chipworks 16 Apr '03

16 Apr '03

1 0