mniip 2017-02-03 05:45:33
hey Cale
mniip 2017-02-03 05:46:36
hmm
reactormonk 2017-02-03 05:47:11
Gurkenglas, so use the prism for the Either on checking if it would be a valid lens?
Taneb 2017-02-03 05:48:13
reactormonk, a Lens must obey the law view l (set l x) = x
Gurkenglas 2017-02-03 05:48:18
reactormonk, you mean "Either e a -> Lens' s a -> t -> s -> s"?
Gurkenglas 2017-02-03 05:48:36
um
Gurkenglas 2017-02-03 05:48:44
"Either e a -> Lens' s a -> s -> s"
mniip 2017-02-03 05:49:06
does anyone know what does the Arrow typeclass represent in CT?
Cale 2017-02-03 05:49:45
mniip: hi
Gurkenglas 2017-02-03 05:49:58
You might even say "Maybe a -> a -> a" :P
mniip 2017-02-03 05:49:58
it appears that &&& is the mediating morphism of the binary product in the category, and then first/second/*** are built from it and projections
Cale 2017-02-03 05:49:59
mniip: It's sorta kinda like the definition of a symmetric monoidal category
reactormonk 2017-02-03 05:49:59
Taneb, yeah, that's not the problem. However, it's possible to have x which can't be set.
mniip 2017-02-03 05:50:20
but then I'm not sure why 'arr' which is a kind of inverse of a forgetful functor is in the class
Cale 2017-02-03 05:50:44
Yeah, arr doesn't really fit in with that description
Taneb 2017-02-03 05:50:57
reactormonk, if set l x silently fails, then view l (set l x) will not be x
mniip 2017-02-03 05:51:00
and then ArrowChoice implements the comediating morphism to the binary coproduct
Taneb 2017-02-03 05:51:07
reactormonk, so you don't have a lens
mniip 2017-02-03 05:51:10
and it's a subclass of Arrow which makes no sense again
Tuplanolla 2017-02-03 05:51:17
Didn't Conal have arrows without `arr`?
Gurkenglas 2017-02-03 05:51:17
reactormonk, afaik you'll just have to use or not use set depending on whether x is valid
dolio 2017-02-03 05:51:35
Arrows are strong monads in a 2-category involving profunctors instead of functors.
dolio 2017-02-03 05:51:41
Or something along those lines.
Gurkenglas 2017-02-03 05:51:43
Which you can do by turning x into Maybe a and then using the maybe id const thing from earlier :D
Cale 2017-02-03 05:51:48
Yeah, there's that description...
dolio 2017-02-03 05:51:57
It's the correct one. :)
Cale 2017-02-03 05:52:32
I don't know about Conal, but back when Ryan and I were working on AFRP for our game, we ended up making the Arrow class hierarchy reflect the definition of a symmetric monoidal category better
Cale 2017-02-03 05:52:57
and for instance, arr went off into its own subclass
dolio 2017-02-03 05:52:57
Cale: Right, you want arrows to be soemthing better. :)
Cale 2017-02-03 05:53:24
Well, yeah. They pretty much undermine all their own best usecases as it stands.
reactormonk 2017-02-03 05:53:34
Gurkenglas, which I could turn into a Prism as well, with the error message.
reactormonk 2017-02-03 05:54:02
I'm wondering if there's another type which allows me to encode that only one way might fail, and the other is fine.
Gurkenglas 2017-02-03 05:54:16
Will the one way always fail?
reactormonk 2017-02-03 05:54:39
No, it can.
reactormonk 2017-02-03 05:55:19
Request => URI is always valid. URI => Request is not. Prism URI (Either Err Request) from what I understand.
dolio 2017-02-03 05:55:28
reactormonk: You can't make a lens that fails to set. People have tried, I think, calling them stuff like, 'partial lenses,' but you end up not being able to specify nice things about them the way you can with lenses, as I recall.
Taneb 2017-02-03 05:55:48
reactormonk, why not Prism' URI Request
reactormonk 2017-02-03 05:56:00
Taneb, let's go with that.
mniip 2017-02-03 05:56:02
dolio, ok, let's dissect that one
mniip 2017-02-03 05:56:08
which 2-category are we talking
reactormonk 2017-02-03 05:56:30
ah nice, Prism looks pretty reasonable.
dolio 2017-02-03 05:56:33
mniip: Let's not do that. Instead, let's think about switching the monad definition to profunctors.
mniip 2017-02-03 05:57:10
eh
dolio 2017-02-03 05:57:34
The identity profunctor is (->), and profunctor composition is: (F . G)(x,y) = exists e. F x e * G e y
lpaste_ 2017-02-03 05:58:05
chrisdone pasted "Testing paste announcement on DigitalOcean" at http://lpaste.net/352059
dolio 2017-02-03 05:58:47
So if you just take the definition of monad and swap 'profunctor' for 'functor', (->) for identity functor, and profunctor composition for functor composition...
mniip 2017-02-03 05:59:01
dolio, you mean the hom(-, -) profunctor into Set, or the internal hom endo-profunctor?
dolio 2017-02-03 05:59:27
hom, profunctors in category theory all go into Set.
mniip 2017-02-03 05:59:37
okee
dolio 2017-02-03 06:00:15
You'll notice: eta : hom(-,-) -> M is hom(x,y) -> M(x,y).
dolio 2017-02-03 06:00:19
Which is arr.
ARTF2 2017-02-03 06:00:44
hi
mniip 2017-02-03 06:00:50
wait
mniip 2017-02-03 06:00:58
what is a natural transformation on a profunctor?
ARTF2 2017-02-03 06:00:58
wha?
dolio 2017-02-03 06:01:08
Just a point-wise natural transformation.
mniip 2017-02-03 06:01:13
just NT on like a regular functor?
mniip 2017-02-03 06:01:29
treating profunctor as a (- x -) ---> - functor?
mniip 2017-02-03 06:01:45
ok
dolio 2017-02-03 06:01:52
As D^op x C -> Set, yes.
mniip 2017-02-03 06:02:19
hm, this might be easier to imagine if we construct the category of profunctors
mniip 2017-02-03 06:02:25
and examine monoids under composition
dolio 2017-02-03 06:02:39
In this case it's C^op x C -> Set, I guess, because it has to be an endo-profunctor, like a monad is an endofunctor.
Jinixt 2017-02-03 06:02:47
anyone used llvm-general for llvm ir generation? is it any good?
mniip 2017-02-03 06:02:59
ok so, what's the composition again?
dolio 2017-02-03 06:03:28
(F . G)(x,y) = exists e. F(x, e) * G(e, y)
mniip 2017-02-03 06:03:59
* being the binary product in Set?
dolio 2017-02-03 06:04:00
I think, at least. I might have things swizzled around.
dolio 2017-02-03 06:04:03
Yeah.
mniip 2017-02-03 06:04:54
how do you propose we impose equality on profunctors to warrant that F . G == F . G?
dolio 2017-02-03 06:05:10
So mu in the monad is going to look like: forall a c. (exists b. M(a,b) * M(b,c)) -> M(a,c)
dolio 2017-02-03 06:06:08
I don't understand your question.
mniip 2017-02-03 06:06:27
you define profunctor composition nonconstructively
dolio 2017-02-03 06:06:38
exists is the Haskell-like exists.
dolio 2017-02-03 06:06:48
In category theory it'd be a coend.
mniip 2017-02-03 06:07:25
so a sum over all possible e's?
dolio 2017-02-03 06:07:30
Yeah.
mniip 2017-02-03 06:07:42
I need to think about that
e 2017-02-03 06:07:52
there is only one possible e, thank you
dolio 2017-02-03 06:08:03
Yeah, good choice of name. :)
mniip 2017-02-03 06:08:22
e: go back into Set
Forty-Bot 2017-02-03 06:08:31
I've created an implementation of in haskell: https://gist.github.com/anonymous/81000a73ba2604964d870ed089498e14
e 2017-02-03 06:08:35
haha
mniip 2017-02-03 06:08:57
no wait, actually, e is in C, and the *sum* is over Set
Forty-Bot 2017-02-03 06:09:01
I'm not a very experienced haskeller, so I'd appreciate some feedback on if stuff isn't idiomatic
noan 2017-02-03 06:09:54
Oh god baby's first haskell. I'm sitting here staring at IO UTCTime and trying to figure out how to Construct a IO SessionToken { String, UTCTime } out of it
dolio 2017-02-03 06:09:57
mniip: One thing to think about is turning functors into profunctors. Like if F is a functor (- -> F=) is a profunctor. And if you do (exists e. (- -> Fe) * (e -> G=)), you can massage that into (- -> FG=).
noan 2017-02-03 06:09:58
baby's first monad please
noan 2017-02-03 06:10:00
XD
Forty-Bot 2017-02-03 06:10:09
I'm also not sure which bits should be inlined; I've based it mostly off of Number.Complex, but I haven't figured out a general rule for that
mniip 2017-02-03 06:10:42
noan, do x <- ioutctime; return $ SessionToken string x
mniip 2017-02-03 06:10:45
if all else fails
dolio 2017-02-03 06:10:52
So composing two profunctors built that way out of functors is equivalent to building a profunctor out of the functor composition.
mniip 2017-02-03 06:11:20
dolio, I don't understand the notation of (- -> F=)
dolio 2017-02-03 06:11:55
Star f x y = x -> f y
dolio 2017-02-03 06:12:13
Star f . Star g ~ Star (f . g)
dolio 2017-02-03 06:12:55
Where the left side is profunctor composition and the right side is functor composition.
mniip 2017-02-03 06:13:20
wait
mniip 2017-02-03 06:14:29
I can't see how id_X . id_X would be equal to id_X
spatial 2017-02-03 06:14:46
Anyone can point out some tutorial to get started with Spock. I use spacemacs
dolio 2017-02-03 06:14:47
They're isomorphic.
mniip 2017-02-03 06:14:49
hence again, how do we equate profunctors
dolio 2017-02-03 06:15:17
Wait, id_X?
mniip 2017-02-03 06:15:28
er
mniip 2017-02-03 06:15:33
yes, id(X, X)
mniip 2017-02-03 06:15:53
eh
mniip 2017-02-03 06:15:55
no not that either
dolio 2017-02-03 06:16:03
You mean the identity profunctor (hom)?
mniip 2017-02-03 06:16:38
yes that's what I mean
dolio 2017-02-03 06:16:51
So, if you have F(x,y) and hom(y,z) you can use the fact that you can use covariant mapping to turn that into F(x,z).
dolio 2017-02-03 06:17:57
And if you have hom(z,x) and F(x,y) you can turn that into F(z,y).
mniip 2017-02-03 06:19:02
hom(x, y) is the set of all morphisms from x to y, (hom . hom)(x, y) is the disjoin union of (set of morphisms from x to e, set of morphisms from e to y) for every e in C
mniip 2017-02-03 06:19:07
how do you propose we equate the two
mniip 2017-02-03 06:20:13
doesn't sound very isomorphic to me tbf
dolio 2017-02-03 06:21:22
To go from (exists e. hom(x,e) * hom(e, y)) to hom(x,y) you compose the two arrows.
dolio 2017-02-03 06:22:00
To go from hom(x,y) to (exists e. hom(x,e) * hom(e, y)) you pair the arrow you have with either the identity-on-x or identity-on-y.
dolio 2017-02-03 06:22:15
Depending on whether you choose e = x or e = y.
dolio 2017-02-03 06:22:59
And that's an isomorphism because while 'disjoint union' is the right kind of intuition, it's not perfectly accurate.
dolio 2017-02-03 06:23:57
It's more like a disjoint union quotiented by the fact where you sort of forget about exactly what 'e' you picked.
mniip 2017-02-03 06:24:35
okay that kinda makes sense
mniip 2017-02-03 06:24:46
though, hom is a set not a morphism
dolio 2017-02-03 06:25:10
It's the set of arrows.
mniip 2017-02-03 06:25:24
1486142483 [20:21:23] To go from (exists e. hom(x,e) * hom(e, y)) to hom(x,y) you compose the two arrows.
dolio 2017-02-03 06:25:35
To give an isomorphism, you explain how to map between the values of the two sets.
dolio 2017-02-03 06:25:50
And then prove that the mappings are inverses.
mniip 2017-02-03 06:26:42
your explanation doesn't sound correct but I think I figured it out anyway
dolio 2017-02-03 06:26:55
Okay. :)
oz_ 2017-02-03 06:28:08
hello
mniip 2017-02-03 06:28:10
o
mniip 2017-02-03 06:28:18
I forgot one important detail
oz_ 2017-02-03 06:28:31
where am i
mniip 2017-02-03 06:28:34
it's not a pair of sets, it's a cartesian product
dolio 2017-02-03 06:28:42
Yeah.
mniip 2017-02-03 06:28:43
oz_, this is #haskell on freenode
dolio 2017-02-03 06:28:56
Values are pairs of arrows.
oz_ 2017-02-03 06:31:21
thank you! i was trying to find #cicadian but have had no luck
sm 2017-02-03 06:31:31
oz_: on the internet. planet earth, sol system.
mniip 2017-02-03 06:31:46
oz_, /join #cicadian
Forty-Bot 2017-02-03 06:35:48
does anyone have feedback on the comments in https://gist.github.com/anonymous/81000a73ba2604964d870ed089498e14 ?
spatial 2017-02-03 06:44:32
Any tutorial explains how to use Spock. I have spacemacs.
