[Haskell-cafe] Newbie Question on type constructors

[Paul Hudak]

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