One thought: Num to 0 as ? to list?
Is there somethinig corresponding to Num concering lists? I mean there is + - /.. defined. + - are not type specific (Int, Double) neither is : [1,2] notation to Elements.. But what about different implementatins of lists? (linked lists? hash lists? array with index? In other words: why not overload (:) ? Then it would be possible to use "blah" for fast packed strings, too Then you could also implement implementations for C arrays and access them. (Sure you can do it anyway but not using syntactic sugar) One part of the answer is patterns? f 'a' = .. f _ = .. Marc
On Sun, 2006-08-13 at 20:36 +0200, Marc Weber wrote:
Is there somethinig corresponding to Num concering lists?
I mean there is + - /.. defined. + - are not type specific (Int, Double) neither is : [1,2] notation to Elements.. But what about different implementatins of lists? (linked lists? hash lists? array with index?
In other words: why not overload (:) ?
It might be nice to be able to use (:) to deconstruct other list like representations however the other list representations cannot efficiently support construction with (:). For example for the array-with-an-index representation it is an O(n) operation.
Then it would be possible to use "blah" for fast packed strings, too
An easier way of doing that might be to define literal strings to desugar into a function application much like numeric literals desugar into applications of fromIntegral. At the moment we can at least get the performance benefit of not converting via a list representation using GHC rules. So if you write: pack "blah" it gets transformed into: packAddr "blah"# where that literal string is just the address of a constant C string. Duncan
Hello Marc, Sunday, August 13, 2006, 10:36:39 PM, you wrote:
In other words: why not overload (:) ?
i have such proposal, more or less complete: 1) define [] as type class and [] and ':' as operations of this class: class [] c where [] :: c a -- creates empty container (:) :: a -> c a -> c a -- prepends new element to the head of container head :: c a -> a -- returns first container's element tail :: c a -> c a -- returns remaining container's elements 2) allow to use type classes in type declarations like the types itself. for example, allow the following: f :: Num a => a -> Int write as f :: Num -> Int and following: sequence :: Monad m => [m a] -> m [a] write as sequence :: [Monad a] -> Monad [a] these two changes together will change the meaning of existing list functions declarations, making them polymorphic functions that are ready to work with any container which is an instance of [] class. For example, the following declaration: foldr :: (a -> b -> b) -> b -> [a] -> b now will be treated as: foldr :: ([] c) => (a -> b -> b) -> b -> c a -> b 3) translate pattern matching on the left side of function equations to the equivalent pattern guards: foldr k z [] = z foldr k z (x:xs) = x `k` foldr k z xs turns into: foldr k z xx | xx==[] = z | x<-head xx, xs<-tail xx = x `k` foldrL k z xs 4) improve Haskell defaulting mechanism to allow declaring default container type used when there is not enough context: default [] => List main = print (head [1,2,3]) Here, [1,2,3] desugared into 1:2:3:[]. Because there is no information which allow to decide which container should be used, we defaults to use List instance: type List a = Cons a (List a) | Nil instance [] List where ..... Some Haskeller once said that lists are widely used in Haskell primarily because they are supported much better than any other data structure. All these changes together will allow to use any other container with the same easy as lists. i have attached a file which implements the idea without language changes. at the last end, it computes length and sum of two containers - list and array slice - using the same polymorphic functions: lengthL xs = foldrL (\_->(+1)) 0 xs sumL xs = foldrL (+) 0 xs Of course, this idea is not yet completely developed. Two problems that i see just now is dealing with pattern matching failures (f.e. trying to call 'head' for empty list) and building an hierarchy of classes representing various list features. at least, array slices don't support efficient ':' implementation. -- Best regards, Bulat mailto:Bulat.Ziganshin@gmail.com
Bulat Ziganshin
2) allow to use type classes in type declarations like the types itself. for example, allow the following:
f :: Num a => a -> Int write as f :: Num -> Int
and following:
sequence :: Monad m => [m a] -> m [a] write as sequence :: [Monad a] -> Monad [a]
How would you distinguish the class contexts of (for instance) sequenceLift :: (Monad m, Monad r) => [m a] -> r [a] if it were to be written instead as simply sequenceLift :: [Monad a] -> Monad [a] And how would one add multiple class constraints to a single type variable, for instance in: f :: (Functor m, Monad m) => (a->b) -> m [a] -> m b ? Regards, Malcolm
Hello Malcolm, Tuesday, August 22, 2006, 4:22:50 PM, you wrote:
2) allow to use type classes in type declarations like the types itself. for example, allow the following:
f :: Num a => a -> Int write as f :: Num -> Int
and following:
sequence :: Monad m => [m a] -> m [a] write as sequence :: [Monad a] -> Monad [a]
How would you distinguish the class contexts of (for instance) sequenceLift :: (Monad m, Monad r) => [m a] -> r [a] if it were to be written instead as simply sequenceLift :: [Monad a] -> Monad [a]
And how would one add multiple class constraints to a single type variable, for instance in: f :: (Functor m, Monad m) => (a->b) -> m [a] -> m b
both your examples cannot be written using proposed syntax what i propose is not full replacement of existing syntax - quite the contrary it is just a syntax sugar for most frequent cases of using classes in function signatures. the key idea is that in most cases we use only one type class for each type variable, and the same type for each occurrence of type class in the type: (+) :: Num -> Num -> Num This also simplifies the case when programmer has developed his code with one concrete type in mind and later decided to transform it into typeclass. In this case my idea allows to retain old definitions in most cases (and promoting [] to type class is very typical example here! we can browse prelude/list module and count how many definitions need to be changed if [] becomes type class) This proposal born from my experience of using type classes to make Streams library more flexible. i found that type signatures using type classes becomes larger and less readable and thought that they can be made no more complex than ordinary ones by using this idea. Java/C++ also allows to specify names of abstract classes/interfaces instead of concrete classes. Haskell's benefit is that general syntax allows to express more complex restrictions. I propose to combine it with the OOP-like simple syntax for simple cases (which is 80-90% of total ones) so, while this proposal is rather minor, i think that it is Good thing -- Best regards, Bulat mailto:Bulat.Ziganshin@gmail.com
On 8/22/06, Bulat Ziganshin
what i propose is not full replacement of existing syntax - quite the contrary it is just a syntax sugar for most frequent cases of using classes in function signatures. the key idea is that in most cases we use only one type class for each type variable, and the same type for each occurrence of type class in the type:
(+) :: Num -> Num -> Num
[...]
so, while this proposal is rather minor, i think that it is Good thing
I disagree. As a new learner to Haskell, I already have a hard time keeping Constructors, Types, and Classes straight. I know what they all are and what they all do, but sometimes I really have to think hard to remember which is which in a piece of code. What helps my understanding is that each has a specific place in the type signature (which I guess includes 'nowhere' regarding constructors). Being able to put Classes where Types go would just serve to muddle that understanding. Bryan Burgers
Hello Bryan,
On 2006-08-22, Bryan Burgers
so, while this proposal is rather minor, i think that it is Good thing
I disagree. As a new learner to Haskell, I already have a hard time keeping Constructors, Types, and Classes straight. I know what they all are and what they all do, but sometimes I really have to think hard to remember which is which in a piece of code. What helps my understanding is that each has a specific place in the type signature (which I guess includes 'nowhere' regarding constructors). Being able to put Classes where Types go would just serve to muddle that understanding.
This is an instance of a general conflict: should we sacrifice nice notation for ease of learning? You could make a similar case for list comprehensions, for example: they complicate matters for newcomers (yet another meaning of brackets and pipe), but once you get used to them, they may actually simplify code. However, this need not be a conflict at all. Introductory material can simply ignore syntactic sugar like list comprehensions and this new proposal (*). If there are independent tutorials of these "extra features", explaining their meaning in terms of basic haskell, someone learning haskell can learn to use them one at a time, as s/he encounters them in the wild. I agree that it may be complicating to have more than one way to write the same code. There is a balance between the gained ease of writing (and reading!) and the burden of having to do a mental translation when combining code using the different ways, but this should be kept distinct from the problem of learning Haskell. (*) In this specific instance one might (ab?)use the additional notation to create a gentle introduction to type classes in a course/tutorial: one of the first lessons/chapters could state that the type of '(+)' is 'Num -> Num -> Num', where 'Num' means "some numeric type" (stressing that it is *the same* type in all three places), only later confessing that this is actually shorthand for something more elaborate, and that the vague notion of "some numeric type" can be made explicit using type classes. Greetings, Arie -- Mr. Pelican Shit may be Willy. ^ /e\ ---
Arie said: {... This is an instance of a general conflict: should we sacrifice nice notation for ease of learning? You could make a similar case for list comprehensions, for example: they complicate matters for newcomers (yet another meaning of brackets and pipe) ...}
I have to totally agree with that statement, and surely hopeful that no one takes away the list comprehensions, as a person new to Haskell that was something that I got the hang of right away. I've used other languages for YEARS before I needed or used a given construct, and the fact that it was there never bothered me much.. I JUST DIDN'T use it. Now as to the whole namespace part of the argument made by Brian... well that is another kettle of fish, and I will leave that to guys with his knowledge.. to cipher out such things... somebody has been doing a good job on this language so far! happy day to all, gene
Hello Arie, Tuesday, August 22, 2006, 7:24:34 PM, you wrote:
I disagree. As a new learner to Haskell, I already have a hard time keeping Constructors, Types, and Classes straight. I know what they all are and what they all do, but sometimes I really have to think hard to remember which is which in a piece of code. What helps my understanding is that each has a specific place in the type signature (which I guess includes 'nowhere' regarding constructors). Being able to put Classes where Types go would just serve to muddle that understanding.
(*) In this specific instance one might (ab?)use the additional notation to create a gentle introduction to type classes in a course/tutorial: one of the first lessons/chapters could state that the type of '(+)' is 'Num ->> Num -> Num', where 'Num' means "some numeric type" (stressing that it is *the same* type in all three places), only later confessing that this is actually shorthand for something more elaborate, and that the vague notion of "some numeric type" can be made explicit using type classes.
to be exact, it is intended usage - like in the OOP model, Num or [] can specify not only concrete type - it's something that can have subtypes. so, meaning of (+) :: Num -> Num -> Num or sequence :: [Monad a] -> Monad [a] or hTell :: SeekableStream -> IO Integral is simple and straightforward. And it's the _advanced_ material that identifiers used here may be not only defined by type declarations, but also by class declarations, and moreover - some of already studied type names denote classes actually. Subtyping introduced in very natural (at least for OOP souls) way. We may, for example, have functions: doit :: MemBuf -> IO Int hRequestBuf :: MemoryStream -> IO Int hTell :: SeekableStream -> IO Integral and call doit -> hRequestBuf -> hTell and then return result, and all will work fine because MemBuf is subclass of MemoryStream that is subclass of SeekableStream while Int is subclass of Integral. We can describe whole type hierarchy as having types at leafs and type classes at internal nodes As an example that clears my idea the following is function signatures from one my module: copyStream :: (BlockStream h1, BlockStream h2, Integral size) => h1 -> h2 -> size -> IO () copyToMemoryStream :: (BlockStream file, MemoryStream mem, Integral size) => file -> mem -> size -> IO () copyFromMemoryStream :: (MemoryStream mem, BlockStream file, Integral size) => mem -> file -> size -> IO () saveToFile :: (MemoryStream h) => h -> FilePath -> IO () readFromFile :: FilePath -> IO MemBuf As one can see, there is only one function that don't uses classes, and another one that can't be written using this syntax, another 3 is just created for using this proposal. I don't say that such ratio is typical, but at least i have a large number of polymorphic functions in my library and found the way to simplify most of their signatures: copyStream :: BlockStream* -> BlockStream** -> Integral -> IO () copyToMemoryStream :: BlockStream -> MemoryStream -> Integral -> IO () copyFromMemoryStream :: MemoryStream -> BlockStream -> Integral -> IO () saveToFile :: MemoryStream -> FilePath -> IO () readFromFile :: FilePath -> IO MemBuf i think that second block of signatures is an order of magnitude more readable -- Best regards, Bulat mailto:Bulat.Ziganshin@gmail.com
Bulat Ziganshin wrote:
from one my module:
copyStream :: (BlockStream h1, BlockStream h2, Integral size) => h1 -> h2 -> size -> IO ()
in my library and found the way to simplify most of their signatures:
copyStream :: BlockStream* -> BlockStream** -> Integral -> IO ()
i think that second block of signatures is an order of magnitude more readable
I think template haskell could do this translation. Eg if you declared some dummy phantom types so the arg to the template function could be parsed, and as a way of telling the function which types were to be replaced by type variables with class constraints the block of signatures would just be declared in a splice: $(expandSigs [d| data BlockStream' data BlockStream'' data Integral' copyStream :: BlockStream' -> BlockStream'' -> Integral' -> IO () ... |]) Though I leave the definition of expandSigs :: Q [Dec] -> Q () as a little exercise for the reader... :-) Best regards, Brian. -- Logic empowers us and Love gives us purpose. Yet still phantoms restless for eras long past, congealed in the present in unthought forms, strive mightily unseen to destroy us. http://www.metamilk.com
Bulat Ziganshin wrote:
Subtyping introduced in very natural (at least for OOP souls) way. We may, for example, have functions:
doit :: MemBuf -> IO Int hRequestBuf :: MemoryStream -> IO Int hTell :: SeekableStream -> IO Integral
and call doit -> hRequestBuf -> hTell and then return result, and all will work fine because MemBuf is subclass of MemoryStream that is subclass of SeekableStream while Int is subclass of Integral. We can describe whole type hierarchy as having types at leafs and type classes at internal nodes
As an example that clears my idea the following is function signatures from one my module:
copyStream :: (BlockStream h1, BlockStream h2, Integral size) => h1 -> h2 -> size -> IO () copyToMemoryStream :: (BlockStream file, MemoryStream mem, Integral size) => file -> mem -> size -> IO () copyFromMemoryStream :: (MemoryStream mem, BlockStream file, Integral size) => mem -> file -> size -> IO () saveToFile :: (MemoryStream h) => h -> FilePath -> IO () readFromFile :: FilePath -> IO MemBuf
As one can see, there is only one function that don't uses classes, and another one that can't be written using this syntax, another 3 is just created for using this proposal. I don't say that such ratio is typical, but at least i have a large number of polymorphic functions in my library and found the way to simplify most of their signatures:
copyStream :: BlockStream* -> BlockStream** -> Integral -> IO () copyToMemoryStream :: BlockStream -> MemoryStream -> Integral -> IO () copyFromMemoryStream :: MemoryStream -> BlockStream -> Integral -> IO () saveToFile :: MemoryStream -> FilePath -> IO () readFromFile :: FilePath -> IO MemBuf
i think that second block of signatures is an order of magnitude more readable
These sorts of signatures seem to be the only ones where some way of using a class as a type would be useful - when single parameter type classes constrain variables which only occur once, and the variables are only constrained by a single class. This could be handled with existential wrappers, except that the wrapping is annoying, and probably interferes with optimizing when a concrete type is known. Instead, a few changes to type synonyms handle Bulat's cases. With the proper interpretation, type synonyms like type ABlockStream = BlockStream b => b type AMemoryStream = MemoryStream m => m support some of Bulat's signatures like copyStream :: ABlockStream -> ABlockStream -> Integer -> IO () saveToFile :: AMemoryStream -> FilePath -> IO () This requires two changes to the interpretation of type synonyms 1) Free variables in the definition of the type synonym are allowed, and become fresh (wobbly) variables when the synonym is applied 2) Class constraints in the definition of a type synonym float up to the closest binding of a constrained type. Now, more discussion, examples, and comparisons to the Haskell 98 standard type synonyms and the GHC (6.4.1) implementation. 1) Free variables expand to (wobbly) fresh variables. That is, each time a type synonym with a free variable is used, all the free variables are given fresh names, and then allowed to unify with other types during type checking. This allows the synonyms above to introduce a new type variable, which can carry the class constraint. for example, with type AnAuto = a -> a these definitions are legal op1 :: AnAuto op1 = id op2 :: AnAuto -> AnAuto -> (Int, Bool) op2 f g = (f 1, g True) op3 :: AnAuto -> AnAuto -> AnAuto op3 f g = g . f and result in types op1 :: forall x . x -> x op2 :: (Int->Int) -> (Bool->Bool) -> (Int, Bool) op3 :: forall y . (y -> y) -> (y -> y) -> (y -> y) Implicitly freshening free variables in type synonyms seems very much in the spirit of implicitly quantifying variables in type signatures, and the treatment of names in hygienic macros (the GHC user's guide says " Type synonyms are like macros at the type level"). Standards: Free variables are not allowed by Haskell 98, or GHC. Perhaps there is an explicit quantifier corresponding to this behavior, but I don't see how to make it properly a part of the type system, rather than just something that happens around synonym expansion. What might be meant by something like [fresh a . a -> a]? 2) A class constraint in a type synonym floats up to the nearest binding occurrence of any of the constrained types. This allows the type synonyms above to put a class constraint on the new variable they introduce (which is bound at the top level by the implicit forall). This extension would also allow parameterized type synonyms to add constraints to their arguments. (this would need some changes to error messages, like "cannot satisfy class constraint XX arising from application of type synonym Showable at nn:xx-yy) Type synonyms that add extra constraints to their argument can provide the syntax I suggested earlier to Bulat, where each use of a class-as-type is tagged with a variable, to indicate sharing. type TagMonad a = Monad a => a type TagFunctor a = Functor a => a sequence :: [TagMonad m a] -> TagMonad m [a] sequenceLift :: [TagMonad m a] -> TagMonad r [a] confuse :: (a -> b) -> (TagMonad m) [a] -> (TagFunctor m) b This nearly subsumes Brian Hulley's proposal to allow a list of curried class contexts in braces in front of types, completely if you don't mind declaring a new synonym for each set. Standards: GHC 6.4.1 requires that a class constraint mention some variable bound by a forall in the synonym, Haskell 98 doesn't allow quantifiers in synonyms at all. Brandon
Hello Brandon,
This could be handled with existential wrappers, except that the wrapping is annoying, and probably interferes with optimizing when a concrete type is known. Instead, a few changes to type synonyms handle Bulat's cases.
With the proper interpretation, type synonyms like type ABlockStream = BlockStream b => b type AMemoryStream = MemoryStream m => m
support some of Bulat's signatures like copyStream :: ABlockStream -> ABlockStream -> Integer -> IO () saveToFile :: AMemoryStream -> FilePath -> IO ()
This requires two changes to the interpretation of type synonyms
1) Free variables in the definition of the type synonym are allowed, and become fresh (wobbly) variables when the synonym is applied
2) Class constraints in the definition of a type synonym float up to the closest binding of a constrained type.
I find those free variables a bit scary. It is not clear to me what it means for a value to have type 'AnAuto'. I like to think about type synonyms as only that, synonyms - so you can always substitute the definition for an occurrence. How does your proposal compare to introducing existential types proper? As in type ABlockStream = exists b. BlockStream b => b . This is a known extension, supported partly by jhc and fully by ehc. It seems to be exactly what you need for
copyStream :: ABlockStream -> ABlockStream -> Integer -> IO ()
Greetings, Arie -- Mr. Pelican Shit may be Willy. ^ /e\ ---
Arie Peterson wrote:
Hello Brandon,
This could be handled with existential wrappers, except that the wrapping is annoying, and probably interferes with optimizing when a concrete type is known. Instead, a few changes to type synonyms handle Bulat's cases.
With the proper interpretation, type synonyms like type ABlockStream = BlockStream b => b type AMemoryStream = MemoryStream m => m
support some of Bulat's signatures like copyStream :: ABlockStream -> ABlockStream -> Integer -> IO () saveToFile :: AMemoryStream -> FilePath -> IO ()
This requires two changes to the interpretation of type synonyms
1) Free variables in the definition of the type synonym are allowed, and become fresh (wobbly) variables when the synonym is applied
2) Class constraints in the definition of a type synonym float up to the closest binding of a constrained type.
I find those free variables a bit scary. It is not clear to me what it means for a value to have type 'AnAuto'. I like to think about type synonyms as only that, synonyms - so you can always substitute the definition for an occurrence.
Those free variables are just necessary to match the proposed syntax exactly. The type variables could be provided as parameters - type AMemoryStream m = MemoryStream m => m writeToFile :: AMemoryStream m -> FilePath -> IO () type Stream s = Stream s => s copyStream :: Stream s1 -> Stream s2 -> Integer -> IO () That said, making fresh unification variables seems like a reasonable interpretation of free variables in a type synonym, the converse of the renaming you can see in type Cont x = forall r . (x -> r) -> r where the forall doesn't capture the x, even if you use the synonym in return :: r -> Cont r
How does your proposal compare to introducing existential types proper? As in
type ABlockStream = exists b. BlockStream b => b
. This is a known extension, supported partly by jhc and fully by ehc. It seems to be exactly what you need for
copyStream :: ABlockStream -> ABlockStream -> Integer -> IO ()
I don't understand the difference very well. I'm proposing to allow a bit of type inference to further resolve these variables when the type synonym is expanded. A function taking an existential type must work for any type in that existential package. A fresh variable could resolve a bit more, if it turns out that those two BlockStream types must be the same, or the parameter actually has to be a function type. I think mostly it's like a kind of partial type signature, but I'm wondering if there's an interpretation as a logical quantifier. Brandon
Hello Arie, Wednesday, August 23, 2006, 2:54:54 AM, you wrote:
With the proper interpretation, type synonyms like type ABlockStream = BlockStream b => b type AMemoryStream = MemoryStream m => m
How does your proposal compare to introducing existential types proper? As in
type ABlockStream = exists b. BlockStream b => b
existential variables pack dictionary inside the data item (object) itself, like in the OOP languages. so this the _semantic_ change. Brandon's idea is just _syntax_ sugar, one of the possible ways to simplify writing of signatures for regular Haskell polymorphic functions, what pass dictionaries apart of objects read the http://haskell.org/haskellwiki/OOP_vs_type_classes and look for "existential" there -- Best regards, Bulat mailto:Bulat.Ziganshin@gmail.com
Bulat Ziganshin wrote:
f :: Num a => a -> Int write as f :: Num -> Int
so, while this proposal is rather minor, i think that it is Good thing
I wouldn't like it because I'd like to eventually make the class namespace separate from the tycon namespace so that I could write: class Object a where ... data Object = forall a. Object a => Object a etc (this goes with H' proposal that the namespace should always be explicit on the module export/import list [1]). A good editor (hint: the one I'm writing!!!) will be able to highlight the uses of "Object" to make it clear which is a class, which is a Tycon, and which is a ValueCon, and the operation of replacing a concrete type with a class in the type signature to generalise some functions could be made easier with a good refactoring tool. Best regards, Brian. [1] http://hackage.haskell.org/trac/haskell-prime/wiki/TagExportsWithNamespace -- Logic empowers us and Love gives us purpose. Yet still phantoms restless for eras long past, congealed in the present in unthought forms, strive mightily unseen to destroy us. http://www.metamilk.com
Brian Hulley wrote:
Bulat Ziganshin wrote:
f :: Num a => a -> Int write as f :: Num -> Int
Actually separating the class namespace from the tycon namespace would allow you to get a very similar effect to the use of abstract interfaces in C++ ie: class Object a where name :: a -> Unique -- generated automatically? data Object = forall a. Object a -- general version foo :: Object a => a -> Unique -- to use with the standard Object wrapper foo :: Object -> Unique Regards, Brian. -- Logic empowers us and Love gives us purpose. Yet still phantoms restless for eras long past, congealed in the present in unthought forms, strive mightily unseen to destroy us. http://www.metamilk.com
Brian Hulley wrote:
Bulat Ziganshin wrote:
f :: Num a => a -> Int write as f :: Num -> Int
so, while this proposal is rather minor, i think that it is Good thing
I wouldn't like it because I'd like to eventually make the class namespace separate from the tycon namespace...
Apologies for that phrasing. I should have said: "I'd like to eventually find myself living in some mode of existence wherein ClassCons and TyCons no longer share the same namespace." Also apologies for these multiple posts... ;-) Brian.
Hello Brian and others,
On 2006-08-22, Brian Hulley
I wouldn't like it because I'd like to eventually make the class namespace separate from the tycon namespace so that I could write:
class Object a where ...
data Object = forall a. Object a => Object a
I like the idea of separating class and type constructor namespaces, and then being able to use existentials as in your example (although the latter would also belong in the category "not nice to beginners struggling with discriminating type constructors, data constructors and classes"). On the other hand, I find Bulat's proposal also very attractive, especially when considering the important example of the list type. The question is essentially: what do we want to express when writing things like: f :: Object -> Object g :: Object -> Object -> Ordering h :: Object -> Object -> Object i :: Int -> Object ? Is the argument of 'f' an 'Object' of the same concrete type as the result (Bulat's proposal)? Or do we only demand that they are both an object, possibly implemented in different ways (using sloppy OO language)? Putting it this way, I think I tend to prefer the latter. It is easier somehow if the meaning of "Object" does not depend on other parts of the type signature. Consider the following example: k :: Garage -> Car type Garage = Car -> Car Bulat's proposal (if suitably extended to apply to type synonyms as well) would not allow you to substitute the definition of 'Garage' (which would then be equivalent to 'type Garage = forall a. (Car a) => a -> a') in the type signature of 'k' (because then the 'Car' of the 'Garage' definition would suddenly be unified with the result type of 'k'). Greetings, Arie -- Mr. Pelican Shit may be Willy. ^ /e\ ---
Hello Arie, Tuesday, August 22, 2006, 8:24:17 PM, you wrote:
data Object = forall a. Object a => Object a
I like the idea of separating class and type constructor namespaces, and then being able to use existentials as in your example (although the latter would also belong in the category "not nice to beginners struggling with discriminating type constructors, data constructors and classes").
On the other hand, I find Bulat's proposal also very attractive, especially when considering the important example of the list type.
The question is essentially: what do we want to express when writing things like:
f :: Object -> Object g :: Object -> Object -> Ordering h :: Object -> Object -> Object i :: Int -> Object
? Is the argument of 'f' an 'Object' of the same concrete type as the result (Bulat's proposal)? Or do we only demand that they are both an object, possibly implemented in different ways (using sloppy OO language)?
my proposal is modeled after real situations. i found than in most cases when some class is used two times or more in function signature, it should be the same type. existential types, suggested by Brian, rather rarely used in Haskell. may be it's just because there is no good syntax, but i think than in most cases polymorphic types are just enough
k :: Garage -> Car
type Garage = Car -> Car
Bulat's proposal (if suitably extended to apply to type synonyms as well) would not allow you to substitute the definition of 'Garage' (which would then be equivalent to 'type Garage = forall a. (Car a) => a -> a') in the type signature of 'k' (because then the 'Car' of the 'Garage' definition would suddenly be unified with the result type of 'k').
you are right here -- Best regards, Bulat mailto:Bulat.Ziganshin@gmail.com
Bulat Ziganshin wrote:
Hello Malcolm,
Tuesday, August 22, 2006, 4:22:50 PM, you wrote:
2) allow to use type classes in type declarations like the types itself. for example, allow the following:
f :: Num a => a -> Int write as f :: Num -> Int
and following:
sequence :: Monad m => [m a] -> m [a] write as sequence :: [Monad a] -> Monad [a]
I dislike the way mentioning a class implicitly introduces a new type variable. To make the dependency explicit you might make the type that is supposed to get the constraint a parameter to the class name, like
sequence :: [Monad m a] -> Monad m [a]
e class contexts of (for instance) sequenceLift :: (Monad m, Monad r) => [m a] -> r [a] if it were to be written instead as simply sequenceLift :: [Monad a] -> Monad [a]
This type could be written like [Monad m a] -> Monad r [a]
I think this syntax could be done with associated types, if class Monad declared an associated type synonym Monad m, and somehow all instances were known to define the synonym equal to the type getting the instance. Knowing the type Monad m = m only matters if you want to be able to use m and Monad m interchangeably.
And how would one add multiple class constraints to a single type variable, for instance in: f :: (Functor m, Monad m) => (a->b) -> m [a] -> m b
I think it would just be confusing trying to inline constraints, but with the associated type interpretation it seems each "constrained occurrence" of a type would add another class constraint to the type, so maybe you could write (a -> b) -> Monad m [a] -> Functor m b. both your examples cannot be written using proposed syntax
what i propose is not full replacement of existing syntax - quite the contrary it is just a syntax sugar for most frequent cases of using classes in function signatures. the key idea is that in most cases we use only one type class for each type variable, and the same type for each occurrence of type class in the type:
(+) :: Num -> Num -> Num
I don't like how this repeats the class name. Repetition of the name a in Num a => a -> a -> a is completely different, because the name 'a' is just a placeholder for expressing some local sharing in the type. This reminds me vaguely of the syntax proposed in Daan's paper on MLF, where some constraints about polymorphism could be inlined, as in (x == forall a . a -> a) => [x]->String --> [forall a . a -> a] -> String Maybe there's some similarly useful shorthand here?
This also simplifies the case when programmer has developed his code with one concrete type in mind and later decided to transform it into typeclass. In this case my idea allows to retain old definitions in most cases (and promoting [] to type class is very typical example here! we can browse prelude/list module and count how many definitions need to be changed if [] becomes type class)
This really isn't much easier than changing things to use type classes. Instead of replacing the concrete type with the name of a class, you could replace the concrete type with a variable (maybe just change the case of the first letter) and add a constraint. Any editor smarter than ed should be able to automate either operation. (even sed, and pretty trivially if you don't handle multi-line type signatures)
This proposal born from my experience of using type classes to make Streams library more flexible. i found that type signatures using type classes becomes larger and less readable and thought that they can be made no more complex than ordinary ones by using this idea. Java/C++ also allows to specify names of abstract classes/interfaces instead of concrete classes. Haskell's benefit is that general syntax allows to express more complex restrictions. I propose to combine it with the OOP-like simple syntax for simple cases (which is 80-90% of total ones)
so, while this proposal is rather minor, i think that it is Good thing In general, the proposal reminds me a bit of the shorthand proposed in Daan Leijen's paper on MLF, available at http://www.cs.uu.nl/~daan/pubs.html#qmlf
It's a nice type system, but for this message all that matters is that MLF handles polymorphism using constraints like (x = forall a . a -> a) or (y >= forall a . a -> a), which appear in a type at the same place as class constraints. His shorthand is to allow the right side of a constraint to be embedded directly into a type, without naming it at all, if there is only a single occurrence, and the type is left of an arrow for an = constraint, or right for a >= constraint, e.g. (x = forall a . a -> a, y >= forall a . a -> a) => [x] -> [y] ---> [forall a . a -> a] -> [forall a . a -> a] (yes, MLF handles impredicative types quite nicely. Daan's paper shows how to add type classes to MLF, making it easy to work with types like [forall a . (Show a) => a], and if I read correctly even to infer the types in x1 = [] :: forall a . [a] x2 = const : x1 :: [forall a b. a -> b -> a] x3 = min : x2 :: [forall a . (Ord a) -> a -> a -> a] x4 = (<) : x3 :: [Bool -> Bool -> Bool] Just the MLF heritage is enough to let you use ($) at type ((forall s . ST s a) -> a) -> (forall s . ST s a) -> a, eg runST $ return 3 --yay! ) There are several reasons to think this sort of shorthand would be more useful for MLF types than class constraints, but it does seem to be quite handy with MLF. Perhaps there is something similar that could be done with type classes. In particular, I very much like Daan's rule of only inlining a constraint if the type it binds is only used once, which would mean Num -> Num -> Num would be equivalent to (Num a, Num b, Num c) => a -> b -> c For an alternate proposal, how about allowing a single-parameter type class as an annotation around a subexpression of a type expression, meaning the same as a constraint that that subexpression belong to that class. For example, (+) :: Num a -> a -> a, or sort :: [Ord a] -> [a] this is a bit closer to how I would read the types, "sort takes a list of comparable a to a list of a" Brandon
Brandon Moore wrote:
Perhaps there is something similar that could be done with type classes. In particular, I very much like Daan's rule of only inlining a constraint if the type it binds is only used once, which would mean
Num -> Num -> Num
would be equivalent to
(Num a, Num b, Num c) => a -> b -> c
A problem here is that you need to know that Num is a class and not a tycon before you can work out what the above syntax means. For an editor, suppose you open a new file and enter: module M import Q foo :: Z -> Z how is the editor supposed to fontify Z if module Q has not yet been written? With the existing syntax, just the grammar alone is enough to determine that Z is a tycon.
For an alternate proposal, how about allowing a single-parameter type class as an annotation around a subexpression of a type expression, meaning the same as a constraint that that subexpression belong to that class. For example,
(+) :: Num a -> a -> a, or sort :: [Ord a] -> [a]
this is a bit closer to how I would read the types, "sort takes a list of comparable a to a list of a"
To me this looks as if you mean (assuming Ord is known to be a class): sort :: forall a. [ forall a. Ord a=>a] -> [a] because the Ord is hidden inside the list brackets. In contrast: sort :: forall a. Ord a => [a] -> [a] makes it very clear that the Ord constraint scopes over both occurrences of 'a'. I feel "if it ain't broken don't fix it", and not only is the existing syntax not broken, it's already (imho) absolutely perfect in it's clarity and consistency ie adding all these dubious "shortcuts" to the Haskell type syntax would be about as sensible as deliberately chopping one's legs off to walk quicker!!! ;-) Brian. -- Logic empowers us and Love gives us purpose. Yet still phantoms restless for eras long past, congealed in the present in unthought forms, strive mightily unseen to destroy us. http://www.metamilk.com
Hello Brian, Tuesday, August 22, 2006, 9:35:21 PM, you wrote:
I feel "if it ain't broken don't fix it", and not only is the existing syntax not broken, it's already (imho) absolutely perfect in it's clarity and consistency
it's because you not programmed a lot with type classes. if you start, you will soon realize that type signatures with classes are just unreadable. just look at sources of my streams library -- Best regards, Bulat mailto:Bulat.Ziganshin@gmail.com
Bulat Ziganshin wrote:
Hello Brian,
Tuesday, August 22, 2006, 9:35:21 PM, you wrote:
I feel "if it ain't broken don't fix it", and not only is the existing syntax not broken, it's already (imho) absolutely perfect in it's clarity and consistency
it's because you not programmed a lot with type classes. if you start, you will soon realize that type signatures with classes are just unreadable. just look at sources of my streams library
copyStream :: (BlockStream h1, BlockStream h2, Integral size) => h1 -> h2 -> size -> IO () Here is another possible syntax, which wouldn't conflict with the existing syntax but could be used as a sugar: copyStream :: {BlockStream} h1 -> {BlockStream} h2 -> {Integral} size -> IO () The type variables could be optional if they are distinct (or not needed in the body) so you could write: copyStream :: {BlockStream} -> {BlockStream} -> {Integral} -> IO () The {} is needed to distinguish the use of classes from that of types, and also allows more than one constraint eg: foo :: (Num a, Bar a) => a -> a === foo :: {Num, Bar} a -> a (the constraint(s) just get written before the first occurrence of a given type variable), and it's even possible to represent constraints between type variables eg: foo :: Collection c a => a -> c === foo :: {Collection c} a -> c It's slightly more difficult to know how to represent the following: foo :: Collection c a => c -> c perhaps: foo :: {Collection * a} c -> c where the * represents the location of the variable in the constraint. Even a rank 2 type like: forall a. Num a => (forall b. (Coll b a, Ord b) => b a -> ()) -> () (forall b. {Coll * a, Ord}b {Num}a -> ()) -> () ie forall a. (forall b. ({Coll * a, Ord} b) ({Num} a) -> ()) -> () (It doesn't matter how nested the location of the constraints are since we'd just gather them up and use them to restrict the quantification for that variable) Anyway that's as far as I've got trying to think up alternative representations - the above may have some bug or problem with it but I'm half thinking of adding the above sugar to my editor (when I eventally get past all the low-level gui stuff I'm doing at the moment). Best regards, Brian. -- Logic empowers us and Love gives us purpose. Yet still phantoms restless for eras long past, congealed in the present in unthought forms, strive mightily unseen to destroy us. http://www.metamilk.com
it's because you not programmed a lot with type classes. if you start, you will soon realize that type signatures with classes are just unreadable. just look at sources of my streams library
copyStream :: (BlockStream h1, BlockStream h2, Integral size) => h1 -> h2 -> size -> IO ()
I know this is probably just a personal preference, but I have to say that this syntax (the canonical Haskell'98 one) is by far the most readable and instantly clear of any of the alternatives that have been suggested in this thread: copyStream :: BlockStream* -> BlockStream** -> Integral -> IO () Here you have invented a new notation for type variables (* and **), when we already have a perfectly good one. copyToMemoryStream :: BlockStream -> MemoryStream -> Integral -> IO () Whereas here, the lack of any type variable means I am no longer aware that overloading is going on. This is likely to discourage the reuse of this code fragment, rather than encourage it. copyStream :: {BlockStream} h1 -> {BlockStream} h2 -> {Integral} size -> IO () What is gained by attaching the constraints inline with the type variables? If the type variable occurs more than once, which occurrence should I attach the constraint to? What if I attach different constraints to different occurrences of the same variable? (Obviously the union is intended, but writing constraints in several different locations would be highly confusing). But at least there is a syntactic marker ({}) that overloading is happening. copyStream :: {BlockStream} -> {BlockStream} -> {Integral} -> IO () Again, omitting type variables means that the possible mental confusion over whether the two {BlockStream} constraints apply to the same implicit variable or to different ones is unpleasant. Better to be fully explicit, after all, it only takes one extra character to name the variable!
foo :: Collection c a => a -> c === foo :: {Collection c} a -> c
foo :: Collection c a => c -> c === foo :: {Collection * a} c -> c
forall a. Num a => (forall b. (Coll b a, Ord b) => b a -> ()) -> () === (forall b. {Coll * a, Ord}b {Num}a -> ()) -> () === forall a. (forall b. ({Coll * a, Ord} b) ({Num} a) -> ()) -> ()
The lengths people will go to in making things difficult for the reader, just to save a few characters is truly amazing. Remember, the code will be read many more times than it is written. IMHO, the various proposed sugar adds nothing helpful, and just muddies understanding. Regards, Malcolm
On Wed, Aug 23, 2006 at 01:28:57PM +0100, Malcolm Wallace wrote:
The lengths people will go to in making things difficult for the reader, just to save a few characters is truly amazing. Remember, the code will be read many more times than it is written. IMHO, the various proposed sugar adds nothing helpful, and just muddies understanding.
Seconded. If someone just wants to type less characters, the he/she can omit most of type signatures. I haven't used any IDE for Haskell (like VisualHaskell), but it would be nice if it could fill the missing type signatures automatically. In cases when monomorphism restriction kicks in, it could also present the type that would be inferred with MR turned off. Best regards Tomasz
tomasz.zielonka:
On Wed, Aug 23, 2006 at 01:28:57PM +0100, Malcolm Wallace wrote:
The lengths people will go to in making things difficult for the reader, just to save a few characters is truly amazing. Remember, the code will be read many more times than it is written. IMHO, the various proposed sugar adds nothing helpful, and just muddies understanding.
Seconded. If someone just wants to type less characters, the he/she can omit most of type signatures.
I haven't used any IDE for Haskell (like VisualHaskell), but it would be nice if it could fill the missing type signatures automatically. In cases when monomorphism restriction kicks in, it could also present the type that would be inferred with MR turned off.
I use the following script from vim to infer top level type declarations for me. I've found it particularly useful for understanding others' code: #!/bin/sh # input is a top level .hs decls FILE=$* DECL=`cat` ID=`echo $DECL | sed 's/^\([^ ]*\).*/\1/'` echo ":t $ID" | ghci -v0 -cpp -fglasgow-exts -w $FILE echo $DECL Saved to 'typeOf', you can bind it from vim with: :map ty :.!typeOf %^M in your .vimrc So, from vim the following source: f (x,y,z) a b = y + a + b hit, 'ty' and its replaced with: f :: forall b c a. (Num b) => (a, b, c) -> b -> b -> b f (x,y,z) a b = y + a + b I imagine it would be possible to bind from emacs with little effort. -- Don
On Wed, Aug 23, 2006 at 11:11:59PM +1000, Donald Bruce Stewart wrote:
So, from vim the following source:
f (x,y,z) a b = y + a + b
hit, 'ty' and its replaced with:
f :: forall b c a. (Num b) => (a, b, c) -> b -> b -> b f (x,y,z) a b = y + a + b
Nice! Best regards Tomasz
On 8/23/06, Donald Bruce Stewart
I use the following script from vim to infer top level type declarations for me. I've found it particularly useful for understanding others' code:
<delurk> On the topic of coding Haskell with Vim is there an indentation plugin for Haskell available? Google hasn't found one for me and none is mentioned on the Haskell wiki. Thanks, Toby.
participants (12)
-
Arie Peterson -
Brandon Moore -
Brian Hulley -
Bryan Burgers -
Bulat Ziganshin -
dons＠cse.unsw.edu.au -
Duncan Coutts -
Gene A -
Malcolm Wallace -
Marc Weber -
Toby Hutton -
Tomasz Zielonka