- Glasgow-haskell-users

Re: Existentials
by Albert Lai 17 Apr '03

17 Apr '03

Reminds me of the very intimate relationship between forall and exist in predicate logic. For example, (forall x. P=>Q) = (exist x. P)=>Q (exist x. P=>Q) = (forall x. P)=>Q provided Q mentions no x and the logic is classical enough. But the two quantifiers are closer than being duals to each other as in the above. I think they are re-incarnations of each other at times. How do you formalize "if an even prime number exists, it has to be 2"? You don't normally use the existential quantifier, no no. You write: forall x. even x /\ prime x ==> x=2

1 0

implicit parameters
by Dean Herington 17 Apr '03

17 Apr '03

There's apparently something very basic that I don't understand about implicit parameters. In the following program, compilation fails if either of the type declarations is omitted. What is "implicit" about implicit parameters, then? {-# OPTIONS -fglasgow-exts #-} main = print f1 f1 = let ?f = \ x -> x ++ x in f2 f2 :: (?f :: String -> String) => String f2 = f3 f3 :: (?f :: String -> String) => String f3 = ?f "x"

2 1

Re: Existentials
by Hans Aberg 17 Apr '03

17 Apr '03

You might determine whether it should be "all" or "exist" by means of a formal analysis: In metamathematics exist x: A is a rewriting of not(all x: not A) Then an example of a set of metamathematical axioms for the "all" quantifier is as follows (written as code in my program): theory Q. -- Quantification axioms, Mendelson, p.57 (called `K' there). { formula A, B, C term t free x. axiom Q1. A => (B => A). axiom Q2. (A => (B => C)) => ((A => B) => (A => C)). axiom Q3. (not B => not A) => ((not B => A) => B). axiom Q4. t free for x in A |- (all x: A) => [x\t]A. axiom Q5. x not free in A |- (all x: A => B) => (A => all x: B). axiom MP `modus ponens'. A, A => B |- B. axiom Gen `generalization'. A |- all x: A. } -- theory Q. Here, the symbol "|-" is the metamathematical implication, i.e., provability. Here, A |- B corresponds to Prolog B :- A. In Haskell, what is the analogue of the generalization axiom Gen? -- If you know that, then you know what should be "all" and "exist" in Haskell. Hans Aberg

1 0

forall vs. exists
by George Russell 17 Apr '03

17 Apr '03

1) The problem is basically whether you regard the type constructor as a way of constructing a type or of taking it apart. So using the current notation data A = forall x . B x => C x forall seems sensible if you think of a constructor as a way of constructing a type (for all x that's a B, C gives you an A), but not if want to take it apart, where your attitude is (there exists an x that's a B that's inside this C). I really can't see any reason for preferring the viewpoint of the constructor to the destructor, or vice-versa. So my vote would be for keeping things as they are. 2) I currently existential datatypes 17 times or thereabout. Replacing "forall" by "exists" through all these would be annoying, but not take very long. Also there seem to be two modules which use the variable name "exists", but while having to replace that would be annoying, again it wouldn't take very long. Altogether perhaps 20 minutes, if that. So while the suggested change-over would be a pain, it wouldn't be a major pain.

2 1

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