Re: [Haskell-cafe] [ANNOUNCE] First Public Release of the Snap Framework
Awesome! Congratulations on the first release, I look forward to working with it. Also, the web design is great, possibly the best designed Haskell library website I've seen so far. -chris On 22 mei 2010, at 07:25, Gregory Collins wrote: Hello all, To coincide with Hac Phi 2010 (http://www.haskell.org/haskellwiki/Hac_%CF%86), the Snap team is happy to announce the first public release of the Snap Framework, a simple and fast Haskell web programming server and library for unix systems. For installation instructions, documentation, and more information, see our website at http://snapframework.com/. Snap is well-documented and has a test suite with a high level of code coverage, but it is early-stage software with still-evolving interfaces. Snap is therefore most likely to be of interest to early adopters and potential contributors. Snap is BSD-licensed and currently only runs on Unix platforms; it has been developed and tested on Linux and Mac OSX Snow Leopard. Snap Features: * A simple and clean monad for web programming, similar to happstack's but simpler. * A *fast* HTTP server library with an optional high-concurrency backend (using libev). * An XML-based templating system for generating xhtml that allows you to bind Haskell functionality to XML tags in your templates. * Some useful utilities for web handlers, including gzip compression and fileServe. * Iteratee-based I/O, allowing composable streaming in O(1) space without any of the unpredictable consequences of lazy I/O. If you have questions or comments, please contact us on our mailing list (http://mailman-mail5.webfaction.com/listinfo/snap) or in the #snapframework channel on the freenode IRC network. Cheers, G -- Gregory Collins g...@gregorycollins.net ___ 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] Re: Proof question -- (==) over Bool
On Sat, 2010-05-22 at 00:15 +, R J wrote:
I'm trying to prove that (==) is reflexive, symmetric, and transitive
over the Bools, given this definition:
(==) :: Bool - Bool - Bool
x == y = (x y) || (not x not y)
My question is: are the proofs below for reflexivity and symmetricity
rigorous, and what is the proof of transitivity, which eludes me?
Thanks.
Theorem (reflexivity): For all x `elem` Bool, x == x.
Proof:
x == x
={definition of ==}
(x x) || (not x not x)
={logic (law of the excluded middle)}
True
I'd add additional step:
x == x = (x x) || (not x not x) = x || not x = T
def A A = A A || not A = T
However it depends on your level - the more advanced you are the more
step you can omit.
Theorem (symmetricity): For all x, y `elem` Bool, if x == y, then y
== x.
Proof:
x == y
={definition of ==}
(x y) || (not x not y)
={lemma: () is commutative}
(y x) || (not x not y)
={lemma: () is commutative}
(y x) || (not y not x)
={definition of ==}
y == x
Theorem (transitivity): For all x, y, z `elem` Bool, if x == y, and y
== z,
then x == z.
Proof: ?
For example by cases in Y (assume Y is true and prove it correct and
then assume Y is false and prove it correct. As in logic where there is
law of excluded middle Y have to be true or false it holds). It took
around 7 lines.
Regards
signature.asc
Description: This is a digitally signed message part
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Proof question -- (==) over Bool
R J rj248...@hotmail.com writes: I'm trying to prove that (==) is reflexive, symmetric, and transitive over the Bools, given this definition: (==):: Bool - Bool - Bool x == y = (x y) || (not x not y) Since Bool is a type, and all Haskell types include ⊥, you need to add conditions in your proofs to exclude it. -- Jón Fairbairn jon.fairba...@cl.cam.ac.uk ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] cabal problem on OS X
When I run cabal update on my Mac (Snow Leopard, Intel), I get: % cabal update Downloading the latest package list from hackage.haskell.org cabal: Codec.Compression.Zlib: incompatible zlib version Anyone else seeing this? Reinstalling the Haskell Platform hasn't helped. Thanks! ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] cabal problem on OS X
Bill Atkins watk...@alum.rpi.edu writes: When I run cabal update on my Mac (Snow Leopard, Intel), I get: % cabal update Downloading the latest package list from hackage.haskell.org cabal: Codec.Compression.Zlib: incompatible zlib version I'm going to randomly guess that the version of the C zlib library that Cabal was indirectly built against is different to the one on your machine. -- Ivan Lazar Miljenovic ivan.miljeno...@gmail.com IvanMiljenovic.wordpress.com ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Performance Issue
Richard, I found this very annoying when I first realised GHC doesn't do any CSE, given that the result of pure functions only depend on their parameters. Even though CSE usually sounds good, when you ask, they go and find obscure examples in which it causes great trouble :) I think, there should at least be a compiler flag or something similar to enforce CSE on some structures. But currently, as others pointed out, you need to bind and do your sub expression elimination yourself. Best, On 18 May 2010 17:30, Richard Warburton richard.warbur...@gmail.com wrote: A colleague of mine pointed out that ghc wasn't performing as he expected when optimising some code. I wonder if anyone could offer any insight as to why its not noting this common subexpression: main = print $ newton 4 24 newton a 0 = a newton a n = ((newton a (n-1))^2 + a)/(2*(newton a (n-1))) Compiled with 'ghc -O3 --make perf.hs', results in: real0m5.544s user0m5.492s sys 0m0.008s However if we factor out the repeated call to the newton method: main = print $ newton2 4 24 newton2 a 0 = a newton2 a n = (x^2 + a)/(2*x) where x = newton2 a (n-1) real0m0.004s user0m0.004s sys 0m0.004s It looks to me like Referential transparency should make this a sound optimisation to apply, but ghc isn't doing it even on -O3. regards, Richard ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- Ozgur Akgun ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Performance Issue
Hello, Even though CSE usually sounds good, when you ask, they go and find obscure examples in which it causes great trouble :) Do you (or others) have any particular mean but understandable example? Cheers, Michael ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Performance Issue
Michael Lesniak mlesn...@uni-kassel.de writes: Even though CSE usually sounds good, when you ask, they go and find obscure examples in which it causes great trouble :) Do you (or others) have any particular mean but understandable example? http://www.haskell.org/haskellwiki/GHC:FAQ#Does_GHC_do_common_subexpression_elimination.3F All hail Google! :p -- Ivan Lazar Miljenovic ivan.miljeno...@gmail.com IvanMiljenovic.wordpress.com ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Performance Issue
Hello, http://www.haskell.org/haskellwiki/GHC:FAQ#Does_GHC_do_common_subexpression_elimination.3F All hail Google! :p You're right :D. Thanks! - Michael -- Dipl.-Inf. Michael C. Lesniak University of Kassel Programming Languages / Methodologies Research Group Department of Computer Science and Electrical Engineering Wilhelmshöher Allee 73 34121 Kassel Phone: +49-(0)561-804-6269 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Existentials and SYB [Was: GADTs and Scrap your Boilerplate]
enDataI :: (Int - DataBox) enDataI = DataBox enDataB :: (Bool - DataBox) enDataB = DataBox instance Data DataBox where gfoldl k z (DataBox d) = z DataBox `k` d gunfold k z c = (if True then k (z enDataI) else k (z enDataB)) Interesting solution but I'm not smart enough to see how the solution can be generalized to any data type that's an instance of Data. Do I have to repeat the if then else for every instance of the Data type class (which I can't) or is there some other way? Oscar ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] cabal problem on OS X
I have a different problem (also after doing a cabal update): I get a bus error. I just created this ticket for it: http://hackage.haskell.org/trac/hackage/ticket/691 -chris On 22 mei 2010, at 13:20, Bill Atkins wrote: When I run cabal update on my Mac (Snow Leopard, Intel), I get: % cabal update Downloading the latest package list from hackage.haskell.org cabal: Codec.Compression.Zlib: incompatible zlib version Anyone else seeing this? Reinstalling the Haskell Platform hasn't helped. Thanks! ___ 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] Performance Issue
On Saturday 22 May 2010 15:00:25, Thomas Schilling wrote:
Actually, in this case it would be safe to do CSS. Because
a) the function is strict in both arguments so GHC creates a worker
which only uses unboxed types
b) this cannot cause any space leaks (it contains no pointers)
The generated Core does look pretty weird, though:
$wnewton =
\ (ww_s115 :: Double#) (ww1_s119 :: Int#) -
case ww1_s119 of ds_Xr8 {
__DEFAULT -
case ^_r11D
(case $wnewton ww_s115 (-# ds_Xr8 1)
of ww2_s11d { __DEFAULT -
D# ww2_s11d -- box the result of $wnewton
})
lvl_r11B
of _ { D# x_avk --- unbox it again
The boxing is due to the use of (^).
If you write x*x instead of x^2, it can use the primop *## and needn't box
it.
As a side effect, the original time leak probably wouldn't have occured
with x*x instead of x^2 because one would've made it
let x = newton a (n-1) in (x*x +a) / (2*x)
instead of writing out newton a (n-1) thrice anyway, wouldn't one?
case $wnewton ww_s115 (-# ds_Xr8 1)
of ww2_s11d { __DEFAULT -
/##
(+## x_avk ww_s115) (*## 2.0 ww2_s11d)
}
};
0 - ww_s115
}
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Performance Issue
On Saturday 22 May 2010 16:48:27, Daniel Fischer wrote: The boxing is due to the use of (^). If you write x*x instead of x^2, it can use the primop *## and needn't box it. As a side effect, the original time leak probably wouldn't have occured with x*x instead of x^2 because one would've made it let x = newton a (n-1) in (x*x +a) / (2*x) instead of writing out newton a (n-1) thrice anyway, wouldn't one? Even if. With newton :: Double - Int - Double newton a 0 = a newton a n = (((newton a (n-1)) * (newton a (n-1)) ) + a)/(2*(newton a (n-1))) (and optimisations of course), GHC does share newton a (n-1). Lesson: Writing x^2 is a baad thing. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Performance Issue
On May 22, 2010, at 08:30 , Ozgur Akgun wrote: Even though CSE usually sounds good, when you ask, they go and find obscure examples in which it causes great trouble :) They're not actually that obscure. Most of them can be summarized thusly: anything that would cause a fold to cause a stack or heap overflow if you get the strictness wrong is likely to cause the same problems if CSE optimizes it, for much the same reason. And, worse, if you have CSE, the only way to avoid this would be to disable it; the current situation at least permits you to manually perform CSE via let-binding. (In particular, it's often impossible to manipulate strictness; consider computing an average over a list as sum / length (obscure?): the only way to avoid a large list exploding in memory usage is to pull apart sum and length and thread them together, *no* strictness annotation will help.) -- brandon s. allbery [solaris,freebsd,perl,pugs,haskell] allb...@kf8nh.com system administrator [openafs,heimdal,too many hats] allb...@ece.cmu.edu electrical and computer engineering, carnegie mellon universityKF8NH PGP.sig Description: This is a digitally signed message part ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Proof question -- (==) over Bool
On May 22, 2010, at 1:32 AM, Jon Fairbairn wrote: Since Bool is a type, and all Haskell types include ⊥, you need to add conditions in your proofs to exclude it. Not really. Bottom isn't a value, so much as an expression for computations that don't refer to real values. It's close enough to be treated as a value in many contexts, but this isn't one of them. Proof by pattern matching (i.e., proof by truth table) is sufficient to ensure that bottom (as a value) isn't included. After all, the Bool type is enumerable. At least in principle. So perhaps the constructive Haskell proof would go something like: -- Claim to prove transitivity :: Bool - Bool - Bool - Bool transitivity x y z = if (x == y) (y z) then x == z else True -- The proof unifier :: Bool unifier = all (True ==) $ [ transitivity x y z | x - [ True, False ] , y - [ True, False ] , z - [ True, False ] ] This includes some syntactic sugar R J might not be entitled to, but the intent is pretty clear. We are programmatically validating that every assignment of truth values to the sentence if (x == y) (y z) then x == z is true. (The theorem is vacuously true for assignments where the antecedent of the conditional is false)___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Performance Issue
On 22 May 2010 16:06, Daniel Fischer daniel.is.fisc...@web.de wrote: On Saturday 22 May 2010 16:48:27, Daniel Fischer wrote: The boxing is due to the use of (^). If you write x*x instead of x^2, it can use the primop *## and needn't box it. As a side effect, the original time leak probably wouldn't have occured with x*x instead of x^2 because one would've made it let x = newton a (n-1) in (x*x +a) / (2*x) instead of writing out newton a (n-1) thrice anyway, wouldn't one? Even if. With newton :: Double - Int - Double newton a 0 = a newton a n = (((newton a (n-1)) * (newton a (n-1)) ) + a)/(2*(newton a (n-1))) (and optimisations of course), GHC does share newton a (n-1). Lesson: Writing x^2 is a baad thing. Interesting. Clearly GHC needs a better partial evaluator! :) (^) is not inlined because it's recursive (or rather it's worker is) and there also is no SPECIALISE pragma for Double - Integer - Double. Yes, it's Integer, not Int, because the literal 2 defaults to Integer. It doesn't seem to be possible to add SPECIALISE pragmas for non-local functions. If I copy over the definition of (^) no pragma is needed. GHC creates an worker for Double# - Integer - Double# and that seems to be sufficient to make CSE work. -- Push the envelope. Watch it bend. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Proof question -- (==) over Bool
Note that all (True ==) is logically equivalent to all id and to the and function from the prelude. A more general approach based on type classes, the function taut takes a boolean function and determines (by exhaustive search) if it is a tautology: class BooleanFunction a where taut :: a - Bool instance BooleanFunction Bool where taut = id instance (Bounded a,Enum a, BooleanFunction b) = BooleanFunction (a - b) where taut f = and $ map (taut . f) $ enumFrom minBound unifier = taut transitivity On 22 May 2010 19:37, Alexander Solla a...@2piix.com wrote: On May 22, 2010, at 1:32 AM, Jon Fairbairn wrote: Since Bool is a type, and all Haskell types include ⊥, you need to add conditions in your proofs to exclude it. Not really. Bottom isn't a value, so much as an expression for computations that don't refer to real values. It's close enough to be treated as a value in many contexts, but this isn't one of them. Proof by pattern matching (i.e., proof by truth table) is sufficient to ensure that bottom (as a value) isn't included. After all, the Bool type is enumerable. At least in principle. So perhaps the constructive Haskell proof would go something like: -- Claim to prove transitivity :: Bool - Bool - Bool - Bool transitivity x y z = if (x == y) (y z) then x == z else True -- The proof unifier :: Bool unifier = all (True ==) $ [ transitivity x y z | x - [ True, False ] , y - [ True, False ] , z - [ True, False ] ] This includes some syntactic sugar R J might not be entitled to, but the intent is pretty clear. We are programmatically validating that every assignment of truth values to the sentence if (x == y) (y z) then x == z is true. (The theorem is vacuously true for assignments where the antecedent of the conditional is false) ___ 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] [ANNOUNCE] First Public Release of the Snap Framework
Congratulations on the release. I was interested in seeing how this would work as a WAI handler, and came across some questions: * I noticed that the Method datatype is restricted to a set of specific methods. Seeing as the list of methods can be expanded[1], why was this chosen? * The CIByteString datatype provides no way of accessing directly the lower-case version of the bytestring, or of setting it. Seeing as WAI already lower-cases the headers (following your suggestion btw) it would be more efficient to only do this once. Would you consider exposing the constructor? * For simplicity at the moment, I decided to use the getRequestBody function, but it seems to be returning an empty result. Is there a known gotcha here? Overall, writing the WAI wrapper is pretty straight-forward. The main problem is that the WAI request body does not require an inversion of control approach, while the Snap version does; some usage of lazy I/O here could solve the problem, though that's obviously sub-optimal. Also, it seems a little unclear whether the writeBS et al functions store the body in memory before returning the result, though the documentation implies it. Could you provide some clarifications? Good work, Michael [1] http://www.w3.org/Protocols/rfc2616/rfc2616-sec9.html http://www.w3.org/Protocols/rfc2616/rfc2616-sec9.html On Sat, May 22, 2010 at 8:25 AM, Gregory Collins g...@gregorycollins.netwrote: Hello all, To coincide with Hac Phi 2010 (http://www.haskell.org/haskellwiki/Hac_%CF%86), the Snap team is happy to announce the first public release of the Snap Framework, a simple and fast Haskell web programming server and library for unix systems. For installation instructions, documentation, and more information, see our website at http://snapframework.com/. Snap is well-documented and has a test suite with a high level of code coverage, but it is early-stage software with still-evolving interfaces. Snap is therefore most likely to be of interest to early adopters and potential contributors. Snap is BSD-licensed and currently only runs on Unix platforms; it has been developed and tested on Linux and Mac OSX Snow Leopard. Snap Features: * A simple and clean monad for web programming, similar to happstack's but simpler. * A *fast* HTTP server library with an optional high-concurrency backend (using libev). * An XML-based templating system for generating xhtml that allows you to bind Haskell functionality to XML tags in your templates. * Some useful utilities for web handlers, including gzip compression and fileServe. * Iteratee-based I/O, allowing composable streaming in O(1) space without any of the unpredictable consequences of lazy I/O. If you have questions or comments, please contact us on our mailing list (http://mailman-mail5.webfaction.com/listinfo/snap) or in the #snapframework channel on the freenode IRC network. Cheers, G -- Gregory Collins g...@gregorycollins.net ___ 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] [ANNOUNCE] First Public Release of the Snap Framework
Michael Snoyman mich...@snoyman.com writes: Congratulations on the release. I was interested in seeing how this would work as a WAI handler, and came across some questions: * I noticed that the Method datatype is restricted to a set of specific methods. Seeing as the list of methods can be expanded[1], why was this chosen? The answer is no particular reason -- nobody really uses this. I think you're right that this makes us technically out of spec, if it becomes an issue for anyone we'll add a custom constructor later. * The CIByteString datatype provides no way of accessing directly the lower-case version of the bytestring, or of setting it. Seeing as WAI already lower-cases the headers (following your suggestion btw) it would be more efficient to only do this once. Would you consider exposing the constructor? Would you accept: ciToLower :: CIByteString - ByteString instead? I prefer opaque datatypes in general. We didn't see a need for that use-case, the idea was that the string representation would be the same but we would do a case-insensitive compare. * For simplicity at the moment, I decided to use the getRequestBody function, but it seems to be returning an empty result. Is there a known gotcha here? If the POST body has content-type application/x-www-form-urlencoded we parse it for you and put the fields in the parameter mapping. If this isn't your case I'd appreciate a bug report. This is a place where we made a different design decision than you did -- a WAI application which expects to parse the POST body itself won't work. I'll think about adding a knob to make this behaviour optional. Overall, writing the WAI wrapper is pretty straight-forward. The main problem is that the WAI request body does not require an inversion of control approach, while the Snap version does; some usage of lazy I/O here could solve the problem, though that's obviously sub-optimal. A Chan a forkIO could work here also (we've discussed that one before I think.) Also, it seems a little unclear whether the writeBS et al functions store the body in memory before returning the result, though the documentation implies it. Could you provide some clarifications? The Snap monad carries a Response in its state, with rspBody being an output Enumerator. The writeBS function composes enumBS foo with the Enumerator from that state; so when you call writeBS you're really building up a *program* to send the response body out later. So yes, we hang onto that data until the request is served. If you want to stream in O(1) space you need to provide an Enumerator to do so; the Enumerator has access to the IO monad though. We provide writeBS/writeLBS for those situations in which it's convenient/appropriate to build up the entire response in memory. G. -- Gregory Collins g...@gregorycollins.net ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] [ANNOUNCE] First Public Release of the Snap Framework
On Sat, May 22, 2010 at 11:15 PM, Gregory Collins g...@gregorycollins.netwrote: Michael Snoyman mich...@snoyman.com writes: Congratulations on the release. I was interested in seeing how this would work as a WAI handler, and came across some questions: * I noticed that the Method datatype is restricted to a set of specific methods. Seeing as the list of methods can be expanded[1], why was this chosen? The answer is no particular reason -- nobody really uses this. I think you're right that this makes us technically out of spec, if it becomes an issue for anyone we'll add a custom constructor later. * The CIByteString datatype provides no way of accessing directly the lower-case version of the bytestring, or of setting it. Seeing as WAI already lower-cases the headers (following your suggestion btw) it would be more efficient to only do this once. Would you consider exposing the constructor? Would you accept: ciToLower :: CIByteString - ByteString instead? I prefer opaque datatypes in general. We didn't see a need for that use-case, the idea was that the string representation would be the same but we would do a case-insensitive compare. Well, that solves half the problem: I also would like to be able to hand in a lower-case version when converting from the WAI ResponseHeader to a CIByteString. * For simplicity at the moment, I decided to use the getRequestBody function, but it seems to be returning an empty result. Is there a known gotcha here? If the POST body has content-type application/x-www-form-urlencoded we parse it for you and put the fields in the parameter mapping. If this isn't your case I'd appreciate a bug report. This is a place where we made a different design decision than you did -- a WAI application which expects to parse the POST body itself won't work. I'll think about adding a knob to make this behaviour optional. I'd appreciate such a knob. Out of curiosity, do you also parse multi-part data? Overall, writing the WAI wrapper is pretty straight-forward. The main problem is that the WAI request body does not require an inversion of control approach, while the Snap version does; some usage of lazy I/O here could solve the problem, though that's obviously sub-optimal. A Chan a forkIO could work here also (we've discussed that one before I think.) You're right; it doesn't actually require the lazy I/O bit, just the forkIO. Not that I'm crazy about that solution either. Also, it seems a little unclear whether the writeBS et al functions store the body in memory before returning the result, though the documentation implies it. Could you provide some clarifications? The Snap monad carries a Response in its state, with rspBody being an output Enumerator. The writeBS function composes enumBS foo with the Enumerator from that state; so when you call writeBS you're really building up a *program* to send the response body out later. So yes, we hang onto that data until the request is served. That's what it looked like to me; maybe you could update the docs to make that clear. I'd hate for people to accidentally kill their performance. If you want to stream in O(1) space you need to provide an Enumerator to do so; the Enumerator has access to the IO monad though. We provide writeBS/writeLBS for those situations in which it's convenient/appropriate to build up the entire response in memory. I figured I'd end up writing that, but I just wanted to test things out the simple way first via writeLBS. I'll have to wait in any event for the ability to bypass automatic request body parsing. Michael ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] [ANNOUNCE] First Public Release of the Snap Framework
Michael Snoyman mich...@snoyman.com writes: Would you accept: ciToLower :: CIByteString - ByteString instead? I prefer opaque datatypes in general. We didn't see a need for that use-case, the idea was that the string representation would be the same but we would do a case-insensitive compare. Well, that solves half the problem: I also would like to be able to hand in a lower-case version when converting from the WAI ResponseHeader to a CIByteString. You can pass a lower-case input, it'll get lowercased again but that isn't such a big price to pay. If the POST body has content-type application/x-www-form-urlencoded we parse it for you and put the fields in the parameter mapping. If this isn't your case I'd appreciate a bug report. This is a place where we made a different design decision than you did -- a WAI application which expects to parse the POST body itself won't work. I'll think about adding a knob to make this behaviour optional. I'd appreciate such a knob. Out of curiosity, do you also parse multi-part data? No, not yet :(, and we'll never do so automatically; we limit POST bodies to 1MB or something like that (to prevent malicious requests from trashing the server) but multipart requests can contain file uploads, which we would probably want to be able to stream to disk somehow. G -- Gregory Collins g...@gregorycollins.net ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ANN: has-0.4 Entity based records
There are many libraries to write function takes an record has Foo and Bar and returns something. But writing type of the function is still difficult. I can't write such types using HList or records without reading documents. I think, using has, There's few effort to write such types. In which manner do you need to read less documentation to write: ] f :: Has Foo r = r - ... Instead when using HList: ] f :: HasField Foo record fieldType = ... HasField only gives projection function (hLookupByLabel), but Has gives projection, injection and modification function. If I want to write a generic function injecting a value into field Foo in a record by HList, I should read documentation more. I think `has' fits the needs of Haskellers who have the good habit of writing a type of a function before its definition. What does this mean exactly in terms of the type inference possible? Probably, yes. it's still fragile due to some reasons e.g. the behavior of UndecidableInstances language extension. import Data.Has data Foo = Foo; type instance TypeOf Foo = Int data Bar = Bar; type instance TypeOf Bar = Int f r = (Foo ^. r) + (Bar ^. r) *Main :t f f :: forall s. (Contains (Labelled Foo Int) s, Contains (Labelled Bar Int) s) = s - TypeOf Foo -nwn ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
RE: [Haskell-cafe] making the GHC Api not write to stderr
I did some more digging around and it would seem that the error was being
printed from the load call (depanal does some parsing ofcourse to find the
imports).
I managed to silence that using loadWithLogger (const $ return ())
LoadAllTargets (maybe all these loggers should be consolidated).
That stopped it from showing part of the error, but can’t figure out what’s
showing the module name at the end. “Printf”
From: Daniel Peebles [mailto:pumpkin...@gmail.com]
Sent: Saturday, May 22, 2010 03:02
To: Phyx
Cc: Thomas Schilling; haskell-cafe@haskell.org
Subject: Re: [Haskell-cafe] making the GHC Api not write to stderr
Have you tried freopen on stderr?
On Fri, May 21, 2010 at 8:43 AM, Phyx loneti...@gmail.com wrote:
Hi,
I tried that, setting it to (\_ _ _ _ - return ()) and it still did the
same, also tried setting it to undefined to see whether the code that's
printing the error is using it, and it didn't crash
So I assume it's not.
---
*VsxParser getModInfo True
C:\\Users\\Phyx\\AppData\\Local\\Temp\\tmp5600.hs
return ()
C:\Users\Phyx\AppData\Local\Temp\tmp5600.hs:11:13:
parse error on input `='
Printf
-
I think parseModule might still have a hardcoded print statement in it.
-Original Message-
From: Thomas Schilling [mailto:nomin...@googlemail.com]
Sent: Friday, May 21, 2010 12:53
To: Phyx
Cc: haskell-cafe@haskell.org
Subject: Re: [Haskell-cafe] making the GHC Api not write to stderr
You could try changing the log_action[1] member of the DynFlags. A while
ago I turned most printed errors into some form of error message, but I
wouldn't be surprised if I missed some places. All output should go through
log_action, though, so try changing that to intercept any output.
[1]:
http://haskell.org/ghc/docs/6.12-latest/html/libraries/ghc-6.12.2/DynFlags.h
http://haskell.org/ghc/docs/6.12-latest/html/libraries/ghc-6.12.2/DynFlags.h%0d%0atml#v%3Alog_action
tml#v%3Alog_action
On 20 May 2010 19:05, Phyx loneti...@gmail.com wrote:
I was wondering how to forcibly quiet down the API. I have a custom
handler in place, but when I call the function on failure both my
handler gets called and somewhere somehow errors get printed to the
stderr, which I really need to avoid.
My current code looks like
getModInfo :: Bool - String - String - IO (ApiResults ModuleInfo)
getModInfo qual file path = handleSourceError processErrors $
runGhc (Just libdir) $ do
dflags - getSessionDynFlags
setSessionDynFlags $ configureDynFlags dflags
target - guessTarget file Nothing
addTarget target
setSessionDynFlags $ dflags { importPaths = [path] }
load LoadAllTargets
graph - depanal [] False
let modifier = moduleName . ms_mod
modName = modifier $ head graph
includes = includePaths dflags
imports = importPaths dflags
dflags' - Debug.trace (moduleNameString modName)
getSessionDynFlags
setSessionDynFlags $ dflags' { includePaths = path:includes
, importPaths = path:imports
}
parsed - parse modName
checked - typecheckModule parsed
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
--
Push the envelope. Watch it bend.
___
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] How to construct a lazy list of eagerly-evaluated items?
I'm using Project Euler to learn Haskell. In particular, I'm writing a program for Problem 18: http://projecteuler.net/index.php?section=problemsid=18. As a solution, I'm constructing a list, containing maximum sums of values on a path from top of the triangle to a given item. In this list, item value equals value of an item from an input list plus maximum of values of the top neighbours, taken from the same list we're constructing. Here's the program: BEGIN CODE triangle18 = [75...etc - definition of the input triangle sqrti n = truncate (sqrt (fromIntegral n)) -- returns true if a number is an exact square isSquare n = n == r * r where r = sqrti n -- returns true if a number is a triangular numberx isTriangular n = isSquare (8 * n + 1) -- returns index of the top-right neighbour prevRight i = i - (sqrti (8 * i + 1) - 1) `div` 2 -- returns index of the top-left neighbour prevLeft i = prevRight i - 1 -- returns the list of top neighbours (at most 2) prev i | i == 0 = [] | isTriangular i = [prevRight i] | isTriangular (i + 1) = [prevLeft i] | otherwise= [prevLeft i, prevRight i] -- returns the list of 'path sums' for a given list of input numbers maxPaths vals@(v:vs) = v : zipWith mpath [1..] vs where mpath i val = val + maximum [(maxPaths vals) !! pi| pi - prev i] result18 = maximum (maxPaths triangle18) END CODE The program works, but consumes obscene amount of memory. I suspect that it's because of lazy evaluation of items in the list we're constructing (and also using during construction). How can I force eager evaluation of items, put into the list? Any other comments and suggestions are also very welcome. I know index-based item lookup in a list is not efficient, but I'll take care of this later (I don't know much about arrays yet). For now, I'm more concerned with the memory usage. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
RE: [Haskell-cafe] making the GHC Api not write to stderr
Right, that modulename was being printed due to a trace statement in my code,
so I’m now using withLocalCallbacks (\_ - GhcApiCallbacks (\_ _ - return ()))
$
To override everything along with setting log_action to (\_ _ _ _ - return
()). Now nothing else gets printed J
Thanks for all the help,
Phyx
I did some more digging around and it would seem that the error was being
printed from the load call (depanal does some parsing ofcourse to find the
imports).
I managed to silence that using loadWithLogger (const $ return ())
LoadAllTargets (maybe all these loggers should be consolidated).
That stopped it from showing part of the error, but can’t figure out what’s
showing the module name at the end. “Printf”
From: Daniel Peebles [mailto:pumpkin...@gmail.com]
Sent: Saturday, May 22, 2010 03:02
To: Phyx
Cc: Thomas Schilling; haskell-cafe@haskell.org
Subject: Re: [Haskell-cafe] making the GHC Api not write to stderr
Have you tried freopen on stderr?
On Fri, May 21, 2010 at 8:43 AM, Phyx loneti...@gmail.com wrote:
Hi,
I tried that, setting it to (\_ _ _ _ - return ()) and it still did the
same, also tried setting it to undefined to see whether the code that's
printing the error is using it, and it didn't crash
So I assume it's not.
---
*VsxParser getModInfo True
C:\\Users\\Phyx\\AppData\\Local\\Temp\\tmp5600.hs
return ()
C:\Users\Phyx\AppData\Local\Temp\tmp5600.hs:11:13:
parse error on input `='
Printf
-
I think parseModule might still have a hardcoded print statement in it.
-Original Message-
From: Thomas Schilling [mailto:nomin...@googlemail.com]
Sent: Friday, May 21, 2010 12:53
To: Phyx
Cc: haskell-cafe@haskell.org
Subject: Re: [Haskell-cafe] making the GHC Api not write to stderr
You could try changing the log_action[1] member of the DynFlags. A while
ago I turned most printed errors into some form of error message, but I
wouldn't be surprised if I missed some places. All output should go through
log_action, though, so try changing that to intercept any output.
[1]:
http://haskell.org/ghc/docs/6.12-latest/html/libraries/ghc-6.12.2/DynFlags.h
http://haskell.org/ghc/docs/6.12-latest/html/libraries/ghc-6.12.2/DynFlags.h%0d%0atml#v%3Alog_action
tml#v%3Alog_action
On 20 May 2010 19:05, Phyx loneti...@gmail.com wrote:
I was wondering how to forcibly quiet down the API. I have a custom
handler in place, but when I call the function on failure both my
handler gets called and somewhere somehow errors get printed to the
stderr, which I really need to avoid.
My current code looks like
getModInfo :: Bool - String - String - IO (ApiResults ModuleInfo)
getModInfo qual file path = handleSourceError processErrors $
runGhc (Just libdir) $ do
dflags - getSessionDynFlags
setSessionDynFlags $ configureDynFlags dflags
target - guessTarget file Nothing
addTarget target
setSessionDynFlags $ dflags { importPaths = [path] }
load LoadAllTargets
graph - depanal [] False
let modifier = moduleName . ms_mod
modName = modifier $ head graph
includes = includePaths dflags
imports = importPaths dflags
dflags' - Debug.trace (moduleNameString modName)
getSessionDynFlags
setSessionDynFlags $ dflags' { includePaths = path:includes
, importPaths = path:imports
}
parsed - parse modName
checked - typecheckModule parsed
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
--
Push the envelope. Watch it bend.
___
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] How to construct a lazy list of eagerly-evaluated items?
On Sunday 23 May 2010 01:10:54, Vladimir Ch. wrote: I'm using Project Euler to learn Haskell. In particular, I'm writing a program for Problem 18: snip The program works, but consumes obscene amount of memory. Not if it's compiled. Even interpreted I wouldn't call it obscene, though it is rather bad. I suspect that it's because of lazy evaluation of items in the list we're constructing (and also using during construction). Not really. Your problem is that you calculate maxPaths vals over and over again in where mpath i val = val + maximum [(maxPaths vals) !! pi| pi - prev i] ; the value isn't shared (it is, if compiled with optimisations). If you share the list by giving it a name, your programme becomes much faster (interpreted or compiled without optimisations; with -O, it's below measuring accuracy anyway) and needs only a little memory: maxPaths vals@(v:vs) = mps where mps = v : zipWith mpath [1 .. ] vs mpath i val = val + maximum [mps !! pi| pi - prev i] How can I force eager evaluation of items, put into the list? That's a little tricky. Fortunately, it's not necessary. Any other comments and suggestions are also very welcome. You can get rid of the index calculations and the list indexing if you work on the list of rows (i.e., make triangle18 :: [[Int]]). IMO, the code will be easier to follow then, too. I know index-based item lookup in a list is not efficient, but I'll take care of this later (I don't know much about arrays yet). For now, I'm more concerned with the memory usage. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proposal to solve Haskell's MPTC dilemma
On 21 May 2010 01:58, Carlos Camarao carlos.cama...@gmail.com wrote:
But this type-correct program would become not typeable if
instances such as the ones referred to before (by Daniel Fischer) ...
It seems that single param type classes enjoy a nice property: ...
* Adding an instance to the module defining the class cannot conflict
with any non-orphan instance defined elsewhere ...
Max, thanks very much for your message. I will defer comments about
definitions of orphan instances to a postscript. First I'd like to say the
following.
I think that a notion of orphan instances based on whether an
instance is defined or not in the module where the class of the
instance is defined is not very nice, because classes have global
scope and then it should not matter in which module a class is
defined, as long as it is defined somewhere in the current or some
imported module.
Let us thus not try to extend a definition based on this to MPTCs.
However, the module fragility issue you raised is quite relevant. Let
us call a type-correct module M fragile if definitions inserted in
modules imported by M cause M to become type-incorrect.
This issue is more relevant in Haskell than in other languages because
instance definitions are automatically imported when a module is
imported, and importation of an instance cannot be forbidden.
Our unreacheable_var-implies-overloading_resolution_test proposal
can be viewed as a proposal to
test-visible-instances-before-considering-types-as-ambiguous.
Ambiguity means the existence of two or more conflicting definitions
that could be used in an expression (and the inexistence of a
reasonable criteria for selecting between conflicting definitions). In
Haskell, nowadays, ambiguity is reported without looking to see if
there really are conflicting definitions. What FDs do is to require
programmers to specify dependencies between class variables which make
the compiler look to see if there exist definitions that can satisfy
such dependencies, before reaching any conclusion that an expression
is ambiguous. What we propose (relieving the burden on programmers) is
to make the compiler look itself to see if there exist two or more
(well, or none) definitions and report error only if this is the case
(again, before reaching any conclusion that an expression is
ambiguous). If there is exactly one instance definition, there is no
ambiguity (there is no conflict); in such case, then: use that single
definition that the programmer defined.
A benefit of adopting our approach would be that defaulting would
become unnecessary (defaulting always occurring in favor of visible
definitions).
Module robustness can be achieved --- even maintaining automatic
importation of instance definitions --- by considering, for each
instance definition, say I, defined by
instance C bla1 I bla2 where ...
that an automatic defaulting rule that names C
(see hackage.haskell.org/trac/haskell-prime/wiki/Defaulting) is
virtually and automatically inserted, namely:
default C bla1 I bla2
It should perhaps be noted though that one could have more than one such
automatic default rule for the same class.
Cheers,
Carlos
=
PS: I think that a definition of orphan/non-orphan instance definition
for MPTCs should be different.
Letting:
defM(C) = module where C is defined
local-datatype(T,M,C) = T is defined in M or T is defined in defM(C)
import-list(M,C) = {M} U { import-list(M') | M imports M'}
instance-def(I,C,M,tv) = I is an instance definition of class C,
occurring in
module M, that instantiates class variable tv
then you consider (if I have correctly understood and expressed what
you wrote):
Non-orphan = [for all I,C,M,tv: instance-def(I,C,M,tv) =
local-datatype(T,M,C)]
Orphan = [there exists I,C,M,tv: instance-def(I,C,M,tv) ^ not
local-datatype(T,M,C)]
And I think a correct definition of orphan/non-orphan for MPTCs should
be along the line:
Non-orphan = [there exists I,C,M,tv: instance-def(I,C,M,tv) ^
local-datatype(T,M,C)
Orphan = [forall I,C,M,tv: instance-def(I,C,M,tv) ^ not
local-datatype(T,M,C)]
That is, an instance should be considered non-orphan if there exists
at least one datatype to which a class type variable in such instance
is instantiated, because other instances which instantiated such class
type variable to such datatype would be non-orphan.
GHC is thus correct, I think.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] How to construct a lazy list of eagerly-evaluated items?
Not really. Your problem is that you calculate maxPaths vals over and over again in where mpath i val = val + maximum [(maxPaths vals) !! pi| pi - prev i] ; the value isn't shared (it is, if compiled with optimisations). If you share the list by giving it a name, your programme becomes much faster (interpreted or compiled without optimisations; with -O, it's below measuring accuracy anyway) and needs only a little memory: maxPaths vals@(v:vs) = mps where mps = v : zipWith mpath [1 .. ] vs mpath i val = val + maximum [mps !! pi| pi - prev i] Thank you - exactly the kind of answer I was looking for! ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Mechanics of type-level proxies through branding?
Hi. I'm a Haskell newbie, and I've been reading Oleg's work about lightweight dependent types in Haskell, and I've been trying to figure out if I understand how branding works (warning bells already, I know). At http://okmij.org/ftp/Computation/lightweight-dependent-typing.html#Branding, he states A language with higher-rank types or existential type quantification lets us introduce type proxies for the values. We can associate a value with some type in such a way that type equality entails value equality... Then, in the code for eliminating array bounds checking at http://okmij.org/ftp/Haskell/eliminating-array-bound-check.lhs, the following example of branding is given: brand:: (Ix i, Integral i) = Array i e - (forall s. (BArray s i e, BIndex s i, BIndex s i) - w) - w - w brand (a::Array i e) k kempty = let (l,h) = bounds a in if l = h then k ((BArray a)::BArray () i e, BIndex l, BIndex h) else kempty ... The function brand has a higher-rank type. It is the existential quantification of 's' as well as the absence of BArray constructor elsewhere guarantee that the same brand entails the same bounds. I think I understand that the fact that the type variable 's' is shared between BArray, and BIndex's type constructors in the type annotation for brand, that the array and indices share the same brand. I also think I understand that since 's' is existentially quantified and a phantom type, it's unique and cannot ever be unified w/ any other type? Additionally, it seems that this is all only within the scope of the continuation? That is, type equality entails value equality but not value equality entails type equality, e.g. if I call brand two times with arrays of the same bounds, I'd get two different brands? Finally, I'm confused why the unit type in the explicit type expression at BArray's value constructor application doesn't foil the branding, i.e. why it doesn't destroy the uniqueness/opaqueness of 's'? Thanks for anyone who can explain this! Dave ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] [ANNOUNCE] First Public Release of the Snap Framework
On Sun, May 23, 2010 at 1:36 AM, Gregory Collins g...@gregorycollins.netwrote: Michael Snoyman mich...@snoyman.com writes: If the POST body has content-type application/x-www-form-urlencoded we parse it for you and put the fields in the parameter mapping. If this isn't your case I'd appreciate a bug report. This is a place where we made a different design decision than you did -- a WAI application which expects to parse the POST body itself won't work. I'll think about adding a knob to make this behaviour optional. I'd appreciate such a knob. Out of curiosity, do you also parse multi-part data? No, not yet :(, and we'll never do so automatically; we limit POST bodies to 1MB or something like that (to prevent malicious requests from trashing the server) but multipart requests can contain file uploads, which we would probably want to be able to stream to disk somehow. If you're interested, you can look at the Network.Wai.Parse module in wai-extra. The parseRequestBody function takes an argument of type Sink that specifies how data should be stored. By default, I provide an lbsSink and tempFileSink. Michael ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Functional Parsers in GHCI
Hi All, I am a newbie to Haskell, and have been using Programming in Haskell along with Eric Meijer videos covering the book syllabus. I am currently on Chapter 8 Functional Parsers, and trying to implement few of the examples given in the book. Following is the example : item = \inp - case inp of [] - [] (x:xs) - [(x,xs)] p = do x - item y - item z - item return (x,y,z) = When I compile it using GHCI, I get the following error : [1 of 1] Compiling Main ( parser.hs, interpreted ) parser.hs:5:8: No instance for (Monad ((-) [t])) arising from a do statement at parser.hs:5:8-16 Possible fix: add an instance declaration for (Monad ((-) [t])) In a stmt of a 'do' expression: x - item In the expression: do x - item y - item z - item return (x, y, z) In the definition of `p': p = do x - item y - item z - item Failed, modules loaded: none. = I tried googling for samples, above error message etc. But not getting to solution. Can anyone guide me as to what am I doing wrong and how can I fix this. Regards, Amiruddin Nagri, India GTalk : amir.na...@gmail.com ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Mechanics of type-level proxies through branding?
On Sat, May 22, 2010 at 8:36 PM, Dave Neuer dave.ne...@pobox.com wrote:
Hi.
I'm a Haskell newbie, and I've been reading Oleg's work about
lightweight dependent types in Haskell, and I've been trying to figure
out if I understand how branding works (warning bells already, I
know).
At
http://okmij.org/ftp/Computation/lightweight-dependent-typing.html#Branding,
he states A language with higher-rank types or existential type
quantification lets us introduce type proxies for the values. We can
associate a value with some type in such a way that type equality
entails value equality...
Then, in the code for eliminating array bounds checking at
http://okmij.org/ftp/Haskell/eliminating-array-bound-check.lhs, the
following example of branding is given:
brand:: (Ix i, Integral i) = Array i e
- (forall s. (BArray s i e, BIndex s i, BIndex s i) - w)
- w - w
brand (a::Array i e) k kempty =
let (l,h) = bounds a
in if l = h then k ((BArray a)::BArray () i e, BIndex l, BIndex h)
else kempty
...
The function brand has a higher-rank type. It is the existential
quantification of 's' as well as the absence of BArray constructor
elsewhere guarantee that the same brand entails the same bounds.
First, Haskell lacks (free) existential type quantifiers, so the above
uses universal quantification. The usage is equivalent to using an
existential but it is an encoding and so it is important to know what
is being encoded or alternatively to stick just to the actual
universal quantification that is there. Second, this function encodes
more than is necessary. It is necessary to use a CPS style for the
encoding of existentials, but the above code also CPS encodes a case
analysis. Here's an equivalent implementation and a proof that it is
equivalent. Here and elsewhere I'll set i to Int for simplicity.
{-# LANGUAGE RankNTypes, ScopedTypeVariables, ExistentialQuantification #-}
import Data.Array
newtype BA s e = BArray (A e)
newtype BI s = BIndex Int
type A e = Array Int e
brand :: A e - (forall s. (BA s e, BI s, BI s) - w) - w - w
brand (a :: A e) k kempty =
let (l,h) = bounds a
in if l = h then k (BArray a :: BA () e, BIndex l, BIndex h)
else kempty
brand' :: A e - (forall s. Maybe (BA s e, BI s, BI s) - w) - w
brand' (a :: A e) k = k (if l = h then Just (BArray a :: BA () e,
BIndex l, BIndex h) else Nothing)
where (l,h) = bounds a
brandFromBrand' :: A e - (forall s. (BA s e, BI s, BI s) - w) - w - w
brandFromBrand' a k kempty = brand' a (maybe kempty k)
brand'FromBrand :: A e - (forall s. Maybe (BA s e, BI s, BI s) - w) - w
brand'FromBrand a k = brand a (k . Just) (k Nothing)
Once you see the Maybe it's easier to see what the existential type
would be if Haskell had the appropriate existentials.
brand :: A e - exists s. Maybe (BA s e, BI s, BI s)
or equivalently
brand :: A e - Maybe (exist s. (BA s e, BI s, BI s))
Using local existential quantification which GHC supports we can
encode the above and prove it equal to the earlier representations.
data B e = forall s. B (BA s e) (BI s) (BI s)
brand'' :: A e - Maybe (B e)
brand'' a = if l = h then Just (B (BArray a) (BIndex l) (BIndex h))
else Nothing
where (l,h) = bounds a
brand''FromBrand' :: A e - Maybe (B e)
brand''FromBrand' a = brand' a (fmap (\(ba,l,h) - B ba l h))
brand'FromBrand'' :: A e - (forall s. Maybe (BA s e, BI s, BI s) - w) - w
brand'FromBrand'' a k = case brand'' a of
Nothing - k Nothing
Just (B ba l h) - k (Just (ba, l, h))
I think I understand that the fact that the type variable 's' is
shared between BArray, and BIndex's type constructors in the type
annotation for brand, that the array and indices share the same
brand.
Correct.
I also think I understand that since 's' is existentially quantified
and a phantom type, it's unique and cannot ever be unified w/ any
other type?
The phantom type aspect is irrelevant. s is a phantom type because we
don't need to actually represent it in any way. As far as the rest of
the paragraph it's somewhat tricky though I think you've got the right
idea. Whether s can unify with something depends on your perspective.
In general, when introducing a universal quantifier we need to treat
the quantified variable as a fresh constant that doesn't unify with
anything. This guarantees that we aren't making any assumptions about
it. When eliminating a universal quantifier, we do allow unification,
or, when instantiation is explicit, we explicitly are saying what type
to unify the type variable with. The rules for existentials are dual.
brand is eliminating a universal and brand'' is equivalently
introducing an existential, within the body of brand/brand'' so s can
and does unify. In brand it is unified with (). Consumers of these
will be doing the dual operation and so they must not unify s.
Additionally, it seems that this is all only within the
