Hi.
Marcin 'Qrczak' Kowalczyk writes, in reply to Ch. A. Herrmann:
> > If using a natural type, people will insist on having a partial
> > minus operation. How should the compiler check that this operation
> > is well-defined? If the compiler can't, why have this type at all
> > if the integers are available?
>
> This is not a valid argument, because it requires adding the result
> of 1/0 to the type of rationals, and it says that you must use complex
> numbers instead of reals because reals don't have square root defined
> on all arguments... Or I can't see the difference.
>
> I don't say that we need the natural type in Haskell. It is so close
> to integers (only half of values is wasted) and it is so common to
> convert between the two, that it's not worth the duplication and
> confusion. I certainly would not want to have to convert the result
> of length from natural to integer when I want to compute a signed
> difference between two lengths!
This has wandered within pouncing distance of one of my pet topics:
specialisation by constraint (S by C), as described in [1].
I'm posting this, not as a wish list item, but in the hope that people
will reply "That's already been explored in the FP world, in
so-and-so's 1986 paper", or just think "That's a nice intuitive way of
dealing with inheritance".
S by C is an approach to inheritance, in the "every value in type T2
is also in type T1" sense. The features of S by C include:
- When a type T2 is declared as a subtype of a type T1, the
declaration includes a constraint which distinguishes values in T2
from values in T1\T2.
For example, every natural number is an integer, and an integer x
is a natural number if and only if x >= 0. There is no such thing
as a value 0 which counts as an integer but not as a natural
number.
- The principle of value substitutability applies. If T2 is a
subtype of T1, then anywhere that type T1 is inferred at compile
time, it is acceptable for a value of type T2 to appear at run
time.
For example, a natural number is acceptable wherever an integer is
expected. The literal -1 evaluates to an integer value, but the
literal 0 evaluates to a natural number value, even if both those
literals were originally declared in connection with the integer
type.
- In case we need a more specific type than can be inferred at
compile time, there are controlled ways of deferring the check
until run time.
For example, if we can only be sure of having an integer value,
but need a natural number value to apply a function like take or
drop to, we use functions like the following, which are defined as
a by-product of declaring Nat:
isNat :: Rational -> Bool
treatAsNat :: Rational -> Maybe Nat
(Assuming that Rational is the maximal supertype of Nat, and using
the familiar Haskell syntax and Maybe.)
S by C is focussed on properties of values (like nonnegativity), in
contrast to Haskell's class system, which is focussed on properties of
types (like closure under subtraction).
This makes an S by C declaration of a natural number type depend on an
existing declaration of an integer type. A Haskell natural number
class, however, would belong in the predicate for Integral (perhaps
indirectly).
Regards,
Tom
[1] Foundation for Object/Relational Databases: The Third Manifesto,
C. J. Date and Hugh Darwen,
Addison-Wesley 1998
