erisco 2017-02-03 16:46:17
surely S m <= S n ==> m <= n is a theorem
erisco 2017-02-03 16:46:42
why is finding it so tricky :s
barryburd 2017-02-03 16:47:17
I must have some confusion about the IO monad, and maybe someone can clear it up for me. Suppose you have x <- getLine ; putStrLn x and the user inputs Hello. Then getLine is an action (a monadic value) and the <- symbol lets x refer to the value "Hello" that's part of the getLine action. But in another run of the code, the user inputs Goodbye, so doesn't getLine then represent a slightly different monadic value (one
barryburd 2017-02-03 16:47:18
which "Goodbye" is part of the value)? As far as I can see, the difference between the two getLine actions is like the difference between Just "Hello" and Just "Goodbye" in a Maybe monad.
dfeuer 2017-02-03 16:47:28
erisco: what's your definition of <=?
erisco 2017-02-03 16:47:45
dfeuer, http://hackage.haskell.org/package/type-natural-0.7.1.2/docs/Data-Type-Natural.html#t:PeanoOrder
dfeuer 2017-02-03 16:48:07
Oh.
dfeuer 2017-02-03 16:48:09
That.
mniip 2017-02-03 16:48:11
barryburd, getLine doesn't "contain" Hello or Goodbye
mniip 2017-02-03 16:48:23
same way as (+) doesn't contain the number 8
geekosaur 2017-02-03 16:48:24
@quote /bin/ls
lambdabot 2017-02-03 16:48:24
shachaf says: getLine :: IO String contains a String in the same way that /bin/ls contains a list of files
mniip 2017-02-03 16:49:09
good quote
barryburd 2017-02-03 16:49:27
… so referential transparency is preserved.
mniip 2017-02-03 16:49:49
sure is
mniip 2017-02-03 16:50:07
it never was broken
geekosaur 2017-02-03 16:50:07
getLine contains a read-a-string instruction to the runtime. when you use <-, it's actually making a function that will be called when that runtime instruction is executed
dfeuer 2017-02-03 16:50:21
When you start trying to get things out of IO, you're suddenly out of Haskell and writing programs for a graph reduction machine while the optimizer is trying to scramble your code.
geekosaur 2017-02-03 16:50:26
so a Haskell program ends up being a chain of callbacks in IO
erisco 2017-02-03 16:50:45
normally you'd use induction
geekosaur 2017-02-03 16:50:49
(if that sounds vaguely familiar, you may be a JS frontend programmer :)
mniip 2017-02-03 16:50:49
dfeuer, shhhhh
mniip 2017-02-03 16:50:54
you cannot get things out of IO
erisco 2017-02-03 16:51:11
so you'd have S 0 <= S 0 ==> 0 <= 0 trivially because 0 <= 0 is an axiom
dfeuer 2017-02-03 16:51:14
mniip: right. You can only *try* to. And be in a world of extreme difficulty :P
Axman6 2017-02-03 16:51:16
barryburd: getLine is an action which, when executed by the haskell runtime system takes a line of input from the user and pass that into the program. it is a recipe for how to do that, it is not the string itself
mniip 2017-02-03 16:51:20
dfeuer, shhhhhhhhh
erisco 2017-02-03 16:51:38
S m <= S n ==> S (S m) <= S (S n) is trivial because that is already given to us
barryburd 2017-02-03 16:51:39
I understand that it's not the string itself.
erisco 2017-02-03 16:51:50
but I don't think we can convince Haskell about inductive proofs here
mniip 2017-02-03 16:52:10
erisco, if you eat away the S you can
mniip 2017-02-03 16:52:13
it wouldn't be undecidable
dfeuer 2017-02-03 16:52:32
mniip: normally I'm on your side, but I just overhauled the implementation of Control.Monad.ST.Lazy to make it thread-safe, so I have weird stuff on the brain.
erisco 2017-02-03 16:52:32
oh I think my inductive step is backwards :P
jle` 2017-02-03 16:52:50
erisco: oh yes, that one is probably better :)
mniip 2017-02-03 16:52:55
huh
barryburd 2017-02-03 16:53:00
I've asked about the definition of the bind function for the IO monad, and been told that it's not worth looking at.
dfeuer 2017-02-03 16:53:22
barryburd: it is not worth looking at until you get to extreme low-level hacking.
mniip 2017-02-03 16:53:22
barryburd, it's not useful to look at, at your stage
geekosaur 2017-02-03 16:53:30
and possibly not even then
mniip 2017-02-03 16:53:30
you might get mislead
jle` 2017-02-03 16:53:49
i can't even imagine a situation where it would be worth looking at
geekosaur 2017-02-03 16:53:50
the real trick here is do notation turns your apparently imperative "statements" into chains of callbacks
dfeuer 2017-02-03 16:53:57
GHC's model of IO is pretty badly broken, in fact.
mniip 2017-02-03 16:54:06
dfeuer, how come
mniip 2017-02-03 16:54:11
(do you have a better proposal)
dfeuer 2017-02-03 16:54:31
mniip: it requires a large number of terrible compiler hacks to mostly work.
jle` 2017-02-03 16:54:34
the implementation of IO is a lie too I think
dfeuer 2017-02-03 16:54:37
There have been several better proposals.
erisco 2017-02-03 16:54:51
it needs to be assuming S m <= S n ==> m <= n prove S (S m) <= S (S n) ==> S m <= S n
dfeuer 2017-02-03 16:54:55
The trouble is that a shit-ton of libraries and applications will break if that's changed.
mniip 2017-02-03 16:54:56
I think it's fine if I understand it correctly?
jle` 2017-02-03 16:55:24
erisco: fun stuff with peano nats huh
geekosaur 2017-02-03 16:55:33
"state hack"
erisco 2017-02-03 16:55:44
well I don't think I could use an inductive proof even if I could figure it out
dfeuer 2017-02-03 16:55:48
mniip: fine? No, it's not fine. Doing IO in the G-machine is not the way anyone would likely try to do it if GHC were being built from the start today.
jle` 2017-02-03 16:55:58
erisco: are you on the same problem from when i last saw
mniip 2017-02-03 16:56:04
uh
jle` 2017-02-03 16:56:07
at this point i don't even use IO in any of my application code anymore
erisco 2017-02-03 16:56:10
jle`, I am trying to prove S m <= S n ==> m <= n
jle` 2017-02-03 16:56:10
i just make a custom data type
mniip 2017-02-03 16:56:30
dfeuer, what way then?
erisco 2017-02-03 16:57:11
not sure it is possible :s
jle` 2017-02-03 16:57:11
erisco: in haskell?
erisco 2017-02-03 16:57:15
yes
jle` 2017-02-03 16:57:28
i suppose it depends on what axioms you have at hand to use
erisco 2017-02-03 16:57:33
http://hackage.haskell.org/package/type-natural-0.7.1.2/docs/Data-Type-Natural.html#t:PeanoOrder
dfeuer 2017-02-03 16:57:57
mniip: there have been various suggestions; Ed seems to like a sort of codensity-based thing over an opaque FFI type to start with.
jle` 2017-02-03 16:58:18
erisco: maybe you can get away with just doing it inductively
jle` 2017-02-03 16:58:27
hm
jle` 2017-02-03 16:58:31
oh nvm because <= is a type family
erisco 2017-02-03 16:58:32
jle`, how do you encode an inductive proof
mniip 2017-02-03 16:58:48
dfeuer, would that allow for unsafeCoerce
dfeuer 2017-02-03 16:58:57
mniip: what?
dfeuer 2017-02-03 16:59:17
What does unsafeCoerce have to do with it?
jle` 2017-02-03 17:00:08
erisco: maybe you can use http://hackage.haskell.org/package/type-natural-0.7.1.2/docs/Data-Type-Natural.html#v:leqSuccStepL
jle` 2017-02-03 17:00:15
anything with Succ n on the lhs
dfeuer 2017-02-03 17:00:32
mniip: look at http://comonad.com/reader/2011/free-monads-for-less-3/
mniip 2017-02-03 17:00:36
dfeuer, oops, my mind slipped
erisco 2017-02-03 17:00:37
well, sure, so now I am at m <= Succ n but I don't think this gets me far
mniip 2017-02-03 17:00:41
unsafePerformIO
dfeuer 2017-02-03 17:00:48
?
erisco 2017-02-03 17:00:54
in fact I could have just used m <= Succ m then transitivity to get there
dfeuer 2017-02-03 17:01:00
How's that, mniip?
mniip 2017-02-03 17:01:29
hmmmm
mniip 2017-02-03 17:01:35
that's a long read
mniip 2017-02-03 17:01:40
but looks cool
jle` 2017-02-03 17:01:56
erisco: hey you can probably just do it by using the Leq GADT
dfeuer 2017-02-03 17:01:59
The real idea here is that the RTS should *actually* be calculating the "next action", driving evaluation that way,
erisco 2017-02-03 17:02:08
jle`, I just have to do it for Nat. I will try writing it inductively
geekosaur 2017-02-03 17:02:15
I think we may be stuck with unsafePerformIO anyway, unless this also finds a way to make unsafeLocalState go away
jle` 2017-02-03 17:02:18
yes Leq does it for nats
dfeuer 2017-02-03 17:02:21
rather than making that a very short-lived lie.
jle` 2017-02-03 17:02:53
erisco: \case SuccLeqSucc l -> l
dfeuer 2017-02-03 17:03:17
[or actually compiling down to something more low-level, but doing so much later in the game]
dfeuer 2017-02-03 17:03:25
Anyway, I have to try to go to sleep.
jle` 2017-02-03 17:03:59
erisco: so you can use boolToPropLeq/propToBoolLeq and then your proof is trivial
ph88 2017-02-03 17:04:29
is there a way to figure out, programatically, if the code is being run in ghci ?
erisco 2017-02-03 17:04:51
thanks I was looking for how to get :<= from Leq... what is LeqTrueInstance
jle` 2017-02-03 17:05:35
not sure, seems to not be exported
jle` 2017-02-03 17:05:40
maybe you can just use propToClassLeq then
jle` 2017-02-03 17:06:20
a bit annoying
jle` 2017-02-03 17:06:26
time to switch to idris
erisco 2017-02-03 17:07:31
I'm a little deeper than I anticipated but this is good nonetheless
jle` 2017-02-03 17:07:50
it might become clearer once you finish
jle` 2017-02-03 17:07:58
you might see a clear path to refactor
geekosaur 2017-02-03 17:10:48
ph88, nothing other than horrid hacks
geekosaur 2017-02-03 17:11:05
(like poking at /proc/self/exe on linux)
ph88 2017-02-03 17:11:16
did you see it being done before ?
jle` 2017-02-03 17:11:17
maybe check __name__
geekosaur 2017-02-03 17:13:22
ph88, you can be running compiled code in ghci or interpreted code in ghc (TH), compiled code does not know where it is running, what problem are you trying to solve? because this is probably the wrong way
ph88 2017-02-03 17:13:59
i'm doing some quickcheck and i try to adjust the amount of iterations on the speed of the code
ph88 2017-02-03 17:14:46
in ghci i can do 100 iterations reasonably fast, with compiled code 10^9
erisco 2017-02-03 17:16:13
jle`, yup this type checks http://lpaste.net/352073 is there a better way to deal with ZeroLeq?
jle` 2017-02-03 17:16:36
i'd case it
erisco 2017-02-03 17:16:54
but what is the body?
jle` 2017-02-03 17:17:40
added an annotation but
jle` 2017-02-03 17:17:55
i'm hoping that ghc desn't warn you on the ZeroLeq case
erisco 2017-02-03 17:18:10
doesn't seem to
jle` 2017-02-03 17:18:14
neat, it's smart enough
erisco 2017-02-03 17:18:25
maybe I don't have the appropriate warnings enabled
erisco 2017-02-03 17:18:30
I don't usually get partial match warnings
jle` 2017-02-03 17:18:34
o
ph88 2017-02-03 17:18:48
can haskell denote integer literals with an exponent or underscores ?
jle` 2017-02-03 17:18:51
yeah, you should turn on -Wall when doing dependent type stuff like this, that's kind of the whole point, to an extent
jle` 2017-02-03 17:19:17
partial pattern matches should probably be errors
jle` 2017-02-03 17:19:53
the magic is when you can trust ghc/the type system to know what GADT cases can't come up
dmwit 2017-02-03 17:20:22
> 1e9 :: Integer
lambdabot 2017-02-03 17:20:24
error:
lambdabot 2017-02-03 17:20:24
• No instance for (Fractional Integer)
lambdabot 2017-02-03 17:20:24
arising from the literal '1e9'
dmwit 2017-02-03 17:20:34
?let {-# LANGUAGE NumDecimals #-}
lambdabot 2017-02-03 17:20:35
Defined.
dmwit 2017-02-03 17:20:41
> 1e9 :: Integer
lambdabot 2017-02-03 17:20:43
error:
lambdabot 2017-02-03 17:20:43
• No instance for (Fractional Integer)
lambdabot 2017-02-03 17:20:43
arising from the literal '1e9'
jle` 2017-02-03 17:20:52
letting language pragmas just adds a plain ol' comment to the end of L.hs
dmwit 2017-02-03 17:21:05
ok =(
jle` 2017-02-03 17:21:09
lambdabot doesn't know to put them at the top of a file yet heh
erisco 2017-02-03 17:21:15
well then yeah it is not happy with me
erisco 2017-02-03 17:22:01
can I -Wall and disable certain warnings? like unused imports?
erisco 2017-02-03 17:22:14
I have a lot of stuff commented out as I work on this
ertes 2017-02-03 17:26:40
helo
erisco 2017-02-03 17:28:00
I guess I just write undefined for the case? seems pointless but it shuts off the warning I now have lol
erisco 2017-02-03 17:28:14
can I write anything that type checks here?
erisco 2017-02-03 17:28:39
I have to find an n such that S n ~ Z and that seems a bit difficult
erisco 2017-02-03 17:31:00
I don't even know if m is non-zero
erisco 2017-02-03 17:31:25
or I guess I don't have to for that one
erisco 2017-02-03 17:34:55
does Haskell have type inequality? maybe I can bring 'S n !~ Z into scope
mniip 2017-02-03 17:35:10
yes but it's ugly
geekosaur 2017-02-03 17:35:10
nope
geekosaur 2017-02-03 17:35:19
(well, ugly hackery aside)
mniip 2017-02-03 17:35:24
and there's not much you can reason about
geekosaur 2017-02-03 17:35:33
I seem to recall actual type inequalities cause problems
mniip 2017-02-03 17:35:41
yes
mniip 2017-02-03 17:35:57
you could have an evidence that a type family equation does not match
mniip 2017-02-03 17:36:00
with e.g.
mniip 2017-02-03 17:36:14
type family Equals x y where Equals x x = True; Equals x y = False
mniip 2017-02-03 17:36:36
but like, inference on that is going to be terrible
erisco 2017-02-03 17:36:53
('S n :== 'Z) ~ 'False perhaps
erisco 2017-02-03 17:37:11
but I don't see how Haskell is going to figure out the case is impossible from this
erisco 2017-02-03 17:37:17
if it doesn't understand inequalities in the first place
mniip 2017-02-03 17:37:19
Could not decude a ~ S b from the context (Equals a Z) ~ False
erisco 2017-02-03 17:39:17
guess I'll try and see what happens
