Newbie Question on type constructors
This is a tiny question on the "data" syntax. Consider the following (cribbed from Paul Hudak's "School of Expression" book, page 22): data Shape = Circle Float | Square Float I read this something along the lines of "'Shape' is a type constructor, for use in other type-defining expressions, and 'Circle' and 'Sqare' are its two data constructors, which should be used like functions of type 'Float -> Shape'". Indeed, typing "Circle" at the Hugs prompt reveals that Haskell has a "function" named "Circle" with type "Float -> Shape." However, I don't know of other circumstances where (1) I can declare functions with capitalized names (Hugs groans about syntax errors if I attempt the following: Circle2 :: Float -> Shape Circle2 = Circle And (2) where the argument-types of a function can be declared on the function's right-hand side. So, in some sense, am I right to think of "data" as a special syntax for special kinds of function declarations, namely data-constructor function declarations, and that this syntax is different in appearance, but not terribly different in meaning, from the ordinary syntax, typified by circle2 :: Float -> Shape circle2 = Circle (this is just the uncialized version of the one above, and is perfectly legal) Apologies if this is just too nitpicky and pedantic for words, but I try to notice everything.
On Fri, 29 Oct 2004, Brian Beckman wrote:
This is a tiny question on the "data" syntax.
<snip> There's a significant difference between data constructors and ordinary functions - you can't use pattern-matching to match an ordinary function. In effect, data constructors are used not just to build values but also to take them apart. Syntactically speaking, data constructors must begin with a capital letter, variables and function definitions with a lower case letter. -- flippa@flippac.org
Brian Beckman wrote:
data Shape = Circle Float | Square Float
I read this something along the lines of "'Shape' is a type constructor, for use in other type-defining expressions, and 'Circle' and 'Sqare' are its two data constructors, which should be used like functions of type 'Float -> Shape'". Indeed, typing "Circle" at the Hugs prompt reveals that Haskell has a "function" named "Circle" with type "Float -> Shape."
However, I don't know of other circumstances where (1) I can declare functions with capitalized names (Hugs groans about syntax errors if I attempt the following:
Circle2 :: Float -> Shape Circle2 = Circle
And (2) where the argument-types of a function can be declared on the function's right-hand side.
I remember being confused in a similar way by data constructors when I learned Haskell. You might find it easier to think of "Circle" and "Square" as part of the name of a value. "Circle 1.2" is one of the values in the type Shape, for example; it's not a function call which returns the value, it just *is* the value. Circle by itself doesn't really mean anything -- it's not a value of any type -- and Haskell could have been designed to make it a syntax error. But for convenience Haskell's designers decided to treat it as though it meant (\x -> Circle x). -- Ben
Oh, I disagree with this point of view. Circle is certainly a value, i.e. a full-fledged function, as Brian Beckman correctly surmised. The Haskell designers did not decide "for convenience" that Circle is the same as \x -> Circle x. Rather, that's a fundamental law (the eta law, to be exact) of the lambda calculus, on which Haskell is based. The real reason that the Haskell designers chose to have constructors begin with a capital letter is to make pattern-matching clearer. For example, if one writes (\Foo -> 42) it is clear that Foo is a constructor, and this function will be an error when applied to anything but Foo, whereas (\foo -> 42) will match anything. If the namespaces were not separated in this way, then you wouldn't know whether "foo" was a constructor or a formal parameter, without looking at your whole program -- including imports -- to track down all "data" declarations. I hope this helps, -Paul Ben Rudiak-Gould wrote:
Brian Beckman wrote:
data Shape = Circle Float | Square Float
I read this something along the lines of "'Shape' is a type constructor, for use in other type-defining expressions, and 'Circle' and 'Sqare' are its two data constructors, which should be used like functions of type 'Float -> Shape'". Indeed, typing "Circle" at the Hugs prompt reveals that Haskell has a "function" named "Circle" with type "Float -> Shape."
However, I don't know of other circumstances where (1) I can declare functions with capitalized names (Hugs groans about syntax errors if I attempt the following:
Circle2 :: Float -> Shape Circle2 = Circle
And (2) where the argument-types of a function can be declared on the function's right-hand side.
I remember being confused in a similar way by data constructors when I learned Haskell. You might find it easier to think of "Circle" and "Square" as part of the name of a value. "Circle 1.2" is one of the values in the type Shape, for example; it's not a function call which returns the value, it just *is* the value. Circle by itself doesn't really mean anything -- it's not a value of any type -- and Haskell could have been designed to make it a syntax error. But for convenience Haskell's designers decided to treat it as though it meant (\x -> Circle x).
-- Ben
-- Professor Paul Hudak Chair, Dept of Computer Science Office: (203) 432-1235 Yale University FAX: (203) 432-0593 P.O. Box 208285 email: paul.hudak@yale.edu New Haven, CT 06520-8285 WWW: www.cs.yale.edu/~hudak
Oh, I disagree with this point of view. Circle is certainly a value, i.e. a full-fledged function, as Brian Beckman correctly surmised. The
Ben Rudiak-Gould wrote:
Brian Beckman wrote:
data Shape = Circle Float | Square Float
I read this something along the lines of "'Shape' is a type constructor, for use in other type-defining expressions, and 'Circle' and 'Sqare' are its two data constructors, which should be used like functions of type 'Float -> Shape'". Indeed, typing "Circle" at the Hugs prompt reveals that Haskell has a "function" named "Circle" with type "Float -> Shape."
Indeed, they are functions. Another way of thinking about it is as an "initial algebra" (technical term). What this means is this: "Shape" is a set of values that contains - the result of Circle x for all values x :: Float - the result of Square x for all values x :: Float such that - there's nothing in Shape that can't be reached this way ("no junk") - there is no value in Shape that can be reached in two different ways ("no confusion"). HTH. --KW 8-)
Keith Wansbrough wrote:
Indeed, they are functions. Another way of thinking about it is as an "initial algebra" (technical term). What this means is this:
"Shape" is a set of values that contains - the result of Circle x for all values x :: Float - the result of Square x for all values x :: Float such that - there's nothing in Shape that can't be reached this way ("no junk") - there is no value in Shape that can be reached in two different ways ("no confusion").
I think this is orthogonal to the point of contention. For all x :: Float, what value results when your function Circle is applied to the argument x? Obviously, my value Circle x. So the function Circle can be eliminated from the definition by inlining, yielding
"Shape" is a set of values that contains - the value Circle x for all values x :: Float - the value Square x for all values x :: Float such that [...]
This is exactly how I would define Shape. (Well, not quite -- there *are* values in Shape that can't be constructed this way, but that's a totally different issue.) -- Ben
Paul Hudak wrote:
Oh, I disagree with this point of view. Circle is certainly a value, i.e. a full-fledged function, as Brian Beckman correctly surmised.
Interesting. I don't claim that my viewpoint is the One True Path, but I don't think it's wrong, either. I know you're interested in the teaching of Haskell, and the fact remains that I *was* confused by data constructors when I learned Haskell, and it *did* help me to stop thinking of them as functions. Different people learn in different ways, and that's how I learned; even now I find this view more natural than the view of constructors as functions. The wording of the OP's article made me think that he might be suffering from the same conceptual problem, so I tried to suggest the approach which worked for me.
The Haskell designers did not decide "for convenience" that Circle is the same as \x -> Circle x. Rather, that's a fundamental law (the eta law, to be exact) of the lambda calculus, on which Haskell is based.
I think you're begging the question here -- the eta law applies to functions -- but maybe you're just elaborating on your view rather than arguing for it, as I was. (I.e. I was elaborating, not arguing, when I said that Circle was a function "for convenience".)
The real reason that the Haskell designers chose to have constructors begin with a capital letter is to make pattern-matching clearer.
Certainly it's odd to be able to match on the result of a function. "case factorial (2*3) of factorial n -> ..." won't work, so it's surprising that "case Circle (2*3) of Circle x -> ..." does, if Circle is a function. On the other hand, if "Circle 6" is just a literal value, it's not at all surprising that "case Circle 6 of Circle x -> ..." does what it does. And, at least for me, that extends to "case Circle (2*3) of Circle x -> ..." as well. (*) is being called in this example, and is returning an entirely new value, 6, but Circle is just getting "added on" to that result, and then stripped off again. There's a clear symmetry between construction and deconstruction which doesn't seem nearly as clear if Circle is seen as a function. It occurs to me that when I talk about functions here, I am talking about Haskell function values, not about functions as equations "f(x) = ...". In particular, one cannot write an invert :: (a->b) -> Maybe (b->a) which never returns a wrong answer, except for invert = const Nothing -- this is why it makes no sense to me to imagine Circle as being a Haskell *value*. I have no problem imagining it as a function in a more abstract mathematical sense; it's just that Haskell function values don't have that extra structure. The view of Circle that I was trying to express is closer to Prolog clauses. One can assert circle(1.2), and that assertion will match circle(x), but it doesn't really make sense to assert circle, or to try to match it. Have I succeeded in reconciling our views? -- Ben
On Mon, 1 Nov 2004, Ben Rudiak-Gould wrote:
Paul Hudak wrote:
Oh, I disagree with this point of view. Circle is certainly a value, i.e. a full-fledged function, as Brian Beckman correctly surmised.
Interesting. I don't claim that my viewpoint is the One True Path, but I don't think it's wrong, either. I know you're interested in the teaching of Haskell, and the fact remains that I *was* confused by data constructors when I learned Haskell, and it *did* help me to stop thinking of them as functions.
When I saw 'data' the first time, it looked for me similar to C's unions, i.e. a data structure. Sometime later I got the point that constructors are also functions. :-)
Ben Rudiak-Gould wrote:
Have I succeeded in reconciling our views?
Perhaps! In particular, perhaps it's just a pedagogical issue. Note that instead of: data Shape = Circle Float | Square Float the Haskell designers might have used the following syntax: data Shape where Circle :: Float -> Shape Square :: Float -> Shape which conveys exactly the same information, and makes it quite clear that Circle and Square are functions. I often point this out to my students, because I find it less confusing than Haskell's data type declaration, where type constructors and value constructors are intermixed (i.e. "Circle Float"). Would this have been less confusing for you? As for pattern matching, I think the key point relates to Keith Wansbrough's comment that an algebraic data type denotes an initial algebra. If you want to retain referential transparency, each application of the function being pattern-matchined against must yield a unique value (i.e. "no confusion" as Keith describes it). This is guaranteed with a constructor, but not with arbitrary functions. So, another way to look at it is that constructors simply carve out a portion of the function space where this can be guaranteed. That said, there are lots of interesting directions to pursue where pattern-matching against functions IS allowed (requiring higher-order unification and the like). I suppose that topic is out of the scope of this discussion. -Paul Ben Rudiak-Gould wrote:
Paul Hudak wrote:
Oh, I disagree with this point of view. Circle is certainly a value, i.e. a full-fledged function, as Brian Beckman correctly surmised.
Interesting. I don't claim that my viewpoint is the One True Path, but I don't think it's wrong, either. I know you're interested in the teaching of Haskell, and the fact remains that I *was* confused by data constructors when I learned Haskell, and it *did* help me to stop thinking of them as functions. Different people learn in different ways, and that's how I learned; even now I find this view more natural than the view of constructors as functions. The wording of the OP's article made me think that he might be suffering from the same conceptual problem, so I tried to suggest the approach which worked for me.
The Haskell designers did not decide "for convenience" that Circle is the same as \x -> Circle x. Rather, that's a fundamental law (the eta law, to be exact) of the lambda calculus, on which Haskell is based.
I think you're begging the question here -- the eta law applies to functions -- but maybe you're just elaborating on your view rather than arguing for it, as I was. (I.e. I was elaborating, not arguing, when I said that Circle was a function "for convenience".)
The real reason that the Haskell designers chose to have constructors begin with a capital letter is to make pattern-matching clearer.
Certainly it's odd to be able to match on the result of a function. "case factorial (2*3) of factorial n -> ..." won't work, so it's surprising that "case Circle (2*3) of Circle x -> ..." does, if Circle is a function. On the other hand, if "Circle 6" is just a literal value, it's not at all surprising that "case Circle 6 of Circle x -> ..." does what it does. And, at least for me, that extends to "case Circle (2*3) of Circle x -> ..." as well. (*) is being called in this example, and is returning an entirely new value, 6, but Circle is just getting "added on" to that result, and then stripped off again. There's a clear symmetry between construction and deconstruction which doesn't seem nearly as clear if Circle is seen as a function.
It occurs to me that when I talk about functions here, I am talking about Haskell function values, not about functions as equations "f(x) = ...". In particular, one cannot write an invert :: (a->b) -> Maybe (b->a) which never returns a wrong answer, except for invert = const Nothing -- this is why it makes no sense to me to imagine Circle as being a Haskell *value*. I have no problem imagining it as a function in a more abstract mathematical sense; it's just that Haskell function values don't have that extra structure.
The view of Circle that I was trying to express is closer to Prolog clauses. One can assert circle(1.2), and that assertion will match circle(x), but it doesn't really make sense to assert circle, or to try to match it.
Have I succeeded in reconciling our views?
-- Ben
Paul Hudak wrote:
Ben Rudiak-Gould wrote:
Have I succeeded in reconciling our views?
Perhaps! In particular, perhaps it's just a pedagogical issue.
I'm interested in it mainly from a pedagogical perspective, yes.
Note that instead of: data Shape = Circle Float | Square Float
the Haskell designers might have used the following syntax:
data Shape where Circle :: Float -> Shape Square :: Float -> Shape
which conveys exactly the same information, and makes it quite clear that Circle and Square are functions.
No, this is totally different from what I'm talking about. My position for the moment is that they *aren't* functions (or, more precisely, that they shouldn't be so taught), and anything that tries to further the illusion that they are is then a step in the wrong direction. In particular, your notation with type signatures makes it totally unclear that Circle and Square have disjoint ranges; in fact it looks like they have the same range. This notation would have increased my confusion when I was still learning, because what I didn't understand at that time was the nature of the type Shape. Saying that Circle and Square are functions which take a Float and return a Shape tells me nothing about what a Shape is; it might as well be an abstract data type. What I needed to know, and was never clearly told, was that Shape is *precisely the following set:* { Circle 1.2, Circle 9.3, ..., Square 1.2, Square 9.3, ...}. You could even throw in a _|_ and some exceptions-as-values, though I'm not sure it would have been advisable (little white lies are an important pedagogical tool, as long as you eventually own up). The syntax that would have made the most sense to me would have been something like data Shape = forall x::Float. Circle x forall x::Float. Square x with maybe a "+" or something joining the lines, though that might have done more harm than good. Of course GHC 6.4 has your function syntax now with the introduction of GADTs, but I think that it's a mistake; in fact it's interfering right now with my attempt to understand what GADTs are! I suppose I would prefer data Term a = forall x :: Int. Lit x :: Term Int forall x :: Term Int. Succ x :: Term Int forall x :: Term Int. IsZero x :: Term Bool forall x :: Term Bool. forall y,z :: Term a. If x y z :: Term a In fact, maybe I'll try rewriting everything in this form and see if it helps me. I suppose once I do understand GADTs I'll have a better idea of what would have helped.
As for pattern matching, I think the key point relates to Keith Wansbrough's comment that an algebraic data type denotes an initial algebra. If you want to retain referential transparency, each application of the function being pattern-matchined against must yield a unique value (i.e. "no confusion" as Keith describes it). This is guaranteed with a constructor, but not with arbitrary functions. So, another way to look at it is that constructors simply carve out a portion of the function space where this can be guaranteed.
I have no objection to this viewpoint except that I fear it's too abstract for students. I can understand it because I already understand algebraic data types, but I don't think it would have helped me learn.
That said, there are lots of interesting directions to pursue where pattern-matching against functions IS allowed (requiring higher-order unification and the like). I suppose that topic is out of the scope of this discussion.
I don't think I've heard of this (unless you're talking about logic programming). Can you point me to some papers? -- Ben
Ben Rudiak-Gould
In particular, your notation with type signatures makes it totally unclear that Circle and Square have disjoint ranges; in fact it looks like they have the same range. : The syntax that would have made the most sense to me would have been something like
data Shape = forall x::Float. Circle x forall x::Float. Square x
with maybe a "+" or something joining the lines, though that might have done more harm than good.
Instead of +, perhaps we could use U (union) - we are talking about sets of values after all. And U is analogous to V (logical or, a value in the union is either in one set or the other), and on or the most common 'or' characters is, of course, the vertical bar, so perhaps the current syntax makes sense after all? :-) -kzm -- If I haven't seen further, it is by standing in the footprints of giants
Sorry, I had to drop out of this thread for a few days... Ben Rudiak-Gould wrote:
Paul Hudak wrote:
Note that instead of: data Shape = Circle Float | Square Float
the Haskell designers might have used the following syntax:
data Shape where Circle :: Float -> Shape Square :: Float -> Shape
which conveys exactly the same information, and makes it quite clear that Circle and Square are functions.
No, this is totally different from what I'm talking about. My position for the moment is that they *aren't* functions (or, more precisely, that they shouldn't be so taught), and anything that tries to further the illusion that they are is then a step in the wrong direction.
Well then, I guess we'll just have to agree to disagree...:-) They are very definitely functions in my mind: they can be applied, passed as arguments, etc. "If it acts like a duck, then it is a duck." The confusion is that they are MORE than just functions, because of their special treatment in pattern matching. But to deny their functionhood in like denying a king his manhood :-)
In particular, your notation with type signatures makes it totally unclear that Circle and Square have disjoint ranges; in fact it looks like they have the same range.
But they DO have the same range -- they're just not surjective. That said, what you ask for is not unreasonable, it's just that I don't know how to express it in Haskell, for any kind of function. (Unless one were to explicity encode it somehow.)
This notation would have increased my confusion when I was still learning, because what I didn't understand at that time was the nature of the type Shape. Saying that Circle and Square are functions which take a Float and return a Shape tells me nothing about what a Shape is; it might as well be an abstract data type. What I needed to know, and was never clearly told, was that Shape is *precisely the following set:* { Circle 1.2, Circle 9.3, ..., Square 1.2, Square 9.3, ...}. You could even throw in a _|_ and some exceptions-as-values, though I'm not sure it would have been advisable (little white lies are an important pedagogical tool, as long as you eventually own up).
Yes, I can understand your confusion, and I have had students express the same thing. But after I explain essentially what you have written above, there was no more trouble.
The syntax that would have made the most sense to me would have been something like
data Shape = forall x::Float. Circle x forall x::Float. Square x
with maybe a "+" or something joining the lines, though that might have done more harm than good.
I don't see much advantage of this over Haskell's current syntax. You still need to explain its semantics in a way that suits your needs, so you might as well explain the original syntax in the same way.
Of course GHC 6.4 has your function syntax now with the introduction of GADTs, but I think that it's a mistake; in fact it's interfering right now with my attempt to understand what GADTs are! I suppose I would prefer
data Term a = forall x :: Int. Lit x :: Term Int forall x :: Term Int. Succ x :: Term Int forall x :: Term Int. IsZero x :: Term Bool forall x :: Term Bool. forall y,z :: Term a. If x y z :: Term a
In fact, maybe I'll try rewriting everything in this form and see if it helps me. I suppose once I do understand GADTs I'll have a better idea of what would have helped.
I almost mentioned GADT's earlier, but didn't want to stray too far from the path. In fact GADT's strengthen my argument, but I see you don't like their syntax either.
That said, there are lots of interesting directions to pursue where pattern-matching against functions IS allowed (requiring higher-order unification and the like). I suppose that topic is out of the scope of this discussion.
I don't think I've heard of this (unless you're talking about logic programming). Can you point me to some papers?
The work that I'm only somewhat aware of is that out of the "logical frameworks" community, where "higher-order abstract syntax" makes it desirable to work "underneath the lambda", in turn making it desirable to pattern-match against lambdas. See, for example, Carsten Schuermann's work (http://cs-www.cs.yale.edu/homes/carsten/). -Paul
On Mon, 1 Nov 2004, Ben Rudiak-Gould wrote:
In particular, one cannot write an invert :: (a->b) -> Maybe (b->a) which never returns a wrong answer, except for invert = const Nothing
How about: invert = undefined This never returns an answer at all, so it can't return a wrong one! Finn
Finn Wilcox wrote:
On Mon, 1 Nov 2004, Ben Rudiak-Gould wrote:
In particular, one cannot write an invert :: (a->b) -> Maybe (b->a) which never returns a wrong answer, except for invert = const Nothing
How about:
invert = undefined
This never returns an answer at all, so it can't return a wrong one!
Sorry, I should have been clearer: my Nothing return was intended to mean "I don't know an answer", not "there is no answer". So my const Nothing is like your undefined, a function which never returns an answer (and thus never returns a wrong one). -- Ben
participants (8)
-
Ben Rudiak-Gould -
Brian Beckman -
Finn Wilcox -
Henning Thielemann -
Keith Wansbrough -
Ketil Malde -
Paul Hudak -
Philippa Cowderoy