types - 是否可以认为 Ada 子类型等同于依赖类型？

Question

我一直试图围绕 Ada 进行思考，并且我阅读了一些关于 dependent types 的信息。在 Agda 和 idris 。

可以说subtypes在 Ada 中是否等同于依赖类型？

Answer 1

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.

那么你就可以使用子类型来实现它们——

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