Hi
Of course, you can already have these checks without any effort at all, using Catch: http://www-users.cs.york.ac.uk/~ndm/catch/
But then you'd also have to restrict yourself to Haskell 98, right? Or at least to a subset of ghc's extensions.
The Catch tool, as currently implemented, works with Yhc's Core language. Currently you can only generate Yhc's Core language with Yhc. Therefore, currently, the Catch implementation is restricted to Haskell 98 (plus pattern guards). The theory and implementation of Catch are unrestricted, and will cope with all of GHC's extensions including type families, GADT's, MPTC's + FD's, implicit parameters, rank-n types, linear implicit parameters, unboxed types - a slightly larger range of things than GHC's backend code generator can deal with :-) There is a converter from GHC Core to Yhc Core, but GHC's external Core is a bit too flakey/unfinished/in progress to have things work just yet, perhaps once 6.10 is out...
It's not nearly as nice as a solution in the type checker, since it relies on every user of the library running an extra tool if they want a safe interface.
True. But its 0 lines of code, rather than type class hackery - you pay a lot less, you get very slightly less. You can always alias ghc to ghc && catch.
Also, it does nothing to eliminate the actual (admittedly trivial) runtime cost of the use of the Maybe type.
Use a supercompiler, which typically eliminates most things: http://www-users.cs.york.ac.uk/~ndm/supero/ - everything I wrote about Catch and Haskell 98 applies in exactly the same way to Supero. Plus remember that this command will always spawn a process - I think we could put a simple fib generator in there and it still wouldn't make a difference.
Actually, though, now that I think about this, I'm curious... does this mean you intend to teach Catch about this particular interface? Or is it able to sneak into the source code of the library in order to infer that as long as we pass CreatePipe for stdin, the first element of the tuple will be a Just? I suppose it must.
It will almost certainly be able to infer the relationship between the input and output from the implementation. You could of course make createProcess a primitive, in which case you could tell Catch this information.
Which illustrates another advantage of a type-level solution: it allows programmers to infer the behavior of the function from its type, rather than requiring them to look at either its documentation or its implementation (both of which have significant disadvantages... e.g. either of them might not correctly describe all past and future versions of the library, while it's usually a safe assumption that a type-level constraint will lead to a type-check error on any version of the library that fails to satisfy said constraint).
Catch can generate documentation which is precise, and can check annotations. Your point about type signature being a stronger guarantee that is less likely to be broken in the future is completely valid. I'm not recommending we scrap the type system and embrace Catch instead. I'm just suggesting that sometimes instead of hacking the type system in ways that makes peoples heads hurt, there may be an alternative* :-) Thanks Neil * Disclaimer: Alternative may be limited to Haskell 98. Alternative may not work as advertised. Alternative may be poorly supported, compared to something as impressive as GHC. Alternative may turn out to be not the right thing in every case.