Re: [Haskell-cafe] Type vs TypeClass duality
I'm relatively new to Haskell, so maybe this answer is a bit off, in that I'm sure there are times when some sort of auto-existential creation may have a point, but generally I've found that when I want it I've been thinking about the problem wrong. The bigger issue is that as soon as you get fancier types classes, they'll probably be paramaterized over more than one type, not to mention with possible functional dependencies, etc., and very likely be polymorphic over return value as well. in fact, I suspect, Show and maybe fromIntegral or such aside, cases like you describe where you might even have the possibility of doing what you're looking for (i.e., a list of a typeclass such that a function in it is guaranteed a single return type) look fairly rare. Integrals are a good example of what I ran into early on -- suppose you had a [Integral] rather than one of Integral a = [a]. What would be the advantage of this? It would actually make your code messier -- instead of a case of, e.g. [x:x':xs] - x+x' you wold need one of [x:x':xs] - fromIntegral x + fromIntegral x', otherwise you would have no guarantee the types would match! And even then, what would the return type of this function be? Polymorphic over Integral? You'd just be spreading the fuzziness over type to the rest of your program, and probably introducing a load of potential inefficiencies to boot. I suspect that you may still be trying to code with an OO mentality which thinks of the methods of a typeclass as within it as they are within an object, rather than as _on_ it. --s On Oct 23, 2007, at 4:09 AM, TJ wrote: Hi again, Following up on my previous thread, I have figured out why it bothered me that we cannot have a list such as the following: [abc, 123, (1, 2)] :: Show a = [a] It seems to me that there is an annoying duality in treating simple algebraic data type vs type classes. As it stands, I can only have a list where all the elements are of the same basic, ADT, type. There is no way to express directly a list where all the elements satisfy a given type class constraint. If I am not mistaken, type classes are currently implemented in GHC like so: Given a function show of type Show a = a - string, and the expression show 10, GHC will pass the Int dictionary for class Show's methods and the integer 10 to the function show. In other words, for each type class constraint in the function type, there will be a hidden dictionary parameter managed entirely by the compiler. What I find strange is, if we can have functions with hidden parameters, why can't we have the same for, say, elements of a list? Suppose that I have a list of type Show a = [a], I imagine that it would not be particularly difficult to have GHC insert a hidden item along with each value I cons onto the list, in effect making the concrete type of the list [(Dictionary Show, a)]. I'm assuming that it will not be particularly difficult because GHC will know the types of the values I cons onto it, so it will most definitely be able to find the Show dictionary implemented by that type, or report a type mismatch error. No dynamic type information is necessary. I am not an OO programming zealot, but I'd like to note here that this is also how (class based) OO languages would allow the programmer to mix types. e.g. I can have a ListShow where the elements can be instances of Show, or instances of subclasses of Show. Why does this second rate treatment of type classes exist in Haskell? TJ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type vs TypeClass duality
On Wed, Oct 24, 2007 at 11:00:14AM +0800, TJ wrote: Tristan Allwood: Very cool. I don't understand some (a lot of) parts though: instance Show a = Reify (ShowConstraint a) where reify = ShowC ShowC has type (Show a) = ShowConstraint a, whereas reify is supposed to have type ShowConstraint a. Yes. ShowC is a constant that wraps up the knowledge of (Show a =) for ShowConstraint. So (in this case) reify :: ShowConstraint a reify = ShowC (since ShowC is the only non-bottom value ShowConstraint can take) But in order to return ShowC, we must know that a 'is in' Show, which is why the instance declaration requires that at the point you use reify you can demonstrate that a is in Show: instance Show a = Reify (ShowConstraint a) where ^ If the Show a = bit is removed, then the type checker rightly complains, because the ShowC doesn't have a Show a context that it needs. So the trick is that in the cons (#) function which uses reify, you need to prove 'Reify (a b)', and it just so happens that by the instance declaration above, wherever you have 'Show a' then you have 'Reify (ShowConstraint a)' which is why testList needs nothing more than the values to put into it like a normal list. data SingleList (a :: * - *) where Cons :: (a b) - b - SingleList a - SingleList a Nil :: SingleList a Cons has a type variable b in its signature, but no forall. I suppose it comes from the * - * in SingleList's type? Nope. The (a :: * - *) is a kind annotation and means that the a is a type that is parameterised by a type (e.g. Maybe :: * - *, whereas Maybe Int :: *), which is why you can write (a b). I think technically it's a redundant annotation here as it can be inferred from the (a b) useage. The b is 'just' a normal, exisistentially quantified variable - GADTs don't require you to write forall in their declarations - see the very last sentence on http://www.haskell.org/ghc/docs/latest/html/users_guide/gadt.html That's all I can come up with for now. A great deal of high level coding flying around above my head now. Hope that helps some, Regards, Tris ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type vs TypeClass duality
On 10/23/07, Luke Palmer [EMAIL PROTECTED] wrote: On 10/23/07, TJ [EMAIL PROTECTED] wrote: What I find strange is, if we can have functions with hidden parameters, why can't we have the same for, say, elements of a list? Suppose that I have a list of type Show a = [a], I imagine that it would not be particularly difficult to have GHC insert a hidden item along with each value I cons onto the list, in effect making the concrete type of the list [(Dictionary Show, a)]. I'm assuming that it will not be particularly difficult because GHC will know the types of the values I cons onto it, so it will most definitely be able to find the Show dictionary implemented by that type, or report a type mismatch error. No dynamic type information is necessary. Which is exactly what happens with: data Showable = forall a. Show a = Showable a stuff = [Showable 42, Showable hello, Showable 'w'] Which is exactly the kind of 2nd-rate treatment I dislike. What does data Showable = forall a. Show a = Showable a do for you anyway? Nothing. You just have to type it down. Imagine if we have to type down our anonymous functions at the top level, and give them a name just to satisfy the language: ugh. I find this extra annoying due to not being able to declare datatypes anywhere other than at top-level. I am not an OO programming zealot, but I'd like to note here that this is also how (class based) OO languages would allow the programmer to mix types. e.g. I can have a ListShow where the elements can be instances of Show, or instances of subclasses of Show. Why does this second rate treatment of type classes exist in Haskell? I think partially the reason is that such polymorphic data structures are somewhat less useful in Haskell than they are in OO languages. This may be in part due to the fact that there's no down-casting. And certain wrappers, eg. Gtk, emulate up- and down-casting using various typeclass tricks. I was in a similar dilemma shortly after I started learning Haskell, coming from a C++ and Perl background. I think #perl6 has some logs of me whining about Haskell's lack of OO features. How are you supposed to design your programs modularly if you can't have a type-agnostic list? But it doesn't bug me anymore. I can't really say why. The natural solution space in Haskell is so different than that of OO languages, that you don't really need such existentially polymorphic (just made up that term) objects[1]. There is still plenty of modularity in Haskell programs--I would even call it OO, I think--it just looks different, and took a lot of getting used to. I had to remap what I considered an object in my brain. Anyway, enough preachy. Typeclasses definitely aren't perfect; global instance exportation has gotten me in trouble several times. But, other than [exists a. Show a = a] I actually don't understand that line. Substituting forall for exists, someone in my previous thread said that it means every element in the list is polymorphic, which I don't understand at all, since trying to cons anything onto the list in GHCi results in type errors. What would be a first-rate treatment of type classes to you? What kind of features do you want that they don't have? Convenience. Same thing 1st-class functions do for me ;-) TJ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type vs TypeClass duality
On 10/23/07, TJ [EMAIL PROTECTED] wrote: What I find strange is, if we can have functions with hidden parameters, why can't we have the same for, say, elements of a list? Suppose that I have a list of type Show a = [a], I imagine that it would not be particularly difficult to have GHC insert a hidden item along with each value I cons onto the list, in effect making the concrete type of the list [(Dictionary Show, a)]. I'm assuming that it will not be particularly difficult because GHC will know the types of the values I cons onto it, so it will most definitely be able to find the Show dictionary implemented by that type, or report a type mismatch error. No dynamic type information is necessary. Which is exactly what happens with: data Showable = forall a. Show a = Showable a stuff = [Showable 42, Showable hello, Showable 'w'] I am not an OO programming zealot, but I'd like to note here that this is also how (class based) OO languages would allow the programmer to mix types. e.g. I can have a ListShow where the elements can be instances of Show, or instances of subclasses of Show. Why does this second rate treatment of type classes exist in Haskell? I think partially the reason is that such polymorphic data structures are somewhat less useful in Haskell than they are in OO languages. This may be in part due to the fact that there's no down-casting. And certain wrappers, eg. Gtk, emulate up- and down-casting using various typeclass tricks. I was in a similar dilemma shortly after I started learning Haskell, coming from a C++ and Perl background. I think #perl6 has some logs of me whining about Haskell's lack of OO features. How are you supposed to design your programs modularly if you can't have a type-agnostic list? But it doesn't bug me anymore. I can't really say why. The natural solution space in Haskell is so different than that of OO languages, that you don't really need such existentially polymorphic (just made up that term) objects[1]. There is still plenty of modularity in Haskell programs--I would even call it OO, I think--it just looks different, and took a lot of getting used to. I had to remap what I considered an object in my brain. Anyway, enough preachy. Typeclasses definitely aren't perfect; global instance exportation has gotten me in trouble several times. But, other than [exists a. Show a = a] What would be a first-rate treatment of type classes to you? What kind of features do you want that they don't have? [1] I hardly ever use them. When I do use existential types, they are usually without context, i.e. they fill the role of 'something which I know nothing about'. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type vs TypeClass duality
Short answer: You are worrying about syntax. The things you want are possible. TJ wrote: Following up on my previous thread, I have figured out why it bothered me that we cannot have a list such as the following: [abc, 123, (1, 2)] :: Show a = [a] That type doesn't mean what you want it to mean. That means : A list of objects of some fixed type 'a', such that a is a member of the typeclass 'Show'. In fact, worse than that, it's a polymorphic list, which means the *caller* should be able to choose the type 'a'. What you want to mean is 'A list of objects, each of which is of some possibly different type 'a', subject only to the restriction that a is a member of typeclass Show. It seems to me that there is an annoying duality in treating simple algebraic data type vs type classes. As it stands, I can only have a list where all the elements are of the same basic, ADT, type. There is no way to express directly a list where all the elements satisfy a given type class constraint. There is, it's just not as simple as you want it to be. You need a constructor for the existential, as shown in the recent Renderable thread. Incidentally there is no restriction that all the elements in a list have to be an ADT. They can be functions, or tuples of functions, or higher order functions, or lists of tuples of higher order polymorphic functions operating on lists of functions on tuples of. In GHC they can even be higher-rank. If I am not mistaken, type classes are currently implemented in GHC like so: [You are pretty much right, but of course how type classes are *implemented* isn't relevant, except as intuition. Any proposed extension should be based on what they mean (their semantics) not how GHC does it] Suppose that I have a list of type Show a = [a], I imagine that it would not be particularly difficult to have GHC insert a hidden item along with each value I cons onto the list, in effect making the concrete type of the list [(Dictionary Show, a)]. Right. That's almost exactly what the Showable existential does. I'm assuming that it will not be particularly difficult because GHC will know the types of the values I cons onto it, so it will most definitely be able to find the Show dictionary implemented by that type, or report a type mismatch error. No dynamic type information is necessary. Now it sounds like your only complaint is that : has the wrong type? You could have a special case of (:) with type (:) :: Show a = a - [Showable] - [Showable] and then you could write: 123 : 34 : foo : [1,2,3] : (1,2,3) : [] I am not an OO programming zealot, but I'd like to note here that this is also how (class based) OO languages would allow the programmer to mix types. e.g. I can have a ListShow where the elements can be instances of Show, or instances of subclasses of Show. Why does this second rate treatment of type classes exist in Haskell? I don't think it is second rate :) Type classes are a different thing from types, of course they are treated differently... Or maybe, if you're asking a slightly different question: Why is there always some syntactic hint, like an explicit constructor or a carefully typed combinator, when existentials come into play? then the answer is because of type inference. That is, the type inference algorithm which GHC uses, which is not the only one you can imagine, but for a variety of reasons is considered to be one of the best choices, cannot 'automatically' construct existentials, and requires some kinds of explicit annotations to 'delimit' the existential. I will also repeat the non-justified assertion that others have made, and that I've made myself in the other thread, that you don't need existentials as often in haskell as you do in OO languages, and they certainly don't always need to be type-class quantified ones. Jules ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type vs TypeClass duality
On 10/23/07, Jules Bean [EMAIL PROTECTED] wrote: Short answer: You are worrying about syntax. The things you want are possible. TJ wrote: Following up on my previous thread, I have figured out why it bothered me that we cannot have a list such as the following: [abc, 123, (1, 2)] :: Show a = [a] That type doesn't mean what you want it to mean. That means : A list of objects of some fixed type 'a', such that a is a member of the typeclass 'Show'. In fact, worse than that, it's a polymorphic list, which means the *caller* should be able to choose the type 'a'. What you want to mean is 'A list of objects, each of which is of some possibly different type 'a', subject only to the restriction that a is a member of typeclass Show. Yes, of course. But given that what I want isn't directly expressible in Haskell, without creating an existential type, I would not have been able to give a valid Haskell type signature anyway ;-) Incidentally there is no restriction that all the elements in a list have to be an ADT. They can be functions, or tuples of functions, or higher order functions, or lists of tuples of higher order polymorphic functions operating on lists of functions on tuples of. Yes. My mistake. Suppose that I have a list of type Show a = [a], I imagine that it would not be particularly difficult to have GHC insert a hidden item along with each value I cons onto the list, in effect making the concrete type of the list [(Dictionary Show, a)]. Right. That's almost exactly what the Showable existential does. I'm assuming that it will not be particularly difficult because GHC will know the types of the values I cons onto it, so it will most definitely be able to find the Show dictionary implemented by that type, or report a type mismatch error. No dynamic type information is necessary. Now it sounds like your only complaint is that : has the wrong type? No. I am saying that Haskell's type system forces me to write boilerplate. That is, the type inference algorithm which GHC uses, which is not the only one you can imagine, but for a variety of reasons is considered to be one of the best choices, cannot 'automatically' construct existentials, and requires some kinds of explicit annotations to 'delimit' the existential. Why can't it automatically construct them then? Assuming we do have a syntax for A list of objects, each of which is of some possibly different type 'a', subject only to the restriction that a is a member of typeclass Show, as the following: ls :: [a where Show a] Then I would think that all the type checker has to do would be to check that, a) everything you cons onto ls is an instance of class Show b) where you extract items from ls, you only use them as you would use any instance of class Show. Which is exactly the same as for a list intList of type [Int], where a) everything you cons onto it is of type Int b) where you extract items from intList, you use them only as it is valid to use an Int (+,-,*,/,etc) Now assuming the existential type data E = forall a. Show a = E a EList :: [E] What I have done is to wrap up the idea that E contains any instance of Show, and that EList contains any E. Which is a roundabout way of saying what I wanted to say: ls contains any instance of Show. It seems Haskell's type inference has not kept up with advancements in existential types. I will also repeat the non-justified assertion that others have made, and that I've made myself in the other thread, that you don't need existentials as often in haskell as you do in OO languages, and they certainly don't always need to be type-class quantified ones. And I would like to say that whether or not I need it is not the issue, as I currently do not in fact need it. This is a study of the Haskell language not my possible practical applications of it. TJ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Uniqueness of principle type? (was Re: [Haskell-cafe] Type vs TypeClass duality)
TJ wrote: No. I am saying that Haskell's type system forces me to write boilerplate. Fair enough. Why can't it automatically construct them then? Assuming we do have a syntax for A list of objects, each of which is of some possibly different type 'a', subject only to the restriction that a is a member of typeclass Show, as the following: ls :: [a where Show a] Then I would think that all the type checker has to do would be to check that, a) everything you cons onto ls is an instance of class Show b) where you extract items from ls, you only use them as you would use any instance of class Show. This is beyond the detail of my understanding of the type inference algorithm. I believe it is to do with the requirement that expressions have a unique principle type. Certainly in principle the algorithm you outline is possible, but I don't know what else you would lose. And I would like to say that whether or not I need it is not the issue, as I currently do not in fact need it. This is a study of the Haskell language not my possible practical applications of it. Whether one needs it, or does not need it, is indeed an issue: any change to the type inference algorithm has a cost. That cost has to be judged against the value of it. If an extension is seldom needed, then its value is low, so the cost is unlikely to be considered worth it. If an extension is frequently need and the cost is low, then that argues for it.. Jules ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Uniqueness of principle type? (was Re: [Haskell-cafe] Type vs TypeClass duality)
On 10/23/07, Jules Bean [EMAIL PROTECTED] wrote: I believe it is to do with the requirement that expressions have a unique principle type. Certainly in principle the algorithm you outline is possible, but I don't know what else you would lose. I'm not familiar with the term principal type. I shall have to study it. And I would like to say that whether or not I need it is not the issue, as I currently do not in fact need it. This is a study of the Haskell language not my possible practical applications of it. Whether one needs it, or does not need it, is indeed an issue: any change to the type inference algorithm has a cost. That cost has to be judged against the value of it. If an extension is seldom needed, then its value is low, so the cost is unlikely to be considered worth it. If an extension is frequently need and the cost is low, then that argues for it.. Ah... harsh realities of engineering. Well I hope this is judged to be important enough to be included in a future revision of Haskell. Thanks, TJ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type vs TypeClass duality
On Tue, 2007-10-23 at 17:40 +0800, TJ wrote: On 10/23/07, Jules Bean [EMAIL PROTECTED] wrote: That is, the type inference algorithm which GHC uses, which is not the only one you can imagine, but for a variety of reasons is considered to be one of the best choices, cannot 'automatically' construct existentials, and requires some kinds of explicit annotations to 'delimit' the existential. Why can't it automatically construct them then? Assuming we do have a syntax for A list of objects, each of which is of some possibly different type 'a', subject only to the restriction that a is a member of typeclass Show, as the following: ls :: [a where Show a] Then I would think that all the type checker has to do would be to check that, a) everything you cons onto ls is an instance of class Show b) where you extract items from ls, you only use them as you would use any instance of class Show. I think your idea is good, but I also think it's much harder to specify and implement than you seem to imply. Here's an example of one difficult point (the first one I thought of); I'm sure there are many more. Consider the function: show_list x = map show x Can you use show_list on your list? If so: what type does show_list have? How is it implemented? (Consider that in a typical Haskell implementation, show_list would take a hidden dictionary parameter and a normal list parameter. But on your list, show_list takes a list where each element contains a hidden dictionary.) Carl Witty ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type vs TypeClass duality
Why can't it automatically construct them then? Assuming we do have
a syntax for A list of objects, each of which is of some possibly
different type 'a', subject only to the restriction that a is a
member of typeclass Show, as the following:
ls :: [a where Show a]
Then I would think that all the type checker has to do would be to
check that, a) everything you cons onto ls is an instance of class
Show b) where you extract items from ls, you only use them as you
would use any instance of class Show.
Not sure if anyone has mentioned something similar, and it's not quite
what people have been suggesting - but with minimal boilerplate (that
I'm sure a TH hacker could derive for you) you can get close to
typeclass parameterised lists using GADTs ( ghc 6.8 snapshots ;)) at
the moment.
Regards,
Tris
{-# LANGUAGE EmptyDataDecls, ScopedTypeVariables, PatternSignatures, GADTs,
RankNTypes, KindSignatures, TypeOperators #-}
{- A list where all elements are in class Show -}
testList :: SingleList ShowConstraint
testList = () # (LT,EQ,GT) # False # 'a' # (3.0 :: Double) # hello # nil
{- My user functions over that list -}
test = map' (\ShowC - show) testList
test2 = foldr' (\ShowC - (+) . length . show) 0 testList
{- A tiny bit of boilerplate for Show, later rinse repeat for other typeclasses
-}
data ShowConstraint a where
ShowC :: (Show a) = ShowConstraint a
instance Show a = Reify (ShowConstraint a) where
reify = ShowC
{-
*Main test
[(),(LT,EQ,GT),False,'a',3.0,\hello\]
*Main test2
30
-}
{- The bit that is a library -}
{- A generic list definition,
- (a b) is the witness of the type class for this type,
- b is the actual value we put in the list -}
data SingleList (a :: * - *) where
Cons :: (a b) - b - SingleList a - SingleList a
Nil :: SingleList a
{- helper functions to avoid having to pass in the witness explicitly -}
nil :: SingleList a
nil = Nil
infixr 5 #
(#) :: (Reify (a b)) = b - SingleList a - SingleList a
val # rest = Cons reify val rest
{- A way to get the type class constraint witness automagically -}
class Reify a where
reify :: a
{- traditional(ish) map, note the function is passed the witness so it can use
that
- to get the typeclass constraint back into scope by pattern matching on it -}
map' :: forall a c . ((forall b . a b - b - c) - SingleList a - [c])
map' _ Nil = []
map' f (Cons r v rest) = f r v : map' f rest
{- and foldr -}
foldr' :: forall a c . (forall b . a b - b - c - c) - c - SingleList a - c
foldr' f d = go
where
go Nil = d
go (Cons r v rest) = (f r v) (go rest)
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type vs TypeClass duality
On 23/10/2007, Jules Bean [EMAIL PROTECTED] wrote: I will also repeat the non-justified assertion that others have made, and that I've made myself in the other thread, that you don't need existentials as often in haskell as you do in OO languages, and they certainly don't always need to be type-class quantified ones. I also find this, but I worry that it's the old blub paradox again. Haskell makes it a tiny bit clumsy to do value-based dispatch, so you tend to solve problems in ways which doesn't require it. I'm not saying that's the case, but I just can't say that the reason I find myself not using existentials is because I don't need them (whereas they're immensely useful in other languages). I think I've suggested this before, but some sort of syntactical gizmo for expressing the data type which wraps values in class C, and is also instantiated in C itself and just automatically construct the apropriate existential whenever someone uses it, might be worthwhile. Perhaps something like enclosing the class name in angle brackets or something. There needs to be an equivalent way of wrapping the value itself (constructing the wrapper data type), of course (angle brackets again for consistency?). Or automatic type conversion could work, though that seems a bit un-Haskell to me. -- Sebastian Sylvan +44(0)7857-300802 UIN: 44640862 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type vs TypeClass duality
Tristan Allwood: Very cool. I don't understand some (a lot of) parts though: instance Show a = Reify (ShowConstraint a) where reify = ShowC ShowC has type (Show a) = ShowConstraint a, whereas reify is supposed to have type ShowConstraint a. data SingleList (a :: * - *) where Cons :: (a b) - b - SingleList a - SingleList a Nil :: SingleList a Cons has a type variable b in its signature, but no forall. I suppose it comes from the * - * in SingleList's type? That's all I can come up with for now. A great deal of high level coding flying around above my head now. Thanks, TJ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
