Re:Idris 2 0.6.0 is now available for the JVM
by quchen on Monday February 27, 2023 @06:02AM
(#34955082)
Isn’t it contradictory to say it’s the most frequent usage, and in the next sentence that no modern programming language does it?
[ Parent
| on HN ]
Re:Idris 2 0.6.0 is now available for the JVM
by kelipso on Monday February 27, 2023 @12:20PM
(#34959140)
No modern PL explicitly allows for it or type checks for it. Examples are enum types and null pointers, which are used everywhere. Implicit usage includes things like natural numbers (ints more than 0), ranges, values of a type following some rule, etc.