type equivalency

[Jon Cast]

Andrew J Bromage <andrew@bromage.org> wrote:

> G'day all.

> On Wed, Jun 05, 2002 at 08:20:03PM -0500, Jon Cast wrote:

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

> That would be true of Haskell functions were constrained to be total
> functions.  They are not.  Sqrt takes values of type Float, but it
> just happens to be a partial function over that type.

That depends on what you mean by ``partial function''.  Technically,
of course, a function of type (a -> b) is a subset of (a x b)
satisfying certain constraints.  All Haskell functions f satisfy the
property (forall x::a. exists y::b. (x, y) <- f), so you can always
get a value of f at any x.  In other words, sqrt can take any x and
compute with it; it just delivers _|_ at some of them.  My point was,
(sqrt x) is legal Haskell (and has a value) for all (x :: Float).

> > Unfortunately, Haskell doesn't allow {x :: Float | x >= 0} as a
> > type, nor does it provide a positive-only floating point type.

> One general rule of strongly-typed programming is: A program is type
> correct if it is accepted by my favourite type checker.  A corollary
> is that what you call a type, I reserve the right to call a
> precondition.

If I accepted that, I would be un-defining crucial terms.  That would
destroy the potential for discussion here, no?

> Cheers,
> Andrew Bromage

Jon Cast