April 2003 - Glasgow-haskell-users

RE: Existentials
by Hans Aberg 22 Apr '03

22 Apr '03

At 10:34 +0100 2003/04/22, Simon Marlow wrote: >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)? I think you have problem here because, you apply the quantifier to something which is not a predicate. This practise makes it hard to figure out what the semantics should be. For example, in the original example: >At 09:02 +0100 2003/04/17, Simon Peyton-Jones wrote: > data T = forall a. Foo a (a -> Int) if T is a well formed formula in a quantification theory there is an associated predicate P(a) = Foo a (a -> Int) from which one gets T := all a: P(a). One of the quantification axioms that I listed said: axiom Q4. t free for x in A |- (all x: A) => [x\t]A. It means that from T, one can plug in a value t (a term) [a\t]T = [a\t]P(a) to get Foo t (t -> Int) Is that not what you want? However, in math, quantifiers are only applied to predicates, not sets. For sets, one uses operations such as union, intersection and complement. It seems me that data types correspond to sets, not predicates. Thus, one should not use quantifiers "all" and "exist" at all on them, but something corresponding to sets instead. In naive set theory, one identifies the set S := { x | P(x) } with the predicate P(x). If one should get the set S from the closed formula T above, one first applies the axiom Q4 to get P(x) := [a\x]T, and then one can get S from P(x). In the example above, the set becomes S = { a | Foo a (a -> Int) } To begin with, this does not make logically sense, as Foo a (a -> Int) is supposed to return not logical values as is required by a predicate, but data of type T. It seems me that one should instead have someting like data T = union a. Foo a (a -> Int) or data T = disjointUnion a. Foo a (a -> Int) Then, when one instantiates, one will create another addition to the data type, which is how I think is what you really want. Right? Hans Aberg

1 0

DijitalCenter - Haftanın Mutlu Ürünleri
by DijitalCenter 22 Apr '03

22 Apr '03

1 0

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: Classes and interfaces, a naming restriction
by Simon Peyton-Jones 22 Apr '03

22 Apr '03

| Aparantly there's a restriction on having a class and a data type with | the same name. A strange thing to want to do? Maybe not, but illegal in Haskell. I think the main reason is distinguishing classes from instances in export and import lists: module Foo( IStream(..) ) where ... What gets exported, the class IStream or the data type IStream? The best you can do is put them in separate modules. Then you can name them as M1.IStream and M2.IStream if you want. Simon | Here's what I'd like to do: | | class IStream stream char where | readStream :: stream -> Int -> IO [char] | | data IStream char = forall stream. IStream stream char => IStream stream | | instance IStream (IStream char) char where | readStream (IStream stream) = readStream stream | | So here the *type* IStream is the representative member of the *class* | IStream. An OOP analogy is that a particular 'stream' such that | (IStream stream char) => stream | is a particular concrete class that inherits from a virtual base class IStream, | but a 'stream' that is of type IStream is a pointer/reference to something that | inherits from the virtual base class (or a COM interface pointer) | | With the former we have (potentially) static binding, with the latter it is necessarily | dynamic binding. So whenever I need a hetrogenious collection of streams I can apply: | IStream :: forall c s. (IStream s c) => s -> IStream c | | Do I really have to use data IStreamWrapper = ... instead? :-( | | Duncan | _______________________________________________ | Glasgow-haskell-users mailing list | Glasgow-haskell-users(a)haskell.org | http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

1 0

Classes and interfaces, a naming restriction
by Duncan Coutts 21 Apr '03

21 Apr '03

Hi, Aparantly there's a restriction on having a class and a data type with the same name. A strange thing to want to do? Here's what I'd like to do: class IStream stream char where readStream :: stream -> Int -> IO [char] data IStream char = forall stream. IStream stream char => IStream stream instance IStream (IStream char) char where readStream (IStream stream) = readStream stream So here the *type* IStream is the representative member of the *class* IStream. An OOP analogy is that a particular 'stream' such that (IStream stream char) => stream is a particular concrete class that inherits from a virtual base class IStream, but a 'stream' that is of type IStream is a pointer/reference to something that inherits from the virtual base class (or a COM interface pointer) With the former we have (potentially) static binding, with the latter it is necessarily dynamic binding. So whenever I need a hetrogenious collection of streams I can apply: IStream :: forall c s. (IStream s c) => s -> IStream c Do I really have to use data IStreamWrapper = ... instead? :-( Duncan

1 0

BLACKHOLE in heap profile
by Hal Daume III 19 Apr '03

19 Apr '03

My program which should use constant stack/heap is using a ton of heap. I profiled with -hd and the guy that's eating all the heap is BLACKHOLE. What does this mean? -- Hal Daume III | hdaume(a)isi.edu "Arrest this man, he talks in maths." | www.isi.edu/~hdaume

3 5

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