Re: forall quantifier
Am Freitag, 6. Juni 2003 09:15 schrieb Simon Peyton-Jones: I forget whether I've aired this on the list, but I'm seriously thinking that we should change 'forall' to 'exists' in existential data constructors like this one. One has to explain 'forall' every time. But we'd lose a keyword. Or omit the keyword altogether (Doaitse has suggested this before). This is quite in line with uses of quantifiers elsewhere (in the horn rule `path(A,C) :- path(A,B), path(B, C)' the variable `C' is implicitly existentially quantified in the body). Cheers, Ralf ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: forall quantifier
I forget whether I've aired this on the list, but I'm seriously thinking that we should change 'forall' to 'exists' in existential data constructors like this one. One has to explain 'forall' every time. But we'd lose a keyword. exists (like forall in ghc only) could be used independently in a type or expression context without loosing something. Earlier explanations of forall as a sort of negated exists become plain wrong when now exists should replace forall at the very same position. Is moving the keyword exists up an option (and be backward compatible)? Or omit the keyword altogether (Doaitse has suggested this before). This is quite in line with uses of quantifiers elsewhere (in the horn rule `path(A,C) :- path(A,B), path(B, C)' the variable `C' is implicitly existentially quantified in the body). (you mean `B' is implicitly existentially quantified?!) Omitting the keyword may lead to unintended existential quantification and should be accompanied with a noticable warning (that may be switched off by experts). Haskell should support both implicit (with warning) and explicit existential (and universal) quantification! Christian ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: forall quantifier
On 2003-06-06 at 08:15BST Simon Peyton-Jones wrote: I forget whether I've aired this on the list, but I'm seriously thinking that we should change 'forall' to 'exists' in existential data constructors like this one. You did mention it, and there were several replies. I'd characterise them as mainly falling into two classes: Yes, the change is sensible and No, it's all right as it is so long as you stand on your head when reading programmes. It doesn't seem so difficult to me. It's a matter of thinking in terms of expressions for types and functions that return types. If you define type F a = forall t . (a, t) and subsequently write e:: F Int this is equivalent to writing e:: forall t . (Int, t) Now, although we don't have type expressions that correspond to the RHSs of data declarations, it seems perfectly reasonable to expect things to work as if we did -- the chief problem being that we can't see from the context which constructors are data and which type. So data D a = forall t . MkD a t leads us to interpret e:: D Int as e:: forall t . MkD a t I don't think that the problem of type and constructor namespaces detracts from this argument -- if anything, it points up a problem with data constructors, not quantifiers. From there it's easy to decide that to get an existential type we need to write data D a = exists t . MkD a t (and type F a = exists t . (a, t) looks quite reasonable too). One has to explain 'forall' every time. But we'd lose a keyword. Seems like a small price to pay. As Christian Maeder points out it is a loss only in the type variable namespace. As to omitting the quantifier, I say no, since the omission of quantifiers elsewhere corresponds uniformly to universal quantification. Jón PS that's one heck of an email address you have there, Simon! -- Jón Fairbairn [EMAIL PROTECTED] 31 Chalmers Road [EMAIL PROTECTED] Cambridge CB1 3SZ+44 1223 570179 (after 14:00 only, please!) ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: forall quantifier
Ketil Z. Malde wrote: I have a function declared as: anova2 :: (Fractional c, Ord b) = [a-b] - (a-c) - [a] - [Anova1 c] where the first parameter is a list of classifiers. I could simplify it, I guess, to something like classify :: Eq b = [a-b] - [a] - [[[a]]] ^^^ Isn't this one list too many? classify cs xs = ... where for each classifying function in cs, I would get the xs partitioned accordingly. E.g. classify [fst,snd] [(1,0), (1,2), (2,0)] would yield [ [(1,0), (1,2)], [(2,0)] -- classified by `fst` , [(1,0), (2,0)], [(1,2)]] -- classified by `snd` Now, obviously, the problem is that fst and snd, being passed in a list, needs to be of the same type; this complicates classifying a list of type [(Int,Bool)], for instance?. What you'd need would be an existential type of the form classify :: [exists b. Eq b = a-b] - [a] - [[a]] Such a type is not available directly in Haskell, but only through an auxilary data type: data Classifier a = forall b. Eq b = Classifier (a - b) Using that you should be able to implement classify :: [Classifier a] - [a] - [[a]] Cheers, - Andreas -- Andreas Rossberg, [EMAIL PROTECTED] Computer games don't affect kids; I mean if Pac Man affected us as kids, we would all be running around in darkened rooms, munching magic pills, and listening to repetitive electronic music. - Kristian Wilson, Nintendo Inc. ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: forall quantifier
I don't properly understand this either, but as it happens I was looking at this in the GHC user guide only yesterday... [[ : MkFoo :: forall a. a - (a - Bool) - Foo Nil :: Foo Notice that the type variable a in the type of MkFoo does not appear in the data type itself, which is plain Foo. For example, the following expression is fine: [MkFoo 3 even, MkFoo 'c' isUpper] :: [Foo] Here, (MkFoo 3 even) packages an integer with a function even that maps an integer to Bool; and MkFoo 'c' isUpper packages a character with a compatible function. These two things are each of type Foo and can be put in a list. : ]] -- http://www.haskell.org/ghc/docs/latest/html/users_guide/type-extensions.html#EXISTENTIAL-QUANTIFICATION At 15:20 04/06/03 +0200, Ketil Z. Malde wrote: Hi, This is one of those topics everybody else seems to be familiar with, but which I don't quite understand, and can't seem to find any good information about. I have a function declared as: anova2 :: (Fractional c, Ord b) = [a-b] - (a-c) - [a] - [Anova1 c] where the first parameter is a list of classifiers. I could simplify it, I guess, to something like classify :: Eq b = [a-b] - [a] - [[[a]]] classify cs xs = ... where for each classifying function in cs, I would get the xs partitioned accordingly. E.g. classify [fst,snd] [(1,0), (1,2), (2,0)] would yield [ [(1,0), (1,2)], [(2,0)] -- classified by `fst` , [(1,0), (2,0)], [(1,2)]] -- classified by `snd` Now, obviously, the problem is that fst and snd, being passed in a list, needs to be of the same type; this complicates classifying a list of type [(Int,Bool)], for instance¹. I have a vague notion this is solvable using quantifiers (since I ever only use Eq operations on the type), but I'm not sure exactly how, I can't seem to find a good tutorial, and my Monte-Carlo programming approach doesn't seem to be leading anywhere :-) Can somebody suggest a solution, or a place to look? -kzm ¹ I guess I can convert Bool to Int (True-1, False-0), but it's not very appealing, IMHO. -- If I haven't seen further, it is by standing in the footprints of giants ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell --- Graham Klyne [EMAIL PROTECTED] PGP: 0FAA 69FF C083 000B A2E9 A131 01B9 1C7A DBCA CB5E ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: forall quantifier
On Wed, Jun 04, 2003 at 02:46:59PM +0200, [EMAIL PROTECTED] wrote: Now I want to print part of the record. What I would like to do is the following putStrLn $ concatMap show [a,c,d] !!! bang !!! So what I actually do is putStrLn $ concat [show a, show c, show d] Works, but a little bit clumsy, especially with long lists. Is there a nice solution? You can do something like this: infixr 5 +++ (+++) :: Show a = a - [String] - [String] a +++ l = show a : l concat $ a +++ b +++ c +++ [] Best regards, Tom -- .signature: Too many levels of symbolic links ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
RE: forall quantifier
Yes, this would work, thanks. But let me extent my question: what if all the types would be in a class FakeClass which has function specialID :: a - ID and I would like to do foo $ map specialID [a,b,c,d] ? ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: forall quantifier
On Wed, Jun 04, 2003 at 04:43:10PM +0200, [EMAIL PROTECTED] wrote:
Yes, this would work, thanks.
But let me extent my question: what if all the types would be in a
class FakeClass which has function specialID :: a - ID and
I would like to do
foo $ map specialID [a,b,c,d]
?
Well, in Template Haskell you can do:
{-# OPTIONS -fglasgow-exts #-}
module B where
import Language.Haskell.THSyntax
data AnyShow = forall s. Show s = AnyShow s
instance Show AnyShow where
show (AnyShow s) = show s
metaMap :: ExpQ - ExpQ - ExpQ
metaMap qf ql = do
l - ql
case l of
Infix (Just x) (Con GHC.Base::) (Just xs) - do
let ys = metaMap qf (return xs)
[| ($qf $(return x) : $ys) |]
Con GHC.Base:[] - do
[| [] |]
ListExp xs - do
ys - sequence [ [| $qf $(return x) |] | x - xs ]
return $ ListExp ys
other - do
fail $ metaMap: unexpected syntax: ++ show other
and then:
map show $( metaMap [| AnyShow |] [| [1, 1.3, [1,2,3,4]] |]
and
map show $( metaMap [| AnyShow |] [| [1, 1.3, 'a'] |]
will work, but this won't
map show $( metaMap [| AnyShow |] [| [1, 1.3, 'a', [1,2,3,4]] |]
Is there a way to turn of typing within meta quotations?
Best regards,
Tom
--
.signature: Too many levels of symbolic links
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell
RE: forall quantifier
Now, obviously, the problem is that fst and snd, being passed in a
list, needs to be of the same type; this complicates classifying a
list of type [(Int,Bool)], for instance¹.
I have a similar problem.
Say I have a record:
data Rec = Rec { a :: Int, b :: Type1, c :: Type2, d :: Type3, ... }
rec = Rec { a = 1, b = ... }
Now I want to print part of the record. What I would like to do is the
following
putStrLn $ concatMap show [a,c,d]
!!! bang !!!
So what I actually do is
putStrLn $ concat [show a, show c, show d]
Works, but a little bit clumsy, especially with long lists.
Is there a nice solution?
Markus
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell
