- Haskell-Cafe - Haskell.org

Re: [Haskell-cafe] Bool is not...safe?!
by Olaf Klinke 08 Jul '18

08 Jul '18

>But in Prolog every piece of code is evaluated to TRUTH or to FALSE. Each sentence is a goal which can be achieved and becomes a fact >or can not be – and becomes lie. So, if you inverse semantic in Haskell – program is compiled although with strange behaviour but in >Prolog program become lie. Prolog evaluation model has clean definition in run-time too, not only at compile-time. Execution of >Prolog program is a CHECK: is it truth or lie? I have only very limited Prolog pratice. But what you state about Prolog's semantics is only true for very simple cases, isn't it? As soon as I/O is involved, things get messier. Also, there are actually three outcomes as far as I know: provably true, provably false and "could not be proved" which is different from "false". When I anticipate an exception in an application where the condition prohibits the program from fulfilling its purpose, I simply call error. A common pattern I use is a library function that has return type (Either SomeErr Value), and the application takes it and wraps the result in either (error.show) return, transforming (Either SomeErr Value) into (IO Value). For libraries, one should be more careful, as we don't know what kind of environment the function might be called in - see Joachim Durchholz's post. Olaf

1 0

Re: [Haskell-cafe] Bool is not...safe?!
by Olaf Klinke 08 Jul '18

08 Jul '18

> >> true = return () >> (&&) = liftM2 const >> (||) = mplus >> false = mzero > > I don't think it's by definition yet, but surely by convention, that > this is a restricted form of > > true = pure () > (&&) = (<*) > (||) = (<|>) > false = empty > > All of these functions require only an Applicative or an Alternative, > and except for "true", they're all in the library. True, and after sending I realized I should have used exaclty the definitions you gave. It's just that I don't know whether there exists the concept of "commutative applicative". It is equired for (&&) to be commutative. How could one even state it without the monad bind? The following definitions are from a category theory paper [1] by Anders Kock. import Control.Monad -- tensorial strengths t'' :: (Functor m) => a -> m b -> m (a,b) t'' a mb = fmap (\b -> (a,b)) mb t' :: (Functor m) => m a -> b -> m (a,b) t' ma b = fmap (\a -> (a,b)) ma -- so-called linear extensions in the first and second argument linearext1 :: Functor m => (m c -> c) -> (a -> b -> c) -> m a -> b -> c linearext1 struct f ma b = struct $ (fmap $ uncurry f) $ t' ma b linearext2 :: Functor m => (m c -> c) -> (a -> b -> c) -> a -> m b -> c linearext2 struct f a mb = struct $ (fmap $ uncurry f) $ t'' a mb The first argument to linearext1 and linearext2 is called a "structure map" in the context of [1]. Such structure maps exist when m is a monad. Indeed, we have linearext1 join t'' :: (Monad m) => m a -> m b -> m (a, b) linearext2 join t' :: (Monad m) => m a -> m b -> m (a, b) Now m is called commutative if the above two maps are the same [*]. But join does not exist for applicative functors, it is interdefinable with (>>=). Olaf [1] Anders Kock: "Commutative Monads as a Theory of Distributions". Theory and Applications of Categories, Vol. 26 No. 4 (2012). [*] They are called Fubini maps because a special case is Fubini's theorem about integration by parts.

1 0

ANN: network-2.7.0.2
by evan＠evan-borden.com 07 Jul '18

07 Jul '18

Announcing network-2.7.0.2 * Removing withMVar to avoid the deadlock between "accept" and "close" [#330](https://github.com/haskell/network/pull/330) * "close" does not throw exceptions. A new API: "close'" throws exceptions when necessary. [#337](https://github.com/haskell/network/pull/337) * Fixing the hang of lazy sendAll. [#340](https://github.com/haskell/network/pull/340) * Installing NetDef.h (#334) [#334](https://github.com/haskell/network/pull/334) Thank you to network contributors for this bug fix release. -- Evan Borden

1 0

ANN: network-2.6.3.6
by evan＠evan-borden.com 07 Jul '18

07 Jul '18

Announcing network-2.6.3.6 This is a bug fix release for the 2.6 branch of network. * Removed unnecessary withMVar, which caused locking on close. [#330](https://github.com/haskell/network/pull/330) Thank you to network contributors for finding and diagnosing the bug. -- Evan Borden

1 0

[GSoC 2018] Benchmarking Haskell graph libraries
by Alexandre Moine 06 Jul '18

06 Jul '18

[ Results are here: https://github.com/haskell-perf/graphs/tree/master/results/ ] Hi, I am french 2nd year student in maths and computer sciences and I am running a {Google,Haskell} Summer of Code now. One of my goals is to write a benchmarking suite for graphs libraries in Haskell (Fgl, Alga, Containers and Hash-Graph) and I reached a state where I can produce reasonable numbers. If you are interested, I have wrote a little blog article explaining the results I obtained: https://blog.nyarlathotep.one/2018/07/benchmarking-haskell-graph-libraries/ Feel free to comment or to send feedback on the Github :) -- Alexandre Moine

1 0

Bool is not...safe?!
by PY 06 Jul '18

06 Jul '18

Hello, Cafe! There is an opinion that Bool type has problems. It's "dangerous", because it's not good to be used as flag for success/fail result. I read this post: https://existentialtype.wordpress.com/2011/03/15/boolean-blindness/ and was shocked. How popular is such opinion? Is it true, that bool is "bad" type? As I understand arguments of the post, Bool is bad because: 1) you don't know what does True/False mean 2) after comparison you get bit (!) only but then you may need to "recover" the comparing value which was "shrink" to bit already. Let's begin from 2. As I understand the author talks about one register computers ;) if he have to "recover" a value. But shown examples are in ML, where function arguments are bound to all function body, so you don't need to "recover" anything, what was bound as function argument or with "let". Sounds totally weird and more close to psychology than to CS :) Argument #1 is more interesting. A Boolean,/b/, is either*true*, or *false*; that’s it. There is no/information/carried by a Boolean beyond its value, and that’s the rub. As Conor McBride puts it, to make use of a Boolean you have to know its/provenance/so that you can know what it/means./ Really, what does True/False mean? How to find semantic of True? It's very simple, because there is A) contract/interface which interprets True/False and also B) there is a help from science. A) There are a lot of languages (Unix shell, ML, Basic, Haskell, C/C++...) with short-circuit expressions. Ex., e1 || e2 e1 && e2 e1 orelse e2 where interface is described by its operations: ||, &&, orelse, etc and it has absolutely accurate and clear meaning: "||" executes e2 iff e1 *fails, was not success*. "&&" executes e2 iff e1 was succeeded. I don't use words "True" and "False". Because, in different languages marker of success/fail is different. For example, in Bash, the fail is any integer except 0. In Haskell fail is False. In C is 0... What does mean False (and True) is defined by contract/interface of short-circuit operations, related to boolean algebra. A rare case when type is bound with semantic! We read them literally (native English): e1 or-else e2! *This means that using of False to indicate success - is error! And no way to miss provenance/knowledge what True or False means.* (the same: what does Right/False mean?) B) The help from science. Math (and CS) has own history. And one of its mail-stones was birth of formal logic and then of Boolean algebra. CS implemented those in declarative languages (Prolog, for example). If we have some predicate in Prolog, "true" for that predicate means "it was achieved", as goal. If that predicate has side-effects, "true" means it was achieved, i.e. all its steps (side-effects) were successfully executed. Predicate write_text_to_file/2 is "true" when it wrote text to file. And no way to return False on success or to think about sacral sense of True/False :) And that sense traditionally is the same in all programming language. If you invert it, you deny contract, semantic and begin to use "inverted" logic :) We can repeat the same logic with 3.1415926.. What does it mean? Meaning, semantic is described, but contract/interface: this magic irrational was born from part of algebra, called trigonometry. And this algebra defines semantic of Pi, not programmer's usage of Pi, programming context, etc. True/False semantic is defining by its algebra: boolean. So, programmer should not change their semantic, am I right? So, my question is: is this post a april 1st trolling or author was serious? :) --- Best regards, Paul

7 9

Measuring memory usage
by Vlatko Basic 05 Jul '18

05 Jul '18

Hello, I've come to some strange results using Weigh package. It shows that HashMap inside 'data' is using much, much more memory. The strange thing is that I'm seeing too large mem usage in my app as well (several "MapData" like in records), and trying to figure out with 'weigh' what's keeping the mem. Noticed that when I change the code to use HashMap directly (not inside 'data', that's the only change), the mem usage observed with top drops down for ~60M, from 850M to 790M. These are the test results for 10K, 5K and 3.3K items for "data MapData k v = MapData (HashMap k v)" (at the end is the full runnable example.) Case Allocated GCs HashMap 262,824 0 HashMap half 58,536 0 HashMap third 17,064 0 MapData 4,242,208 4 I tested by changing the order, disabling all but one etc., and the results were the same. Same 'weigh' behaviour with IntMap and Map. So, if anyone knows and has some experience with such issues, my questions are: 1. Is 'weigh' package reliable/usable, at least to some extent? (the results do show diff between full, half and third) 2. How do you measure mem consumptions of your large data/records? 3. If the results are even approximately valid, what could cause such large discrepancies with 'data'? 4. Is there a way to see if some record has been freed from memory, GCed? module Main where import Prelude import Control.DeepSeq (NFData) import Data.HashMap.Strict (HashMap, fromList) import GHC.Generics (Generic) import Weigh (mainWith, value) data MapData k v = MapData (HashMap k v) deriving Generic instance (NFData k, NFData v) => NFData (MapData k v) full, half, third :: Int full = 10000 half = 5000 third = 3333 main :: IO () main = mainWith $ do value "HashMap" ( mkHMList full) value "HashMap half" ( mkHMList half) value "HashMap third" ( mkHMList third) value "MapData" (MapData $ mkHMList full) mkHMList :: Int -> HashMap Int String mkHMList n = fromList . zip [1..n] $ replicate n "some text"

4 8

Typechecker Plugin Constraint Solving
by Armin Wurzinger 04 Jul '18

04 Jul '18

Good day, I am currently developing a typechecker plugin for GHC for realizing an idea regarding types based on regular expressions to describe the contents of a string. This is done using type-level literals to denote a particular regex. Additionally there are additional constraints for working with such types. One of those constraints is called Intersectable and denotes whether an intersection between two regexes would be possible in the sense that there is some common alphabet between them. Furthermore there is a type-level function that calculates the actual intersection between two regex types and returns the resulting regex type: type family Intersectable (a :: Symbol) (b :: Symbol) :: Constraint type family Intersection (a :: Symbol) (b :: Symbol) :: Symbol Now i've created a typechecker plugin that resolves such constraints by using a finite-automata representation of the regexes to do the actual work. While my plugin is already able to proof progams where regexes are fully applied, i.e. they can reduce terms to a single regex and then verify the constraints accordingly or reject them, it fails to type "intermediate" functions. As a small example assume the following program: checkFour :: Intersectable a "[0-4]" => RgxString a -> RgxString (Intersection a "[0-4]") checkFour a = undefined checkEight :: Intersectable a "[0-8]" => RgxString a -> RgxString (Intersection a "[0-8]") checkEight a = undefined test = checkFour . checkEight -- this fails to type correctly test2 = checkFour $ checkEight $ (RgxString :: RegexString ".*") -- this works fine The constraint solver wants me to proof the following constraints for test: tcPluginSolve given = [] derived = [] wanted = [ [WD] irred_a2GV {0}:: Intersectable (Intersection a0 "[0-8]") "[0-4]" (CNonCanonical), [WD] irred_a2GY {0}:: Intersectable a0 "[0-8]" (CNonCanonical)] My plugin reduces the first constraint to Intersectable a0 [0-4] as regex intersection is commutative so i can intersect [0-8] with [0-4] first. But i haven't found out yet how i would tell the compiler to put this reduced constraint to the type signature instead of the current one where the constraint got dropped at all instead of at least remain unnormalized, and the return type remains unnormalized as well: RgxString a -> RgxString (Intersection (Intersection a "[0-8]") "[0-4]") I'd need to tell the typechecker somehow that (Intersection (Intersection a "[0-8]") "[0-4]") is equal to Intersection a "[0-4]" so it substitutes it accordingly. My idea is that i have to generate given type and function equality constraints during the typechecking telling it that those representations are equal, but i am really not sure what kind of constraints i need. CTyEqCan for instance seems to require a TyVar on one side while i though i could generate something like Intersection (Intersection a "[0-8]") "[0-4]" ~ Intersection a "[0-4]" I have already tried a lot but there is little documentation on the whole constraint solving process and i am slowly getting stuck. Thanks for helping!

1 0

ForeignPtrs, Finalizers and thread-local storage
by Justin Paston-Cooper 03 Jul '18

03 Jul '18

glpk-hs defines a binding to glpk, a linear programme library. A linear programme is created by calling `glp_create_prob` and deleted by calling `glp_delete_prob`. These two C functions manage memory themselves using thread-local storage. They are called by glpk-hs using the foreign function interface in the following code. Note that glpDelProb and glpCreateProb are imported foreign functions. runGLPK :: GLPK a -> IO a runGLPK m = do lp <- newForeignPtr glpDelProb =<< glpCreateProb withForeignPtr lp (execGLPK m) ( https://github.com/jyp/glpk-hs/blob/master/src/Data/LinearProgram/GLPK/Type… ) It seems that sometimes the finaliser is called in a thread different to the one where glp_create_prob is called. This leads to glpk aborting with a dynamic memory allocation error when tries to de-allocate the linear programme in the wrong thread-local storage, which has never seen that programme. Given that the ForeignPtr is used only in runGLPK, runGLPK could of course be fixed by using Control.Concurrent.bracket instead. However, I'm interested to know whether there is a solution to this problem. I'm only assuming that the finaliser sometimes runs in a different thread. If this is indeed the case, then is there any way to ensure that a finaliser runs in the thread where the pointer is created?

1 1

GHC's timing: Now solid enough for music?
by Jeffrey Brown 03 Jul '18

03 Jul '18

I just discovered Tom Murphy's Vivid-Synth[1], a Haskell library that lets you control SuperCollider. (A few very slight changes allowed me to get it to work in Stack instead of Cabal, as described here[2,3].) TidalCycles[4] also controls SuperCollider from Haskell. It does tortuous backflips to hand the timing job over to SuperCollider. If I recall correctly, that was because SC's timing was more solid than Haskell's. I modified the Vivid demo to go faster and have a few more voices[5], and tried running it at the same time as Spotify and Youtube and apt upgrade and loading LibreOffice and playing some music in VLC, and I detected (by ear) no timing errors. Can I expect GHC's maybe-new rhythmic stability to hold up? [1] http://www.vivid-synth.com/ [2] https://github.com/vivid-synth/vivid/issues/5 [3] https://github.com/JeffreyBenjaminBrown/vivid/commit/3d25266d4495d9dd8e573f… [4] https://tidalcycles.org/ [5] https://github.com/JeffreyBenjaminBrown/vivid/blob/jbb/jbb/sine.hs -- Jeff Brown | Jeffrey Benjamin Brown Website <https://msu.edu/~brown202/> | Facebook <https://www.facebook.com/mejeff.younotjeff> | LinkedIn <https://www.linkedin.com/in/jeffreybenjaminbrown>(spammy, so I often miss messages here) | Github <https://github.com/jeffreybenjaminbrown>

3 2