[Haskell-cafe] Newbie Question on type constructors

[Ben Rudiak-Gould]

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