CODEWITHSUNDEEP
typesadadependent-typetype-theory
nosefouratyou
nosefouratyou

Reputation: 341

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

I've been trying to wrap my head around Ada, and I've been reading a bit about dependent types in Agda and Idris.

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

Upvotes: 6

Views: 1655

Answers (3)

Shark8
Shark8

Reputation: 4198

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

So then 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;

Upvotes: 3

NeoSer
NeoSer

Reputation: 519

Consider the following example:

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

Sub_type B_T is in fact the "same" as the type A_T, since it does not pose any restrictions on it. It is rather a renaming of type A_T for convenience, for example. Thus, you cannot say that Ada sub-types are dependent types.

Upvotes: 1

Jacob Sparre Andersen
Jacob Sparre Andersen

Reputation: 6611

No, not as I read the formal definition of dependent types you referenced.

Upvotes: 1

Related Questions