[Haskell-cafe] ReRe: Basic question concerning data constructors

[Chaddaï Fouché]

2007/12/30, Joost Behrends <webmaster at h-labahn.de>:
> > . 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.
>
> Cannot see any problem here - do we NOT want ClockTime to be initialized by two
> Integers ? Or is this the main reason for introducing "TOD" - to be able to
>  change it without having to make any changes to code using ClockTime ?
> To repeat myself - am i right understanding, that this needs a differently named
> data constuctor ?

We want a value of type ClockTime to be initialized by two Integers,
but the type of this value will be ClockTime, not (ClockTime 2 3), its
_type_ won't depend on its _content_, ok ?

With dependent types, you can have type constructors (not data
constructors) with an non-type parameter, but Haskell hasn't dependent
typing. To give you an example of the potential usefulness of
dependent type, you can have a list type which is parametrized by the
length of the list.
data List :: * -> Integer -> * where
  Empty :: List a 0
  Cons :: a -> List a n -> List a (n+1)
you then can type head() so that you can't apply it on an empty list :
head :: List a n -> List a (n-1) | n > 0
head (Cons x xs) = xs
and the compiler will enforce this restriction at compile time (as
well as it can).

Dependent typing is interesting but not really practical yet. You can
simulate it more or less with Haskell and GHC extensions, but Haskell
isn't dependently typed.

-- 
Jedaï