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 xwith 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 aIn 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
_______________________________________________ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
