Re: MI is sloppy

[Georg Bauhaus <rm.dash-bauhaus@futureapps.de>]

Dmitry A. Kazakov schrieb:

>>> Constraint_Error propagation is the contracted behavior. You have signed
>>> that contract, enjoy it.
>> But the compiler informs you that Constraint_Error will
>> be raised if your program is such that it will be raised.
>> Anything wrong with correcting the program?
> 
> How? The program is already correct it does what you asked it to do.

I had understood that the subprogram in question
was *formally* receiving any file, and in addition
was constrained to only accept a file object that
falls into the correct subset of the File type.
This kind of constraint might be interpreted to be a run-time
thing, but could be made a compile-time check where possible.

What's a correct program?
If the program passes an object outside the set,
it is not correct, taking "correct" to mean the program
operates as intended by the programmer - stopping at type
correctness seems comparatively lame (unless you have a
type system such as that of Qi, see below).


>> If we wanted more of the minor differences covered
>> by type hierarchies, we might end up with a Qi type
>> system... For Ada?
> 
> 1. Qt is not a programming language.

Qi, 'Q' & Character'Val(151), is a programming
language that includes the most powerful type system
of all type systems ever to be invented (in terms of
Turing equivalence).

http://www.lambdassociates.org/


> 2. There is no minor differences in terms of correctness. An incorrect
> program is incorrect.
> 
> There is no *any* way to predict the effect of incorrectness. The system is
> not only instable, it is simply unknown. It does not obey the logic of
> (some) physical systems, where you can A) measure the change, B) measure
> the effects. There is no metric, no distance, no way to measure things, it
> is just non-continuous etc. "minor differences" is meaningless.
> 
> Last but not least, how are you going to make differences visible to the
> program reader? By writing comments explaining when and how
> Constraint_Error, other exceptions, and program crashes would happen?

Minor differences can be formally specified by writing
additional constraints that may not be impressive
enough to justify yet another type.  As you know,
it is not possible (according to different sources)
to express any significant amount of differentiation
employing just a type system *unless* the type system
is so powerful that you are expected and willing to
wait an indeterminate amount of time until your compiler's
type checking parts start commenting on your program, if ever.