I’ve seen a bit of chatter recently in the PS community about dependent types. Many of us that have been using PureScript for years love it because of its simplicity and elegance, and there has been resistance in the community to build out the complexity, both syntax-wise and implementation-wise, of a full-blown dependently-typed language à la Idris and Agda.

But another reason that there’s not much community momentum behind adding dependent types to PureScript is because PureScript already has dependent types 😁