Re: Formal and informal type systems?

From: Dmitry A. Kazakov (mailbox_at_dmitry-kazakov.de)
Date: 09/30/04 

Date: Thu, 30 Sep 2004 10:25:52 +0200

On 29 Sep 2004 19:53:30 +0200, Mark Lorenzen wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
>
>> But this is already possible. Consider the following:
>>
>> type Optional_Integer (Defined : Boolean) is tagged record
>> case Defined is
>> when True => Value : Integer;
>> when False => null;
>> end case;
>> end record;
>>
>> type Defined_Integer is
>> new Optional_Integer (True) with null record;
>>
>> type Undefined_Integer is
>> new Optional_Integer (False) with null record;
>>
>> procedure Do_Something (I : Defined_Integer) is
>> begin
>> Put_Line ("Defined:" & Integer'Image (I.Value));
>> end;
>>
>> procedure Do_Something (I : Undefined_Integer) is
>> begin
>> Put_Line ("Undefined");
>> end;
>>
>> The point is that there is no need to invent extra parameter matching
>> mechanism. One should use and possibly extend the existing one based on
>> inheritance.
>
> In your example, the correct function is chosen by dispatching
> (or?).

Either by dispatching if the actual is class-wide (then the base should
define it as a primitive operation) or just by type when two Do_Something
overload each other.

>>> The pattern matching could also be extended to case statements such as:
>>>
>>> procedure Do_Something (I : Optional_Integer) is
>>> begin
>>> case I is
>>> when Optional_Integer'(Defined => False) => null;
>>> when Optional_Integer'(Defined => True, Value) =>
>>> Do_Something_More(Value);
>>> end case;
>>> end Do_Something;
>>>
>>> (Credit goes to one of my colleagues for the idea of using the type
>>> name as constructor in the patterns.)
>>
>> I don't understand this example. Looks just like a class-wide of
>> Optional_Integer. Am I right?
>
> The proposal does not have anything to do with tagged types, but
> discriminated records where Defined is the discriminant.

I see. But to me there is no difference. T'Tag is just a discriminant of
T'Class in my view. The problem is that one cannot "dispatch" on subtype
constraints. A subtype is not a distinguishable type, this is why I used
tagged types in my example; because the following is illegal:
 
   type Optional_Integer (Defined : Boolean) is record
     case Defined is
        when True => Value : Integer;
        when False => null;
     end case;
   end record;

   subtype Defined_Integer is Optional_Integer (True);
   subtype Undefined_Integer is Optional_Integer (False);

   procedure Do_Something (I : Defined_Integer) is ...
   procedure Do_Something (I : Undefined_Integer) is ...

You cannot overload in Defined_Integer vs Undefined_Integer in the same
context, they are indistinguishable. Though the following will work:

   type Optional_Integer (Defined : Boolean) is record
     case Defined is
        when True => Value : Integer;
        when False => null;
     end case;
   end record;

   type Defined_Integer is new Optional_Integer (True);
   type Undefined_Integer is new Optional_Integer (False);

   procedure Do_Something (I : Defined_Integer) is ...
   procedure Do_Something (I : Undefined_Integer) is ...

But it is not what needed, I suppose.

Returning to your proposal, if tags were treated as discriminants and
discriminants as tags, then one could "derive" from a variant record a
constrained (specialized) type which would be distinguishable from the
base. No patterns needed! (?)

>> To start with, we could introduce function types. I cannot understand why
>> we have access-to-function types and still have to types for the target.
>
> Function types would be very cool, but it is probably be a huge change
> in the language.

It depends on which operation on subroutines will be allowed. If we allow
nothing except call, no variables, then there will be almost no impact. 

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