- Glasgow-haskell-users

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

Re: Derivable type classes
by Christian Maeder 16 Apr '03

16 Apr '03

> The plan would be to automatically derive classes 'Typable' and 'Term' > for every data type, and make TypeReps a bit more efficient and clean. Good, I would appreciate that very much! > is anyone actually using the derivable-type-class stuff? > does anyone mind if they die No, I don't mind Christian

1 0

Derivable type classes
by Simon Peyton-Jones 16 Apr '03

16 Apr '03

Gentle GHC users I'm thinking of removing the "Derivable type classes" stuff from GHC. It's described in a paper that Ralph Hinze and I wrote http://research.microsoft.com/~simonpj/Papers/derive.htm and in the GHC user manual at http://www.haskell.org/ghc/docs/latest/html/users_guide/generic-classes. html But it's quite complicated to implement, it's incomplete (needs constructor-name stuff, and better lifting), and it sometimes gives huge types in the intermediate language (because of the encoding into tuples). So the benefit-to-cost ratio seems poor. Instead, I'm planning to implement the "Scrap your boilerplate" ideas for generic programming, described in another paper http://research.microsoft.com/~simonpj/papers/hmap/ The plan would be to automatically derive classes 'Typable' and 'Term' for every data type, and make TypeReps a bit more efficient and clean. Now, I could add the latter without removing the former, but GHC is big and fat enough already. So this message is really to ask is anyone actually using the derivable-type-class stuff? does anyone mind if they die Speak now or forever hold your peace. Simon Just to remind you, derivable type classes let you write definitions like class Eq t where (==), (/=) :: t -> t -> Bool -- generic default method (==){1} Unit Unit = True (==){a + b} (Inl x1) (Inl x2) = x1 == x2 (==){a + b} (Inr y1) (Inr y2) = y1 == y2 (==){a + b} _ _ = False (==){a * b} (x1 :*: y1) (x2 :*: y2) = x1 == x2 && y1 == y2

1 0

SSL & Glasgow Haskell?
by George Russell 14 Apr '03

14 Apr '03

Has anyone written client/server code in Glasgow Haskell that communicates over an SSL connection?

2 1

Say�n glasgow-haskell-users ,Baskuda.Com`da Bebek / Oyuncak Kategorisi A��ld�!
by Baskuda-12397 14 Apr '03

14 Apr '03

1 0

RE: Help Support
by Simon Marlow 14 Apr '03

14 Apr '03

> (A better mailing list for GHC questions is > Glasgow-haskell-users(a)haskell.org) > > I guess you can say > ghci Main.hs < run_main >& /dev/null > > where run_main contains > main A slight refinement: echo main | ghc -v0 Main.hs the -v0 avoids all extraneous output including the banner and the "Skipping Main..." message. Cheers, Simon

1 0

RE: Help Support
by Simon Peyton-Jones 14 Apr '03

14 Apr '03

(A better mailing list for GHC questions is Glasgow-haskell-users(a)haskell.org) I guess you can say ghci Main.hs < run_main >& /dev/null where run_main contains main That way, GHCi will load Main.hs, and then run 'main'. The output redirection would throw away the banner stuff. It'd be better to be able to say ghc --run Main.hs instead. If a lot of people are keen on that we'll probably do it. Simon | -----Original Message----- | From: haskell-admin(a)haskell.org [mailto:haskell-admin@haskell.org] On Behalf Of edgar cubides | Sent: 11 April 2003 19:51 | To: haskell(a)haskell.org | | Hi, i'm doing my undergraduate project about a HUGS tool. | | I have right now the following components: | | - A software client/server that is compilable on runHUGS. | | The problem is if i compile this software using GHC, can i run it on line.? | How can i do this? | | I apreciate any documentation about it. | | Thanks for your time. | | _________________________________________________________________ | The new MSN 8: advanced junk mail protection and 2 months FREE* | http://join.msn.com/?page=features/junkmail | | _______________________________________________ | Haskell mailing list | Haskell(a)haskell.org | http://www.haskell.org/mailman/listinfo/haskell

1 0