←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. roguecoder ◴[06 Feb 25 17:19 UTC] No.42964438[source]▶
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.