[Haskell-cafe] Basic question concerning data constructors

[Jake McArthur]

On Dec 30, 2007, at 8:24 AM, Joost Behrends wrote:

> For adapting hws (one of the reasons for me to be here, not many  
> languages have
> a native web server) to Windows i must work on time. In System.Time  
> i found
>
> data ClockTime = TOD Integer Integer
>
> 2 questions arise here: Does this define "TOD" (which i do not find  
> elsewhere)
> together with ClockTime also ? And: Why is this not:
>
> data ClockTime Integer Integer = TOD Integer Integer ?
>
> Is it just an abbreviation for the first? Or is there a connection to
> ClockTime as an "abstract data type" (a notion, which would have a  
> subtle
> different meaning than in OOP - since "instance" is such different  
> thing
> here).

You are right that it defines the TOD constructor. As for you second  
question, I will try to be somewhat formal in my response, so  
hopefully I don't just throw you off more. The quick answer is that  
since we already know the parameters on the right side are Integers,  
we don't need to specify them on the left side.

When you define datatypes, you are essentially defining a type-level  
constructors on the left hand side and (value-level) constructors on  
the right hand side. Just like normal functions, constructors and type  
constructors can be parameterized. Let's deviate for a moment from  
Haskell's notation for data types and approach this from the viewpoint  
of a dependently typed language (a language in which there is little  
separating between the type level and the value level). The data type  
we are defining here is called ClockTime, so its type might be  
represented as

      ClockTime :: *

, where * represents "Kind," the type of types. For completeness, the  
sole constructor we define is called TOD and has type

      TOD :: Integer -> Integer -> ClockTime

. Now, let's say we had tried defining ClockTime with parameters as  
you suggested.

      ClockTime' :: Integer -> Integer -> *

Do you see the problem? In order to use the ClockTime type  
constructor, we would have to use Integer values. This (1) does not  
make much sense in a language like Haskell which doesn't have true  
dependent types, and (2) does not help us in any way with our  
definition of the TOD constructor. We already know by the definition  
of TOD that it takes two Integers and returns a ClockTime. If we used  
this modified definition of ClockTime, we would have to parameterize  
it to specify TOD, maybe like.

      TOD' :: Integer -> Integer -> ClockTime' 2 3

(I chose the 2 and 3 arbitrarily, but these exact values have no  
particular relevance here.) This would not work in Haskell.

However, there are cases where you would want to parameterize a type  
constructor. For example, say we _wanted_ our TOD constructor take two  
values of arbitrary types. If we want the type level to reflect the  
types of these parameters, ClockTime must be parameterized.

      ClockTime'' :: * -> * -> *
      TOD''       :: a -> b -> ClockTime'' a b

In Haskell notation, this would be equivalent to

      data ClockTime'' a b = TOD'' a b

. So, to summarize, the reason that we don't use

      data ClockTime Integer Integer = TOD Integer Integer

is because we don't want to parameterize ClockTime, and even if we  
did, we could not use Integer values like this to do it because  
Haskell is not dependently typed.

- Jake