# [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

```