Re: [Haskell-cafe] Re: Semantics of uniqueness types for IO (Was: Why can't Haskell be faster?)
On Nov 2, 2007, at 6:35 , apfelmus wrote: during function evaluation. Then, we'd need a purity lemma that states that any function not involving the type *World as in- and output is indeed pure, which may be a bit tricky to prove in the presence of higher-order functions and polymorphism. I mean, the function arrows are tagged for side effects in a strange way, namely by looking like *World - ... - (*World, ...). I don't quite see that; the Clean way looks rather suspiciously like my unwrapped I/O in GHC example from a couple weeks ago, so I have trouble seeing where any difficulty involving functions not using *World / RealWorld# creeps in. I will grant that hiding *World / RealWorld# inside IO is cleaner from a practical standpoint, though. Just not from a semantic one. -- brandon s. allbery [solaris,freebsd,perl,pugs,haskell] [EMAIL PROTECTED] system administrator [openafs,heimdal,too many hats] [EMAIL PROTECTED] electrical and computer engineering, carnegie mellon universityKF8NH ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Semantics of uniqueness types for IO (Was: Why can't Haskell be faster?)
On Fri, 2007-11-02 at 08:35 -0400, Brandon S. Allbery KF8NH wrote: On Nov 2, 2007, at 6:35 , apfelmus wrote: during function evaluation. Then, we'd need a purity lemma that states that any function not involving the type *World as in- and output is indeed pure, which may be a bit tricky to prove in the presence of higher-order functions and polymorphism. I mean, the function arrows are tagged for side effects in a strange way, namely by looking like *World - ... - (*World, ...). I don't quite see that; the Clean way looks rather suspiciously like my unwrapped I/O in GHC example from a couple weeks ago, so I have trouble seeing where any difficulty involving functions not using *World / RealWorld# creeps in. I will grant that hiding *World / RealWorld# inside IO is cleaner from a practical standpoint, though. Just not from a semantic one. On the contrary. GHC's IO newtype isn't an implementation of IO in Haskell at all. It's an implementation in a language that has a Haskell-compatible subset, but that also has semantically bad constructs like unsafePerformIO and unsafeInterleaveIO that give side effects to operations of pure, non-RealWorld#-involving types. Clean's type system is specified in a way that eliminates both functions from the language, which recovers purity. But proving that is harder than I'd like to attempt. jcc ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Semantics of uniqueness types for IO (Was: Why can't Haskell be faster?)
Brandon S. Allbery KF8NH wrote: apfelmus wrote: during function evaluation. Then, we'd need a purity lemma that states that any function not involving the type *World as in- and output is indeed pure, which may be a bit tricky to prove in the presence of higher-order functions and polymorphism. I mean, the function arrows are tagged for side effects in a strange way, namely by looking like *World - ... - (*World, ...). I don't quite see that; the Clean way looks rather suspiciously like my unwrapped I/O in GHC example from a couple weeks ago, so I have trouble seeing where any difficulty involving functions not using *World / RealWorld# creeps in. I will grant that hiding *World / RealWorld# inside IO is cleaner from a practical standpoint, though. Just not from a semantic one. What do you mean? I mean, in Clean, we may ask the following question: are all functions of type say forall a . Either (a - *World - a) String - [*World] or Either (forall a . a - *World - a) String - Maybe *World pure? In Haskell, the answer to any such question is unconditionally yes (unless you're hacking with unsafePerformIO and GHC internals like RealWorld# of course) even with plenty of appearances of the IO type constructor. But in Clean, functions may perform side effects, that's the only way to explain why the examples loop and loop' aren't the same. Regards, apfelmus ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Semantics of uniqueness types for IO (Was: Why can't Haskell be faster?)
On Nov 2, 2007, at 11:51 , Jonathan Cast wrote: I will grant that hiding *World / RealWorld# inside IO is cleaner from a practical standpoint, though. Just not from a semantic one. On the contrary. GHC's IO newtype isn't an implementation of IO in Haskell at all. It's an implementation in a language that has a Haskell-compatible subset, but that also has semantically bad constructs Differing viewpoints, I guess; from my angle, Clean's uniqueness constraint looks like a hack hidden in the compiler. -- brandon s. allbery [solaris,freebsd,perl,pugs,haskell] [EMAIL PROTECTED] system administrator [openafs,heimdal,too many hats] [EMAIL PROTECTED] electrical and computer engineering, carnegie mellon universityKF8NH ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Semantics of uniqueness types for IO (Was: Why can't Haskell be faster?)
Hello, Just a bit of minor academic nitpicking... Yeah. After all, the uniqueness constraint has a theory with an excellent pedigree (IIUC linear logic, whose proof theory Clean uses here, goes back at least to the 60s, and Wadler proposed linear types for IO before anybody had heard of monads). Linear logic/typing does not quite capture uniqueness types since a term with a unique type can always be copied to become non-unique, but a linear type cannot become unrestricted. As a historical note, the first paper on linear logic was published by Girard in 1987; but the purely linear core of linear logic has (non-commutative) antecedents in a system introduced by Lambek in a 1958 paper titled The Mathematics of Sentence Structure. -Jeff --- This e-mail may contain confidential and/or privileged information. If you are not the intended recipient (or have received this e-mail in error) please notify the sender immediately and destroy this e-mail. Any unauthorized copying, disclosure or distribution of the material in this e-mail is strictly forbidden.___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Semantics of uniqueness types for IO (Was: Why can't Haskell be faster?)
Paul Hudak wrote: loop, loop' :: *World - ((),*World) loop w = loop w loop' w = let (_,w') = print x w in loop' w' both have denotation _|_ but are clearly different in terms of side effects. One can certainly use an operational semantics such as bisimulation, but you don't have to abandon denotational semantics. The trick is to make output part of the final answer. For a conventional imperative language one could define, for example, a (lifted, recursive) domain: Answer = Terminate + (String x Answer) and then define a semantic function meaning, say, such that: meaning loop = _|_ meaning loop' = x, x, ... In other words, loop denotes bottom, whereas loop' denotes the infinite sequence of xs. There would typically also be a symbol to denote proper termination, perhaps . A good read on this stuff is Reynolds book Theories of Programming Languages, where domain constructions such as the above are called resumptions, and can be made to include input as well. In the case of Clean, programs take as input a World and generate a World as output. One of the components of that World would presumably be standard output, and that component's value would be _|_ in the case of loop, and x, x, ... in the case of loop'. Another part of the World might be a file system, a printer, a missile firing, and so on. Presumably loop and loop' would not affect those parts of the World. Ah, so the denotational semantics would be a bit like good old stream-based IO. However, we have to change the semantics of - , there's no way to put the side effects in *World only. I mean, the problem of both loop and loop' is that they never return any world at all, the side effects occur during function evaluation. Then, we'd need a purity lemma that states that any function not involving the type *World as in- and output is indeed pure, which may be a bit tricky to prove in the presence of higher-order functions and polymorphism. I mean, the function arrows are tagged for side effects in a strange way, namely by looking like *World - ... - (*World, ...). In contrast, we can see IO a as an abstract (co-)data type subject to some straightforward operational semantics, no need to mess with the pure - . So, in a sense, the Haskell way is cleaner than the Clean way ;) Regards, apfelmus ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Semantics of uniqueness types for IO (Was: Why can't Haskell be faster?)
On Fri, 2007-11-02 at 11:56 -0400, Brandon S. Allbery KF8NH wrote: On Nov 2, 2007, at 11:51 , Jonathan Cast wrote: I will grant that hiding *World / RealWorld# inside IO is cleaner from a practical standpoint, though. Just not from a semantic one. On the contrary. GHC's IO newtype isn't an implementation of IO in Haskell at all. It's an implementation in a language that has a Haskell-compatible subset, but that also has semantically bad constructs Differing viewpoints, I guess; from my angle, Clean's uniqueness constraint looks like a hack hidden in the compiler. Yeah. After all, the uniqueness constraint has a theory with an excellent pedigree (IIUC linear logic, whose proof theory Clean uses here, goes back at least to the 60s, and Wadler proposed linear types for IO before anybody had heard of monads). It's not some random hack somebody happened to notice would work, any more than existential types are. jcc ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Semantics of uniqueness types for IO (Was: Why can't Haskell be faster?)
On Fri, 2007-11-02 at 15:43 -0400, Jeff Polakow wrote: Hello, Just a bit of minor academic nitpicking... Yeah. After all, the uniqueness constraint has a theory with an excellent pedigree (IIUC linear logic, whose proof theory Clean uses here, goes back at least to the 60s, and Wadler proposed linear types for IO before anybody had heard of monads). Linear logic/typing does not quite capture uniqueness types since a term with a unique type can always be copied to become non-unique, but a linear type cannot become unrestricted. Can I write a Clean program with a function that duplicates World? Clean won't let you duplicate the World. My comment on the mismatch with linear logic is aimed more at general uniqueness type systems (e.g. recent work by de Vries, Plasmeijer, and Abrahamson such as https://www.cs.tcd.ie/~devriese/pub/ifl06-paper.pdf). Sorry for the confusion. Ah. I see. jcc ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
