You can do something like this with OCaml/SML's module system. And certainly from an abstraction point of view you can do this in any dependently typed languag

You can do something like this with OCaml/SML's module system. And certainly from an abstraction point of view you can do this in any dependently typed language like Idris/Agda/Coq, but these don't have great implementations.