[Haskell-cafe] Newbie Question on type constructors
Ben Rudiak-Gould
Benjamin.Rudiak-Gould at cl.cam.ac.uk
Mon Nov 1 15:59:34 EST 2004
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
More information about the Haskell-Cafe
mailing list