可以认为Ada子类型等同于依赖类型吗？

Question

我一直在努力理解Ada，最近读了一些关于Agda和Idris中依赖类型的内容。

可以说，在Ada中的子类型相当于依赖类型吗？

- nosefouratyou

---

请参阅§3.2类型和子类型：注释了解更多信息。 - trashgod

不是“依赖类型是其定义取决于值的类型”，正如您引用的第一句话所述。 基本类型不是一个值。 - user207421

Answer 1

在计算机科学和逻辑中，依赖类型是一种定义取决于值的类型。例如，"一对整数"是一个类型。"第二个整数大于第一个整数的一对整数"是一个依赖类型，因为它依赖于值的大小关系。因此，您可以使用子类型来实现它们--。

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

- Shark8

---

但你可以直接将那个谓词放在“Pair”上。 - Jacob Sparre Andersen

@JacobSparreAndersen -- 我已经实现了引用部分：“一对整数”是一种类型和“第二个整数大于第一个整数的一对整数”是一个依赖类型，因为它依赖于值。 - Shark8

@JacobSparreAndersen -- （同时，“type”关键字是根据LRM的“第一个子类型指示符”） - Shark8

Answer 2

考虑以下例子：

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

子类型B_T实际上与类型A_T“相同”，因为它不对其施加任何限制。它更像是类型A_T的重命名，以方便使用。因此，您不能说Ada子类型是依赖类型。

- NeoSer

Answer 3

不，与您提到的依赖类型的正式定义不符。

- Jacob Sparre Andersen