<div dir="ltr"><div class="gmail_extra"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div class="gmail_extra">Pretty sure it's impossible to allow IO without enabling all of it one way or another. And as soon as you allow *any* IO, you're open to various kinds of failures including segfaults. The only way you will get your type system to prevent that is fully specified dependent typing both in your program *and in the OS level interfaces*. I wish you luck on the latter.</div></div></blockquote><div><br></div><div>I don't agree.  This would seem to imply that type safe / memory safe imperative languages are impossible, and that OCaml/Java/C#/etc are a false promise!</div><div><br></div><div>Which APIs and dangers are you thinking of?  I'm worried about bounds checks on memory access, and the capability of foreign code to poke at arbitrary memory.</div><div><br></div><div>But other APIs like these should be fine:</div><div><ul><li>IORef API</li><li>MVar API<br></li><li>STM API</li><li>File IO API</li></ul><div><br></div></div></div></div></div>