AbelianGrape 2017-02-22 10:47:54
GHC Isn't allowed to assume that a == a, right? That is, it can't assume that if the two arguments to (==) are the same in-memory object, they're equal?
ezyang 2017-02-22 10:48:09
AbelianGrape: GHC is not allowed to assume this
AbelianGrape 2017-02-22 10:48:38
Ok, cool. It would be interesting to have a set of extensions that lets GHC assume you've followed various typeclass laws
AbelianGrape 2017-02-22 10:48:48
You could get a big performance boost for some things, I imagine
ezyang 2017-02-22 10:48:54
well, you can kind of do this with rewrite rules
ezyang 2017-02-22 10:49:02
but you need to define a confluent rewriting system that is profitable
AbelianGrape 2017-02-22 10:49:51
I was thinking more along the lines of Eq/Ord laws than Applicative/Monad laws
AbelianGrape 2017-02-22 10:50:11
Like, if you have a huge object, you can do a cheap pointer equality check before doing the actual equality check
AbelianGrape 2017-02-22 10:50:50
Could save a lot of time for some use cases with strings, vectors, etc
AbelianGrape 2017-02-22 10:51:08
Obviously not a good idea from a theoretical standpoint though
ski 2017-02-22 10:51:35
AbelianGrape : i'd expect `forall a b. a == b = True => a = b' (observationally speaking), though
AbelianGrape 2017-02-22 10:51:47
Yeah, of course
ski 2017-02-22 10:52:20
some memo-libs do that cheap pointer equality check
ski 2017-02-22 10:52:59
(and `forall a b. a == b = False => a =/= b'. howver not the converses of either, since inputs can be partial or infinite)
AbelianGrape 2017-02-22 10:53:12
What was that extension someone published a few days ago with the ===? You could have GHC prove `(\a -> a == a) === const True` and then it would be safe
AbelianGrape 2017-02-22 10:53:42
Probably wouldn't work for anything complicated though
dmwit 2017-02-22 10:55:25
AbelianGrape: Doing a pointer equality check would change the semantics of `(==)`, though, so that's a potentially scary thing to allow.
dmwit 2017-02-22 10:56:23
AbelianGrape: e.g. `let x = repeat 0 in x == x` could suddenly start terminating, which might be odd, and also wouldn't guarantee that `x` had been fully evaluated as it used to do, which could lead to a memory leak.
dmwit 2017-02-22 10:57:07
(Even in the simpler situation where both would terminate the latter fact is a bit worrisome.)
AbelianGrape 2017-02-22 10:59:47
Good point
AbelianGrape 2017-02-22 11:03:13
ski, someone wrote a library that uses GHC's simplification machinery to write proofs of laws
AbelianGrape 2017-02-22 11:03:26
it never makes a false proof, but isn't guaranteed to find a proof (of course)
AbelianGrape 2017-02-22 11:03:31
Let me look for it
ski 2017-02-22 11:03:35
what's the type of `(===)' ?
Tuplanolla 2017-02-22 11:03:45
https://github.com/nomeata/ghc-proofs
AbelianGrape 2017-02-22 11:03:53
a -> a -> () iirc
AbelianGrape 2017-02-22 11:04:01
Yeah that
AbelianGrape 2017-02-22 11:04:04
's it Tuplanolla
ski 2017-02-22 11:04:41
ty
AbelianGrape 2017-02-22 11:04:44
It works well for simple monads and stuff, pretty cool
dmwit 2017-02-22 11:06:42
"Proof" is a funny name for this.
erisco 2017-02-22 11:07:03
Koterpillar, that is not a counter-example
dmwit 2017-02-22 11:07:12
I mean. I guess it's an okay name. But it's not proof of equality in the usual domain we think of; it's proof of equality in GHC's rewrite system.
Koterpillar 2017-02-22 11:07:36
erisco: elemIndex? It should have returned Nothing
ski 2017-02-22 11:07:38
a proof that GHC's rewrite rules believes they are equal
erisco 2017-02-22 11:07:50
that wasn't the whole solution. It didn't even have the correct type! I was just showing the crux of the solution
dmwit 2017-02-22 11:07:56
ski: right
erisco 2017-02-22 11:07:59
you would do a bounds check before that
mikail 2017-02-22 11:10:07
I am looking at monad transformers at the moment and have heard that they can be used to structure programs. Before I jump down a rabbit hole and look into this more deeply, is this the right intuition?
Koterpillar 2017-02-22 11:10:21
a lot of things can be used to structure programs
ezyang 2017-02-22 11:10:24
it depends on what you mean by "structure programs"
ezyang 2017-02-22 11:10:38
My intuition is that monad transformers are a way of making monads
Zemyla 2017-02-22 11:10:48
UML can theoretically be used to structure programs, so that's not a very good benchmark.
dmwit 2017-02-22 11:10:49
I think you should jump.
dmwit 2017-02-22 11:11:37
Also, I don't think that's the right intuition. Also I don't think it's possible to have the right intuition before you jump, even if you say the exact same words somebody who has already jumped says.
mikail 2017-02-22 11:13:29
I'm going by this video: https://www.youtube.com/watch?v=8t8fjkISjus&list=WL&index=2
mikail 2017-02-22 11:14:51
In this presentation, he has an example where he has layered application (see 5:59) and then represents that by stacking his monads appropriately
Zemyla 2017-02-22 11:15:21
Why is there a package called ChasingBottoms on hackage where children can see it?
mniip 2017-02-22 11:16:10
is that a serious question
Zemyla 2017-02-22 11:16:20
No it isn't.
Zemyla 2017-02-22 11:16:58
But the package page talking about "getting a grip on bottoms" can't be accidental.
Zemyla 2017-02-22 11:31:09
Also, I can't test or benchmark the latest build of containers from GitHub, because the test and bench tools themselves require containers.
Zemyla 2017-02-22 11:32:57
How do I break the dependency cycle?
ezyang 2017-02-22 11:33:46
Zemyla: https://github.com/haskell/cabal/issues/1575
mbrock 2017-02-22 11:39:58
mikail: right now I'm working on a program where many operations share similar aspects: they access a state, they emit log events, and they can fail causing rollback in the other aspects. This kind of operation can be written naturally as functions of some type like "input -> state -> Maybe (output, state, [log])" or something like that. It turns out that
mbrock 2017-02-22 11:39:58
all these three aspects are common patterns that fit into the monad pattern. Monad transformers let me compose them together nicely
suppi 2017-02-22 11:40:18
is it possible to convert turtle's FilePath to String?
sdx23 2017-02-22 11:41:32
suppi: the common FilePath is String.
suppi 2017-02-22 11:41:58
sdx23: turtle's FilePath is not a String though, that's my problem :\
Tuplanolla 2017-02-22 11:42:17
@hackage turtle
lambdabot 2017-02-22 11:42:17
http://hackage.haskell.org/package/turtle
suppi 2017-02-22 11:42:56
it uses this specifically: http://hackage.haskell.org/package/system-filepath-0.4.13.4/docs/Filesystem-Path.html#t:FilePath
suppi 2017-02-22 11:43:10
sorry for not linking that earlier.
sdx23 2017-02-22 11:43:50
that is both IsString and Show
