Menu
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?
487
A subtype is a type together with a constraint; a value is said to belong to a subtype of a given type if it belongs to the type and satisfies the constraint; the given type is called the base type of the subtype.
Prominent dependently-typed languages include Coq, Nuprl, Agda, Lean, F*, and Idris. Some of these languages, like Coq and Nuprl, are more oriented toward proving things using propositions as types, and others, like F* and Idris, are more oriented toward writing “normal programs” with strong correctness guarantees.
A dependent type is the label used to indicate that the output's type (i.e. the type of the co-domain) depends on the actual input value/argument passed to the (dependent) function. e.g. F:forall a:A, Y(A) means the input type of F is A and that depending on the specific value of a the output type will be Y(a) .
TypeScript does not provide dependent types, but by combining various features such as unions, literal types and indexed access types we can obtain fairly similar behaviour to a dependent function from the caller point of view.
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;
No, not as I read the formal definition of dependent types you referenced.
29
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With
