私はAdaの周りを頭で囲んでいましたが、私はAgdaとIdrisで少しだけdependent typesを読んできました。Adaサブタイプは依存型と同等であると主張できますか?
Adaのsubtypesは従属型と同等であると主張できますか?
私はAdaの周りを頭で囲んでいましたが、私はAgdaとIdrisで少しだけdependent typesを読んできました。Adaサブタイプは依存型と同等であると主張できますか?
Adaのsubtypesは従属型と同等であると主張できますか?
いいえ、あなたが参照した従属型の正式な定義を読んでいません。
次の例を考えてみましょう:それはそれに制限を課すものではないので、
type A_T is range 1 .. 50;
subtype B_T is A_T;
Sub_type B_T
は、実際にはタイプA_T
として、「同じ」です。たとえば、便宜上、タイプA_T
の名前の変更です。したがって、Adaサブタイプは従属型であるとは言えません。
コンピュータサイエンスとロジックでは、従属型はその値が値に依存する型です。 「整数の対」はタイプです。 「第2の値が第1より大きい整数の対」は、値に依存するため依存型です。
それでは、あなたは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;
参照を実装するためにサブタイプを使用することができます[*§3.2型およびサブタイプ:ノート*](http://www.ada-auth.org/standards/ 12rm/html/RM-3-2.html#p10)を参照してください。 – trashgod
あなたの引用の最初の文にあるように、 '従属型は値に依存する型です'ではありません。基本型は値ではありません。 – EJP