I guess this is a thread about staticly dependently gradually typed purely functional monadic programming because just like real communism it exists only as an abstract idea for academics to sperg about and when attempted in practice will either become impure, result in failure or both at the same time.