Software development topics I've changed my mind on

> 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.

Maybe the author meant gradual static typing?

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)

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.

I recommend https://open.library.ubc.ca/soa/cIRcle/collections/ubctheses... as a place to start.

It isn't about "guaranteeing" _everything_, any more than assertions or guard clauses guarantee everything. It is about giving programmers a semantic tool they can use to communicate expected interfaces in an automatically-detected way, without adding unnecessary toil and boilerplate in tight, local contexts where functions are just working on obvious primitives.

The most graceful implementation I've seen is RDoc comments + Jetbrains tooling in Ruby. When it looks like a type system people assume it's going to work like Java, but having build-time checks based on where people bothered to describe the expected interface catches errors without any of the downsides of type systems that keep type systems from measurably boosting productivity.