- Hugs-Users - Haskell.org

RE: Existentials
by Simon Marlow 22 Apr '03

22 Apr '03

> "Simon Marlow" <simonmar(a)microsoft.com> writes: > > > > The example I tried failed, so I assumed it wasn't supported. > > > > 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 :-) > > Exactly so. :-) If we change the syntax of existentials, would it > be possible to write my local universal example as I did originally > and have it work as expected? Or will it still be necessary to push > the quantifier inside the constructor? If the quantifier is outside the constructor, then it scopes over all the fields of the constructor. So, if you write data T = forall a . C t1 .. tn what should this mean (assuming you want a non-existential interpretation)? Perhaps the sensible meaning is that it is isomorphic to data T = C !(forall a . (t1,...,tn)) Cheers, Simon

1 0

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

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: 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