[Haskell-cafe] Newbie Question on type constructors
Paul Hudak
paul.hudak at yale.edu
Thu Nov 4 10:06:26 EST 2004
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
More information about the Haskell-Cafe
mailing list