I love Shen and highly recommend the Book of Shen and Tarver's other book on Logic and Computation.

The crazy thing about Shen is that its type system is sequent calculus, which means when you define your types, you are literally writing the same language that mathematicians use when they prove things about type theories.

Why would you use it? Because you can leverage a crazy amount of power by writing your own type theories in your programs.

Is it practical in today's corporate world? Probably not, but there is at least one case study in the real world https://www.youtube.com/watch?v=lMcRBdSdO_U