Idris 2: Quantitative Type Theory in Practice

Re:Idris 2: Quantitative Type Theory in Practice by jhhh on Sunday January 23, 2022 @09:22PM (#30052945)

I could be missing something but my example does as well since it's a method level generic:

  Name nameKey = ...;
  Age ageKey = ...;
  
  Optional<String> name = db.get(nameKey);
  Optional<Integer> age = db.get(ageKey);

[ Parent | on HN ]

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.

[ Parent | on HN ]