With dependent types you can encode any proposition in first-order logic (?). You can indeed define an array type that is necessarily sorted. It won't be pretty but it's possible.

More info here: https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...