Re: [Haskell-cafe] Re: Microsoft's Singularity Project and Haskell
David Leimbach schrieb: Haskell's great and all but it does have a few warts when it comes to how much real trust one should put into the type system. Some compromises still exist like unsafePerformIO that you can't detect simply by looking at the types of functions. In order to live up to the hype and the marketing around Haskell, really things like unsafePerformIO should not be allowed at all. I also do not like the ubiquitous use of unsafePerformIO. However I acknowledge that it allows us to implement things in Haskell that would otherwise need a language and compiler extension, e.g. ByteStrings or ST monad. In the Modula-3 Language Report the section about unsafe features is introduced with the quote: There are some cases that no law can be framed to cover. (Aristotle) http://www.cs.purdue.edu/homes/hosking/m3/reference/unsafe.html ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Microsoft's Singularity Project and Haskell
SPJ http://research.microsoft.com/en-us/people/simonpj/default.aspx and probably many others are actually employed at Microsoft research centers. It looks like Microsoft just hasn't been able to find a suitable spot to push Haskell. Haskell influenced F# because they needed a functional language that targeted CLR, and included OO and mutable data. IMO Haskell is even better than their languages Maybe so but singularity actually provides the whole os apis via clr interfaces compared to mainstream windows os where the underlying apis are all in C, C++ and COM. The common intermediate language is not tied to any specific programming language such as C# or VB, it's more generic than that, and has it's advantages. Safety is something they wish to achieve but afaik their main goal is to write an OS in managed code. Haskell does provide a safe runtime but afaik unlike the clr it's tied to the haskell language. I think there has also been some attempts to write an OS in haskell too though, but that's another story... ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Microsoft's Singularity Project and Haskell
I guess that the house OShttp://www.google.com/search?hl=ensafe=offq=+house+OS+haskellaq=faqi=g-sx7aql=oq=gs_rfai=has no one of these problems that singularity tries to solve in the first place. The problem of general OSs is: we have unsafe code, so what we do to deal with it?. The usual option is the isolation trough virtual addresses so that every pointer address is virtual. This imposes cost in task switching and pointer handling. The singularity alternative seems to be to check the managed code for pointer violations at installation time. In singularity they pretend to extend the reach of types, defined in .NET at the assembly level for inter program and inter language safety, to the OS level for runtime safety. This goal is interesting, because a well defined type system, without unsafe operations permitted, managed at the OS level could permit pure code to run wildly in real memory very fast, for example. With effects defined in the type system the advantages may be greater. 2010/7/31 Tim Matthews tim.matthe...@gmail.com SPJ http://research.microsoft.com/en-us/people/simonpj/default.aspx and probably many others are actually employed at Microsoft research centers. It looks like Microsoft just hasn't been able to find a suitable spot to push Haskell. Haskell influenced F# because they needed a functional language that targeted CLR, and included OO and mutable data. IMO Haskell is even better than their languages Maybe so but singularity actually provides the whole os apis via clr interfaces compared to mainstream windows os where the underlying apis are all in C, C++ and COM. The common intermediate language is not tied to any specific programming language such as C# or VB, it's more generic than that, and has it's advantages. Safety is something they wish to achieve but afaik their main goal is to write an OS in managed code. Haskell does provide a safe runtime but afaik unlike the clr it's tied to the haskell language. I think there has also been some attempts to write an OS in haskell too though, but that's another story... ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Microsoft's Singularity Project and Haskell
Haskell's great and all but it does have a few warts when it comes to how much real trust one should put into the type system. Some compromises still exist like unsafePerformIO that you can't detect simply by looking at the types of functions. In order to live up to the hype and the marketing around Haskell, really things like unsafePerformIO should not be allowed at all. The type of unsafePerformIO $ fireTheMissles return 3 ::Int is just Int after all. Does Singularity also have such back doors? Dave On Sat, Jul 31, 2010 at 6:53 AM, Alberto G. Corona agocor...@gmail.comwrote: I guess that the house OShttp://www.google.com/search?hl=ensafe=offq=+house+OS+haskellaq=faqi=g-sx7aql=oq=gs_rfai=has no one of these problems that singularity tries to solve in the first place. The problem of general OSs is: we have unsafe code, so what we do to deal with it?. The usual option is the isolation trough virtual addresses so that every pointer address is virtual. This imposes cost in task switching and pointer handling. The singularity alternative seems to be to check the managed code for pointer violations at installation time. In singularity they pretend to extend the reach of types, defined in .NET at the assembly level for inter program and inter language safety, to the OS level for runtime safety. This goal is interesting, because a well defined type system, without unsafe operations permitted, managed at the OS level could permit pure code to run wildly in real memory very fast, for example. With effects defined in the type system the advantages may be greater. 2010/7/31 Tim Matthews tim.matthe...@gmail.com SPJ http://research.microsoft.com/en-us/people/simonpj/default.aspx and probably many others are actually employed at Microsoft research centers. It looks like Microsoft just hasn't been able to find a suitable spot to push Haskell. Haskell influenced F# because they needed a functional language that targeted CLR, and included OO and mutable data. IMO Haskell is even better than their languages Maybe so but singularity actually provides the whole os apis via clr interfaces compared to mainstream windows os where the underlying apis are all in C, C++ and COM. The common intermediate language is not tied to any specific programming language such as C# or VB, it's more generic than that, and has it's advantages. Safety is something they wish to achieve but afaik their main goal is to write an OS in managed code. Haskell does provide a safe runtime but afaik unlike the clr it's tied to the haskell language. I think there has also been some attempts to write an OS in haskell too though, but that's another story... ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Microsoft's Singularity Project and Haskell
2010/7/31 David Leimbach leim...@gmail.com: Haskell's great and all but it does have a few warts when it comes to how much real trust one should put into the type system. Some compromises still exist like unsafePerformIO that you can't detect simply by looking at the types of functions. Okay, you should look into modules' imports. This worked well for Ada (as far as I can remember - but I didn't program, i just read a book;) and wasn't concern back then and isn't now. In order to live up to the hype and the marketing around Haskell, really things like unsafePerformIO should not be allowed at all. You can use Haskell to generate quite safe code and that generator will use much of haskell type system while not suffering from unsafePerformIO. The type of unsafePerformIO $ fireTheMissles return 3 ::Int is just Int after all. Does Singularity also have such back doors? This is what new Microsoft OS Barrelfish does: http://www.barrelfish.org/fof_plos09.pdf ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Microsoft's Singularity Project and Haskell
David Leimbach wrote: Haskell's great and all but it does have a few warts when it comes to how much real trust one should put into the type system. Some compromises still exist like unsafePerformIO that you can't detect simply by looking at the types of functions. In order to live up to the hype and the marketing around Haskell, really things like unsafePerformIO should not be allowed at all. As I mentioned in the thread about escaping monads, you actually have a proof obligation in order to use unsafePerformIO. The only problem is that those obligations are not captured in the source language itself, so you must trust the code you link against, separately from any trust induced by type checking. There are very real reasons for wanting a function that can take an IO A into A, which is why unsafePerformIO was added in the FFI addendum. The only way to correct this situation is to (a) add a proof theory to the Haskell language, a la dependent types; or, (b) to break apart the IO sin bin so that we can track the more innocuous parts independently from launching missiles. Of course, the second approach also requires proof that information from the, e.g., RTS monad does not leak into the return value of runRTS. To do this in general without loosing the power we want from RTS, we'll need to add a proof theory to the language in order to demonstrate that two functions are extensionally equal. So really, the first option is the only one; in which case you might as well switch to Agda or the like. -- Live well, ~wren ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Microsoft's Singularity Project and Haskell
On Sat, Jul 31, 2010 at 5:23 PM, David Leimbach leim...@gmail.com wrote: Does Singularity also have such back doors? The CLR doesn't load machine code, it loads bytecodes. So it is possible to statically analyse the module and see hmmm, this module uses unsafePerformIO, I'll reject it. If the bytecode is ok, only then it is JITed into efficient machine code. And note that we wouldn't need unsafePerformIO for the FFI if all programs were made in Haskell ;). Cheers, -- Felipe. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Microsoft's Singularity Project and Haskell
And note that we wouldn't need unsafePerformIO for the FFI if all programs were made in Haskell ;). Perhaps that's true, though entirely unrealistic, in the application world. In the OS world you need access to machine registers and special instructions (CR3 anyone? CP15?) which isn't built into any language save assembly - for these FFI will always come in handy. Also, Haskell continues to have an unfortunate lack of primitives suitable for casting types (ex: zero copy form a bytestring like entity to Word32s). In this realm FFI can outperform cleaner looking code that must rely on individual byte reads. Cheers, Thomas ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Microsoft's Singularity Project and Haskell
Thomas DuBuisson wrote: And note that we wouldn't need unsafePerformIO for the FFI if all programs were made in Haskell ;). Perhaps that's true, though entirely unrealistic, in the application world. In the OS world you need access to machine registers and special instructions (CR3 anyone? CP15?) which isn't built into any language save assembly - for these FFI will always come in handy. Also, Haskell continues to have an unfortunate lack of primitives suitable for casting types (ex: zero copy form a bytestring like entity to Word32s). In this realm FFI can outperform cleaner looking code that must rely on individual byte reads. The FFI doesn't always require unsafePerformIO, it's just there for those cases where the foreign function is truly side-effecting (and therefore should be linked to with the type (...-IO A)) but we know it's safe/referentially-transparent to ignore those effects at some call site. You can link to foreign code without giving it an IO type. The zero-copy version of converting bytestrings is one example where the foreign function is pure, and therefore doesn't need to be linked to as IO. -- Live well, ~wren ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Microsoft's Singularity Project and Haskell
On Sat, Jul 31, 2010 at 8:27 PM, wren ng thornton w...@freegeek.org wrote: Thomas DuBuisson wrote: And note that we wouldn't need unsafePerformIO for the FFI if all programs were made in Haskell ;). Perhaps that's true, though entirely unrealistic, in the application world. In the OS world you need access to machine registers and special instructions (CR3 anyone? CP15?) which isn't built into any language save assembly - for these FFI will always come in handy. Also, Haskell continues to have an unfortunate lack of primitives suitable for casting types (ex: zero copy form a bytestring like entity to Word32s). In this realm FFI can outperform cleaner looking code that must rely on individual byte reads. The FFI doesn't always require unsafePerformIO, True. I mis-read the previous e-mail as we wouldn't need unsafePerformIO OR (vs for) the FFI so please ignore that response to a non-existent statement! ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Microsoft's Singularity Project and Haskell
Probably a more poignant question would be a comparison of Haskell's type system and Sing#'s (http://en.wikipedia.org/wiki/Sing_sharp). Vasili On Fri, Jul 30, 2010 at 5:19 PM, Vasili I. Galchin vigalc...@gmail.comwrote: Hello, In the latest ACM CACM is a paper on Singularity. Here also is an overview: http://lambda-the-ultimate.org/node/1081. I haven't finished the CACM paper yet but I only mention of languages like C# and F#. Singularity is predicated around providing a safe environment. IMO Haskell is even better than their languages. My $.02. Regards, Vasili ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
