okeuday_bak 2017-03-04 11:46:07
when using https://hackage.haskell.org/package/binary-0.8.4.1/docs/Data-Binary-Get.html the usage of function runGetOrFail will somehow return the string fed to the fail function in the Left data, right?
geekosaur 2017-03-04 11:46:53
that sounds like the wrong way of thinking about it
geekosaur 2017-03-04 11:47:01
Either is what the name says
okeuday_bak 2017-03-04 11:47:05
or does the exception not get caught at that level?
geekosaur 2017-03-04 11:47:10
it is Either the Left or the Right, it is never both
geekosaur 2017-03-04 11:48:15
the error message from `fail` should be the String element of the tuple
okeuday_bak 2017-03-04 11:48:25
k
geekosaur 2017-03-04 11:48:35
(3rd element)
MarcelineVQ 2017-03-04 11:52:08
ertes: http://lpaste.net/353218
ertes 2017-03-04 11:56:37
MarcelineVQ: this may sound like nitpicking, but you really need to be precise here: "for all naturals n, there exists some natural number k such that n = k*2"
ertes 2017-03-04 11:56:44
counterexample: 1
ertes 2017-03-04 11:57:30
instead you need to define what it means when you say "n is even", which is a definition: "n is even" is the same statement as "…"
geekosaur 2017-03-04 11:57:47
...and this is why most people don't include proofs...
ertes 2017-03-04 11:59:08
MarcelineVQ: however, without nitpicking too much on your syntax, your actual proof is fine, so congratulations =)
ertes 2017-03-04 11:59:49
if you're more rigorous about your syntax, a proof assistant would accept your proof (assuming that you have already proved distributivity)
MarcelineVQ 2017-03-04 12:07:00
that's good, thank you. that rule was more precise before, I flubbbed it when combining lines it looks like. actually I had another issue where I couldnt decide whether to be specific enough to say, "for every even natural n there exists exactly one natural k such that n = k*2" or whether I could ignore that since it'd be a consequence of them being natural numbers, sort of like how having to define distributivity would need its
MarcelineVQ 2017-03-04 12:07:00
own proof that I'm not sure how to tackle
MarcelineVQ 2017-03-04 12:08:36
I can certainly see why, if you need to show every part, proofs would get prety big. Also this shows to me that a proof is only as good as the assumptions you're making, we start this of by saying what even means to us, but who knows, maybe at n = 1000000000 suddenlty even stops being true.
ertes 2017-03-04 12:10:36
MarcelineVQ: in mathematics you generally don't prove every detail… instead you refer to theorems, i.e. things that have already been proven
ertes 2017-03-04 12:10:43
sort of like you use libraries in programming
ertes 2017-03-04 12:10:57
when using a proof assistant those things literally become libraries =)
ertes 2017-03-04 12:11:44
distributivity is surprisingly complex to prove from scratch (not difficult, just very tedious)
hrumph 2017-03-04 12:29:00
it'hi
hrumph 2017-03-04 12:29:02
hi
hrumph 2017-03-04 12:29:12
what do i have to include to have MonadTrans available?
johnw 2017-03-04 12:33:52
Hoogle will tell you
hrumph 2017-03-04 12:34:19
i tried control.monad.trans but it's not available
hrumph 2017-03-04 12:34:33
should i install haskell-platform or something?
johnw 2017-03-04 12:35:13
https://www.haskell.org/hoogle/?hoogle=MonadTrans
ertes 2017-03-04 12:38:31
does the lens library provide a generalisation of splitAt to arbitrary sequence types?
glguy 2017-03-04 12:39:36
no
ertes 2017-03-04 12:39:47
ok, thanks
