Cagdas Ozgenc wrote:

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).

I think you're confused about what the type declarations mean. When you say

sqrt :: Float -> Float

you're promising to operate over /all/ Floats. If you want to restrict that to only certain Floats, you would need a different ``type'':

sqrt :: {x :: Float | x >= 0} -> Float

or introduce your own type isomorphic to this. Unfortunately, Haskell doesn't allow {x :: Float | x >= 0} as a type, nor does it provide a positive-only floating point type. I think your problem is related to the concepts of ``different'' and ``plug in''. All the Haskell compiler performs is type checking; unfortunately, type checking is purely structural; it doesn't enquire whether the resulting program is correct (or even meaningful). You can tell Haskell isn't concerned with whether your programs are meaningful, because Haskell allows the following program:

main = main

This is obviously completely meaningless. Now, then, obviously sqrt and negate are different in the sense of ``unequal''. If you don't know, equality between Haskell functions is defined (ommitting some complications) like such:

f = g <=> forall x.f x = g x

Clearly negate /= sqrt! However, taking your notion of ``not different'', which is apparantly

f = g <=> domain f = domain g

note that both

sqrt x = x ** (1/2)

and

qrrt x = x ** (1/4)

have the same domain. Are they equivalent? It (obviously) depends on the context. Consider the function dist:

dist :: (Double, Double) -> (Double, Double) -> Double dist (x1, x2) (y1, y2) = sqrt ((x1 - y1) ** 2 + (x2 - y2) ** 2)

You can't use qrrt in dist and expect it to be correct any more than you an use negate. On the other hand there may be terms which don't care which among qrrt and sqrt you give them but don't want negate. So, equivalence is a tricky problem---and one you can't solve without reading the programmer's mind. That's why Haskell doesn't address it, being content with type checking.

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).

You're right that the type constructor (,) doesn't carry a lot of information; but I think you misunderstand why: given a type declaration

data FiddleDeDee a b = MkFiddleDeDee a b

FiddleDeDee is ``structurally equivalent'' to (,), and also carries about as much information. Consider: ``What's the French for fiddle-de-dee?'' ``Fiddle-de-dee's not English,'' Alice replied gravely. ``Who ever said it was?'' said the Red Queen. Lewis Carroll, ``Through the Looking Glass''

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.

I assume from your example that by ``structural equivalence'' you mean the relationship between D and E. But they also share that relationship with (,)---what exactly is the difference? Functions over (D Int Int) work even if the caller thinks its (D #apples #oranges) and the function thinks its (D #books #authors). Again, the problem is with Int, not D (or (,)).

Thanks again.