it&#x27;s nice for the haskell folks that they&#x27;ll be getting some sort of dependent types, but suffice it to say that they will be of a very different sort than the Idris ones.<p>Not to mention, there is hope of giving a semantics to Idris since it is based on a fairly routine variant of type theory, whereas I don&#x27;t think there is any hope at all of understanding &quot;which&quot; type theory the Haskell folks shall have implemented.