←back to thread

Software development topics I've changed my mind on

(chriskiehl.com)
873 points belter | 1 comments | 05 Feb 25 09:50 UTC | HN request time: 0.2s | source
Show context
tasuki ◴[05 Feb 25 16:36 UTC] No.42951022[source]▶
> Gradual, dependently typed languages are the future

What's that?

Idris is dependently typed.

> Gradual typing is a type system that lies inbetween static typing and in dynamic typing. Some variables and expressions may be given types and the correctness of the typing is checked at compile time and some expressions may be left untyped and eventual type errors are reported at runtime.

That sounds miserable. I can't see how one would guarantee anything when types of other things aren't known. And I can't see how to connect that to dependent types either.

replies(4): >>42951116 #>>42954208 #>>42955735 #>>42964438 #
1. beders ◴[05 Feb 25 19:56 UTC] No.42954208[source]▶
I can only assume this comes from an observation that once your product matures, the static types become more apparent and you have a better idea how flexible your data modeling should be.

i.e. we are gradually adding more runtime type-checks to our Clojure codebase. (Runtime check are even more powerful than dependent types)