type equivalency

[Jon Cast]

Cagdas Ozgenc <co19@cornell.edu> 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.