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
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
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
