laz 2017-02-06 21:47:26
absence: looks like global stack cache is corrupted
laz 2017-02-06 21:47:45
absence: try to clean ~/.stack
absence 2017-02-06 21:56:39
laz: thanks. i had already cleaned AppData\Local\Programs\stack, but there was an AppData\Roaming\stack that i missed
tfc 2017-02-06 22:01:31
hi there, i built a little applicative parser and i would like someone to look over it to tell me if there is a better way to express it
tfc 2017-02-06 22:01:32
Prelude Text.ParserCombinators.Parsec> parse ((manyTill anyChar $ string "FOO") *> (many $ oneOf ['0'..'9']) <* (string "BAR")) "foo" "bla bla FOO123BAR bla"
erisco 2017-02-06 22:14:55
jle`, I have now defined and proven the total and strict total orders for Nat :)
jle` 2017-02-06 22:15:07
congrats :o
erisco 2017-02-06 22:15:44
negation is still a bit of a strange beast... I found you can also use it to prove branches are dead
erisco 2017-02-06 22:15:51
though I am not sure how well GHC recognises this
erisco 2017-02-06 22:16:03
i.e. you find a contradiction
jle` 2017-02-06 22:16:32
the extent that i've used it in haskell/ghc is just from empty case statements more or less, heh
lyxia 2017-02-06 22:16:48
tfc: that looks good
erisco 2017-02-06 22:16:57
jle`, like this proof here http://lpaste.net/352160
erisco 2017-02-06 22:17:45
so you reach a context where you can construct a :<= proof, such as LteZ n, and then you pass this to the negation proof to find Void
jle` 2017-02-06 22:17:46
nice :)
tfc 2017-02-06 22:17:50
lyxia: thx. how would you change it in order to allow for strings like "bla FOO blabla FOO123BAR" ?
erisco 2017-02-06 22:18:08
which feels a bit odd because we're kinda in a way backtracking
jle` 2017-02-06 22:18:21
it feels weird at first, but yeah, you kind of get used to it
erisco 2017-02-06 22:18:25
we're saying that m can be SZ but oh no wait that is a contradiction
tfc 2017-02-06 22:18:28
lyxia: right now it would error out and i would need to use some kind of a "try" statement ,but i feel uncomfortable with that because i could quickly buffer overflow
erisco 2017-02-06 22:19:13
I couldn't think of any other way to do this proof other than by induction on m and n
erisco 2017-02-06 22:19:41
or recursion I guess
erisco 2017-02-06 22:22:12
jle`, I was happy to realise := for *
erisco 2017-02-06 22:22:24
so that I can prove (a :< b) := Not (b :<= a)
jle` 2017-02-06 22:22:38
:o
jle` 2017-02-06 22:22:44
that gives you the two way implication doesn't it
erisco 2017-02-06 22:22:50
yes
erisco 2017-02-06 22:24:00
though unlike := for Nat, these aren't equivalent types
erisco 2017-02-06 22:24:12
so it cannot be promoted to the context
erisco 2017-02-06 22:24:17
(or derived from the context)
jle` 2017-02-06 22:24:59
oh i see
erisco 2017-02-06 22:25:57
Iso :: { fwd :: a -> b, bwd :: b -> a } -> a := b
erisco 2017-02-06 22:26:29
and of course I prove := is an equivalence relation for all instances
BernhardPosselt 2017-02-06 22:26:53
hi, just wondering if this very simple/naive maybe implementation is similar to the one implemented https://dpaste.de/u17Z
erisco 2017-02-06 22:27:28
because you can mix families and classes it is easy to stipulate the properties along with the data family
jle` 2017-02-06 22:28:19
BernhardPosselt: you're missing a few parentheses, but, yeah
BernhardPosselt 2017-02-06 22:29:42
jle`: yeah, just realised now :D
BernhardPosselt 2017-02-06 22:29:47
Just (f x)
BernhardPosselt 2017-02-06 22:30:18
so basically the only difference between map and flatMap/concatMap for maybe is that map needs to wrap it in a maybe again
BernhardPosselt 2017-02-06 22:30:32
whereas flatMap just returns the value from the function
jle` 2017-02-06 22:30:55
well, that's the difference in how they're implemented
jle` 2017-02-06 22:31:04
conceptually, there are deeper consequences
jle` 2017-02-06 22:31:23
map for Maybe cannot change whether or not a value is Nothing or Just
jle` 2017-02-06 22:31:30
but flatMap/bind can
BernhardPosselt 2017-02-06 22:31:47
so you could return an IO monad from bind?
jle` 2017-02-06 22:32:04
er, that's not what i meant, and it doesn't really make sense either
jle` 2017-02-06 22:32:20
i mean that no matter what function you map, you can't change a Nothing to a Just or a Just to a Nothing
jle` 2017-02-06 22:32:41
but if you use flatMap/bind, you can decide whether or not the result is Just or Nothing based on any potential values that the Maybe might contain
jle` 2017-02-06 22:32:54
that's the extra power you get with bind for Maybe
jle` 2017-02-06 22:33:04
(that you don't have with fmap)
jle` 2017-02-06 22:33:33
er, to be more precise, the function that you flatmap/bind has the power to say whether or not the result is Just or Nothing
jle` 2017-02-06 22:34:09
but, for 'map'/'fmap', the function you pass can't change Nothing/Justness, no matter what
jle` 2017-02-06 22:35:36
people commonly say that map/fmap necessarily preserves 'structure', but bind doesn't have to.
jle` 2017-02-06 22:36:17
in the case of IO, "structure" can be thought of as "effects"; so, fmap/map for IO can never change the effects that that IO action encodes
jle` 2017-02-06 22:36:35
you can fmap any function you want onto an IO action, and it won't change its effects
BernhardPosselt 2017-02-06 22:36:37
i see :)
erisco 2017-02-06 22:37:06
the preservation coming from the requirement fmap id = id
jle` 2017-02-06 22:37:16
but, for >>=/bind on IO, the function bind has the ability to determine what effects your resulting IO action has
jle` 2017-02-06 22:37:28
*the function that you bind
jle` 2017-02-06 22:37:45
just like for how Maybe, the function that you bind has the ability to determine whether or not the resulting value is Just/Nothing
lyxia 2017-02-06 22:40:04
tfc: Sorry for the delay. I think that the manyTill should be moved out. manyTill anyChar . try $ string "FOO" *> many digit <* string "BAR". But was is the try there that worried you or were you using it in another way?
tfc 2017-02-06 22:40:58
lyxia: what bugs me is that i need to tell the parser "drop all the garbage which might prepend my FOO123BAR content."
tfc 2017-02-06 22:41:18
lyxia: and manyTill was my only idea of how to do that
lyxia 2017-02-06 22:41:49
oh I see, manyTill keeps the repeated results and not the end
BernhardPosselt 2017-02-06 22:42:01
concerning algebraic datatypes: when you create a list/tree you need modify nodes. since everything is non mutable how do you do that? construct a completely new tree/list?
Logio 2017-02-06 22:42:41
short answer: yes
jle` 2017-02-06 22:42:42
BernhardPosselt: you don't have to construct a completely new one; because everything is immutable, you can use sharing
erisco 2017-02-06 22:42:48
you must reconstruct the path from the node to the root
BernhardPosselt 2017-02-06 22:43:05
but the compiler can optimize it i suppose
erisco 2017-02-06 22:43:10
no
lyxia 2017-02-06 22:44:06
tfc: looks like the combinator doesn't exist in parsec
BernhardPosselt 2017-02-06 22:44:20
jle`: what do you mean by sharing?
lyxia 2017-02-06 22:44:30
tfc: I suppose because it's not so common that you're just throwing away information.
mfukar 2017-02-06 22:44:58
dminuoso , QAM. Turns out you can easily achieve optimal or near-optimal minimal distances w/ Gaussian integer constellations
