Re:Idris 2: Quantitative Type Theory in Practice
by Mehdi2277 on Sunday January 23, 2022 @09:44PM
(#30053117)
The difference is your keys are types. Dependent types are about generics where the keys are allowed to be values. You can not in Java directly do,
Optional<1> and Optional<“Name”>. You can only have types as arguments.
C++ has some dependent types in it allows you to have generic arguments be ints std::array<…, 4> but it still does not allow most values as generic type argument.
Optional<1> and Optional<“Name”>. You can only have types as arguments.
C++ has some dependent types in it allows you to have generic arguments be ints std::array<…, 4> but it still does not allow most values as generic type argument.