[Haskell-cafe] Basic question concerning data constructors
Jake McArthur
jake.mcarthur at gmail.com
Sun Dec 30 10:13:53 EST 2007
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
More information about the Haskell-Cafe
mailing list