Untitled attachment

Notices where this attachment appears

1. Embed this notice
   Paul Cantrell (inthehands@hachyderm.io)'s status on Friday, 01-Dec-2023 01:47:12 JST Paul Cantrell

   in reply to

   @penguin42 @edavies @thephd
   The concept you’re reaching toward here is “dependent types:” https://en.wikipedia.org/wiki/Dependent_type

   In short: types can carry logical constraints, e.g. not just “integer” but “integer in a range;” not just “list of T,” but “list of T whose elements are in sorted order.” You can statically verify types like that if and only if you can show the compiler how to •prove• those logical conditions are met — and so…