[Haskell-cafe] ReRe: Basic question concerning data constructors
Thanks to both fast answers. there remain problems with Jakes mail for me. This: > 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. is very useful for me. "data" defines TWO constructors, ok. And if i want construction on the type level, then the arguments must obviously be type-"valued", means parameters. From this i conclude, that data ClockTime Integer Integer = ... would never make sense, whatever on the right size. The next isn't understandable for me - i have not the slightest conception of dependently typed languages. Then i arrive at > . 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 ? (I cited "abstract type" from the library reference. Not important for me at the moment, what that means in Haskell.) Thanks for your attention, Joost ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ReRe: Basic question concerning data constructors
2007/12/30, Joost Behrends <[EMAIL PROTECTED]>: > > . 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ï ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ReRe: Basic question concerning data constructors
On Dec 30, 2007, at 12:32 PM, Joost Behrends wrote: Thanks to both fast answers. there remain problems with Jakes mail for me. This: 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. is very useful for me. "data" defines TWO constructors, ok. To be more accurate, it defines one type constructor and however many value constructors you want to define. Then i arrive at . 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 ? No, we do not want the _type_ to be parameterized with our _values_. That is the difference between ClockTime and TOD; ClockTime is on the type level and TOD is on the value level. ClockTime is the type of the value returned by TOD after applying it to two Integer values. - Jake ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
