Re: "Dependent Types"

In Python, PyContracts supports runtime type-checking and value constraints/assertions (as @contract decorators, annotations, and docstrings).

https://andreacensi.github.io/contracts/

Unfortunately, there's yet no unifying syntax between PyContracts and the newer python type annotations which MyPy checks at compile-type.

https://github.com/python/typeshed

What does it mean for types to be "a first class member of" a programming language?