[pyrale]

I guess you could use it to implement an algebra that allows you to build dependent types, but that would be unfit for practical uses.

As a case in point, Haskell has first-class experience for HKTs, and dependent types implementation in haskell is getting hindered by the limits of the language.

[ReleaseCandidat]

For anybody interested in the details, here is the last report of the ongoing implementation of dependent types in GHC: https://discourse.haskell.org/t/ghc-dh-weekly-update-6-2023-...