Könnte argumentiert werden, dass Ada-Subtypen äquivalenten abhängigen Typen entsprechen?

Question

Ich habe versucht, meinen Kopf um Ada zu wickeln, und ich habe ein wenig über dependent types in Agda und Idris gelesen.

Kann man argumentieren, dass subtypes in Ada äquivalent zu abhängigen Typen sind?

Answer 1

Nein, nicht, wie ich die formale Definition der abhängigen Typen lesen Sie verwiesen.

Answer 2

Betrachten Sie das folgende Beispiel:

type A_T is range 1 .. 50; 
subtype B_T is A_T; 

Sub_type B_T in der Tat ist die „gleiche“, wie der Typ A_T, da es keine Beschränkungen auf, es stellen sich. Es ist eher eine Umbenennung vom Typ A_T für die Bequemlichkeit, zum Beispiel. Daher können Sie nicht sagen, dass Ada-Untertypen abhängige Typen sind.

Answer 3

In der Informatik und Logik ist ein abhängiger Typ ein Typ, dessen Definition von einem Wert abhängt. Ein "Paar Ganzzahlen" ist ein Typ. Ein "Paar von ganzen Zahlen, wobei die zweite größer als die erste ist" ist aufgrund der Abhängigkeit von dem Wert ein abhängiger Typ.

So können Sie Subtypen verwenden them--

-- The "pair of integers" from the example. 
Type Pair is record 
    A, B : Integer; 
end record; 

-- The "where the second is greater than the first" constraint. 
Subtype Constrained_Pair is Pair 
    with Dynamic_Predicate => Constrained_Pair.B > Constrained_Pair.A;