←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.212s | 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. crvdgc ◴[05 Feb 25 21:50 UTC] No.42955735[source]▶
Imagine adding types to a legacy JavaScript codebase. You can turn everything to valid TypeScript by annotating `any` everywhere, then you can gradually add types here and there.

Or imagine writing Rust with `Rc` everywhere and then using the borrowing style on the hot path.

I can see where the author is coming from, but sadly a difficulty is that dependently typed languages often require the programmer to prove type equality during type checking. It's hard to do if the information is not complete.