type equivalency

Cagdas Ozgenc co19@cornell.edu
Thu, 6 Jun 2002 00:33:33 +0300


For example all functions with Int -> Int are type equivalent, because
structural equivalency is used. Most of the time the functions are not
compatible because they have different pre/post conditions, even though they
seem to have the same input output types. I rather make my functions an
instance of a type-class to tell the compiler that they can be used
interchangably. For example

sqrt :: Float -> Float
sqrt a =  /* pre : a >= 0 */

negate :: Float -> Float
/* no precondition */

are different functions. You cannot just plug one in place of another (you
can in Haskell because of structural type equivalency).

Also a function working over (Int,Int) will do so even if the numbers are
totally irrelevant to that function. They maybe the number of
(apples,oranges) or number of (books,authors).

However,

data D a b = MkD a b

data E a b = MkE a b

(D Int Int) and (E Int Int) are trated as different because of name
equivalency testing.

Basically there are 2 type constructors -> ( , ) with structural
equivalency, which is odd. Someone just dumped some idiosyncracies of lamda
calculus into the language.

Thanks again.

> Cagdas Ozgenc writes:
>  | Greetings.
>  |
>  | I know 2 special type constructors(there might be other that I do
>  | not know yet) -> and ( , ) where structural type equivalency is
>  | enforced and we can also create new types with an algebric type
>  | constructor notation where name equivalency is enforced.
>  |
>  | What is the rationale? I mean why 2 special type constructors, but
>  | not 5, or 10 or N?
>  |
>  | Thanks for taking time.
>
> -> and (,) are names of type contructors, each with kind *->*->*.
>
> Offhand, I don't see any difference in the way we'd test equivalency
> involving -> or (,) or D, where:
>
>     data D a b = MkD a b
>
> If that doesn't help, will you please give a more concrete example of
> what you mean?
>
> Regards,
> Tom