Do you have a preferred (favorite) implementation of dependent types? Quickly scanning the list on wiki... Ada is the only imperative language listed. Corecur

Do you have a preferred (favorite) implementation of dependent types? Quickly scanning the list on wiki... Ada is the only imperative language listed. Corecursive has had a few episodes about dependent types. Here's two: https://corecursive.com/015-dependant-types-in-haskell-with-stephanie-weirich/ https://corecursive.com/015-dependant-types-in-haskell-with-... https://corecursive.com/023-little-typer-and-pie-language/ https://corecursive.com/023-little-typer-and-pie-language/ Learning more is on my to do list. To noob me, the descriptions remind me of Eiffel's constraints (asserts, pre/post-conditions). And maybe user defined typedefs, like constraining dayOfWeek to values 0..6, a bit like enums.