Maybe with shelter-in-place I'll have time to write it. :) > I'm curious, are there languages that in your opinion support dependent typing well enough to allo

Maybe with shelter-in-place I'll have time to write it. :) > I'm curious, are there languages that in your opinion support dependent typing well enough to allow all the concepts that you are describing? Most of my experience with dependent types comes from a language called Coq (as well as one of my side projects, which is a new dependently typed language). Agda and Idris (among others) also support this style of programming. Idris goes further and uses dependent types to provide amazing IDE capabilities. There's a YouTube video where the designer of Idris used his IDE to automatically implement matrix transposition (the type was so precise that the compiler discovered the only sensible implementation). Unfortunately I think the world is still lacking a good general-purpose dependently typed programming language suitable for production use (though I'm working on it). > Also, does support of dependent types suggest, imply, or require a particular paradigm (function, imperative, procedural, declarative, etc) or is that an orthogonal concern? Generally speaking, dependently typed languages are functional. The fundamental concept in dependently typed languages is the dependent function type, also called "pi type" or (confusingly) "dependent product type". So, the whole thing is based on functions and their types. One could imagine some kind of hybrid language, but combining dependent types and implicit side effects (like imperative languages have) is an active area of research.