This is a big part of what DT folks love, although only a part. Essentially the argue that we've already written one great language (supposedly), so why bolt a

This is a big part of what DT folks love, although only a part. Essentially the argue that we've already written one great language (supposedly), so why bolt a weak language atop it? Why not just use the same one twice? Of course, now we need a type language and checker for the type language, a higher order type language, and so on and so forth infinitely. You end up with a rammified hierarchy of types (just like we had back in 1910). So that's all fine and good and doesn't actually require dependent types yet. In this case, Magpie appears to do something called "Type in Type" which is to compress the whole rammified hierarchy into one layer by just asserting that this is the case. It turns out that this is unsound---you can craft ridiculous things like Girard's Paradox to break it---but for "pragmatic" types that's probably not a huge problem. We're already inconsistent because I assume Magpie is Turing complete. In order to get dependent types you need what's called the "dependent function space" which lets you accept an argument and then have the return type "depend" on both the type of the argument and the value of the argument A : Type B : Type -> A -> Type depend : (x : A) -> B A x which I don't think is expressed in Magpie.