Re: MI is sloppy

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On Fri, 12 Dec 2008 15:29:46 +0100, Georg Bauhaus wrote:

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

Again, how? What are you going to check?

> 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

So can you tell from reading the code, what was intended by the programmer
when the object is outside?

> - stopping at type
> correctness seems comparatively lame (unless you have a
> type system such as that of Qi, see below).

It is not lame. The behavior of values = type. So long you deal with
first-order values, types is where you are. When types become themselves
values for type types..., but you are not that far with mere in/out files.

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

Ah, Qi, sorry. What about unlambda?

http://www.madore.org/~david/programs/unlambda

(:-))

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

According to this to be not 0 is a minor difference, just one value after
all... Does absence of fractional values justify the type Integer? Every
seasoned C programmer knows that the only thing that is really needed is
void *. Everything else is just minor differences...

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

This is absolutely true, but it does not mean that you should avoid
differentiation everywhere. In the case in/out files you can differentiate.
It is decidable. So why shouldn't we?

Constrained types appear not because the change is "minor." They do when we
wanted to have polymorphic objects, because the constraint might be
unknown. But note that polymorphic value is of yet another type. So you can
have both type safety where possible and flexibility elsewhere.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de