Can it be argued that Ada subtypes are equivalent to dependent types?

Question

I try to wrap my head around Ada and I read a little about the dependent types in Agda and Idris.

Can it be argued that subtypes in Ada are equivalent to dependent types?

Answer 1

In computer science and logic, a dependent type is a type whose definition depends on the value. A pair of integers is a type. "A pair of integers where the second is larger than the first" is a dependent type due to the dependence on the value.

So you can use subtypes to implement 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;

Answer 2

, , , .

Answer 3

:

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

Sub_type B_Tis actually "the same" as the type A_T, since it does not create any restrictions on it. It is rather a type renaming A_Tfor convenience, for example. So you cannot say that Ada subtypes are dependent types.