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