Cale 2017-02-19 07:45:10
bollu: limits, colimits, and adjunctions?
johnw 2017-02-19 07:53:34
bollu1: the function maybeToList can be used to create a right Kan extension that turns any a -> Maybe b into an a -> [b]. It's a simplistic example, but maybe that helps you generalize.
johnw 2017-02-19 07:59:16
here we're trivially extending the arrow's Maybe domain into the list domain; but there can be more interesting extensions: ones that are not just strict embeddings, but may involve computation to map across the functors
bollu1 2017-02-19 08:04:24
johnw: I see
bollu1 2017-02-19 08:04:45
johnw: how do we know that it is universal?
johnw 2017-02-19 08:05:05
universal in what sense?
bollu1 2017-02-19 08:06:29
johnw: in terms of the universal property?
bollu1 2017-02-19 08:06:33
the existence of the natural transformation?
johnw 2017-02-19 08:06:38
you mean, that there exists an arrow: Functor k => (forall a. k (Maybe a) -> [a]) -> k b
johnw 2017-02-19 08:06:41
?
bollu1 2017-02-19 08:06:58
yes
bollu1 2017-02-19 08:07:07
uh, I think so
johnw 2017-02-19 08:07:09
let me see
bollu1 2017-02-19 08:07:35
https://en.wikipedia.org/wiki/File:Right_Kan_extension_universal_property_diagram.PNG <- the delta_F
taktoa 2017-02-19 08:08:59
anyone know a good way to describe a smooth map / smooth manifold / lie group constructively? ideally, with laws, since I'm writing idris
bollu 2017-02-19 08:10:21
johnw: how do you encode natural transformations between Functor?
bollu 2017-02-19 08:10:25
(Hask -> Hask)
johnw 2017-02-19 08:10:30
(forall r. f r -> g r)
taktoa 2017-02-19 08:10:41
(I want to write a lie group integrator based on https://t.co/NCglhx9mNY)
bollu 2017-02-19 08:11:01
johnw: but that does not capture the commuting diagram condition. Oh, you would need dependent typing for that I assume?
johnw 2017-02-19 08:11:09
no dependent typnig
johnw 2017-02-19 08:11:12
parametricity is enough
bollu 2017-02-19 08:11:19
?
bollu 2017-02-19 08:11:25
could you elaborate on that please?
johnw 2017-02-19 08:11:27
newtype Nat f g = Nat { runNat :: forall r. f r -> g r }
taktoa 2017-02-19 08:11:40
bollu: I think he's saying it's a free theorem
bollu 2017-02-19 08:11:47
ah
bollu 2017-02-19 08:12:01
johnw: really? how is it "for free" ?
bollu 2017-02-19 08:12:07
johnw: proof, please :)
johnw 2017-02-19 08:12:31
the only thing such an arrow can do is map f to g
johnw 2017-02-19 08:12:52
it can't be affected by the "contents"
bollu 2017-02-19 08:13:04
hm
roconnor 2017-02-19 08:13:59
@free runNat :: forall r. f r -> g r
lambdabot 2017-02-19 08:13:59
Extra stuff at end of line
johnw 2017-02-19 08:14:15
bollu: https://gist.github.com/80fc71f33a4c4114578ffe9ee7d91bed
roconnor 2017-02-19 08:14:22
@free runNat :: F r -> G r
lambdabot 2017-02-19 08:14:22
$map_G f . runNat = runNat . $map_F f
bollu 2017-02-19 08:15:01
roconnor: wait, what does @free do? and that is commuting condition :O
bollu 2017-02-19 08:15:26
johnw: thank you for the gist
sternmull 2017-02-19 08:15:28
i want to use the Reader monad. When i try to import Control.Monad.Reader GHC says "It is a member of the hidden package 'mtl-...'". What am i doing wrong? Is mtl deprecated or something like that?
roconnor 2017-02-19 08:15:28
it write out the free theorem implied for parametric functions
roconnor 2017-02-19 08:15:44
@free sortBy
lambdabot 2017-02-19 08:15:47
(forall x. g x = h (f x) . f) => $map f . sortBy g = sortBy h . $map f
bollu 2017-02-19 08:15:57
johnw: what is the difference between Ran and Lan? (intuitively) I understand what happens to the diagrams
johnw 2017-02-19 08:16:15
bollu: the direction that the functor is "pulled"
roconnor 2017-02-19 08:17:11
(forall x y. g x y = h (f x) (f y)) => $map f . sortBy g = sortBy h . $map f is the ususal way to write that.
maksim__ 2017-02-19 08:20:00
is there a way in ghci to define a colon command that does step and then list
roconnor 2017-02-19 08:20:35
sternmull: definitely not depricated.
sternmull 2017-02-19 08:21:01
roconnor: But what package to i need to import Control.Monad.Reader?
roconnor 2017-02-19 08:21:43
for the monad itself you need transformers. for the class you need mtl, which depends on transformers
johnw 2017-02-19 08:23:14
bollu: try https://www.quora.com/What-is-a-laymans-explanation-of-Kan-extensions
sternmull 2017-02-19 08:23:16
when i have mtl and transformers it works. How do i find out what i need on my own?
johnw 2017-02-19 08:23:42
I like Rúnar's analogy
bollu 2017-02-19 08:23:52
johnwty
bollu 2017-02-19 08:23:54
johnw: ty
johnw 2017-02-19 08:25:29
bollu: also note how my pastie involves the "limit" of the list functor, []
johnw 2017-02-19 08:25:49
without that limit, I couldn't have written the function
johnw 2017-02-19 08:26:20
more on this at: http://comonad.com/reader/2008/kan-extensions/
bollu 2017-02-19 08:26:28
johnw: thanks
bollu 2017-02-19 08:26:39
johnw: "limit" with respect to what diagram?
johnw 2017-02-19 08:26:58
i wasn't thinking of any diagram
johnw 2017-02-19 08:27:06
just the limit of the functor []
bollu 2017-02-19 08:27:30
johnw: OK, limit of [] as a functor from a -> [a] ?
johnw 2017-02-19 08:27:36
yes
maksim__ 2017-02-19 08:27:48
what am i doing wrong? *Main> :show modules
maksim__ 2017-02-19 08:27:48
Databrary.Setup.Git ( Databrary/Setup/Git.hs, interpreted )
maksim__ 2017-02-19 08:27:48
Databrary.Setup.Node ( Databrary/Setup/Node.hs, interpreted )
maksim__ 2017-02-19 08:27:48
Main ( Setup.hs, interpreted )
maksim__ 2017-02-19 08:27:48
*Main> :break Main
maksim__ 2017-02-19 08:27:49
johnw 2017-02-19 08:27:56
or as edwardk once asked me, what value has the type forall a. [a]
maksim__ 2017-02-19 08:28:00
whoops
bollu 2017-02-19 08:28:11
johnw: okay, the way I know to think of a limit is as the final object in the category of cones of [], right?
maksim__ 2017-02-19 08:28:17
i would like to break on some line of Main or Setup.hs
bollu 2017-02-19 08:28:19
johnw: but, like, how do I visualise "cones of []"?
johnw 2017-02-19 08:28:25
bollu: i don't know, I'm unfamiliar with cones
bollu 2017-02-19 08:28:29
johnw: OK
bollu 2017-02-19 08:28:37
johnw: what is your intuition of limit?
bollu 2017-02-19 08:28:48
johnw: mine is that, if you have a limit of a functor F: J -> C
bollu 2017-02-19 08:28:58
you will get the "most general image" of F in C
bollu 2017-02-19 08:29:04
of J in C* wrt F
bollu 2017-02-19 08:29:18
in the sense that, any other image of the functor will have a unique mapping onto the limit
bollu 2017-02-19 08:29:19
right?
johnw 2017-02-19 08:29:32
I don't follow, sorry
bollu 2017-02-19 08:29:56
johnw: OK, can you explain to me your intuition of a limit? I could be wrong :)
johnw 2017-02-19 08:31:20
now that you ask, I do not know; thanks for adding to my reading list :)
johnw 2017-02-19 08:31:34
https://bartoszmilewski.com/2014/05/08/understanding-limits-2/
johnw 2017-02-19 08:32:25
my "coding" intuition is that the limit of f is a value that solves forall a. f a
bollu 2017-02-19 08:32:28
johnw: :)
bollu 2017-02-19 08:32:34
johnw: oh, that is interesting
johnw 2017-02-19 08:32:59
so the limit of Maybe is Nothing, the limit of Const a is any a, etc.
bollu 2017-02-19 08:33:04
ahh
orion_ 2017-02-19 08:33:36
https://www.youtube.com/watch?v=sUIcCyPOA30
orion_ 2017-02-19 08:33:41
The Elite are all about transcendence and living forever and the secrets of the universe and they want to know all this; some are good, some are bad, some are mixed. But, the good ones don't ever want to organise, the bad instead are the ones that organise, because they lust after power. Powerful consciousnesses don't want to dominate other people, they want to empower them, so they don't tend to
orion_ 2017-02-19 08:33:47
get together until things are really late in the game, then they come together. Evil is always defeated, because good is so much stronger. And, we're on this planet and Einstein's physics showed it, Maxwell's physics showed it, all of it, that there is at least twelve dimensions, and now that's why all the top scientist and billionaires are coming out saying it's a false hologram, it is
orion_ 2017-02-19 08:33:54
artificial. The computers are scanning it and finding tensions points where it is artificially projected and gravity is bleeding in to this universe, that's what they call dark matter. So, we're like a thought or a dream that's like a wisp in some computer program, some god's mind, whatever. They're proving it all, it's all coming out.
johnw 2017-02-19 08:33:59
orion_: ok, why shouldn't I ban you :)
Akii 2017-02-19 08:35:02
johnw: good soundtrack on the video
Akii 2017-02-19 08:35:16
sad that some guy is talking over it though
Zyxoas 2017-02-19 08:36:07
Hey, y'all.
Zyxoas 2017-02-19 08:36:17
I have a very quick lens question...
Zyxoas 2017-02-19 08:36:25
Or rather, aeson-lens...
johnw 2017-02-19 08:36:29
Zyxoas: you have 1 second to ask
Zyxoas 2017-02-19 08:36:46
Haha @ johnw
Akii 2017-02-19 08:36:52
too late, next
Akii 2017-02-19 08:36:57
:D
bollu 2017-02-19 08:37:18
johnw: where did you get your idea of limit from?
johnw 2017-02-19 08:37:24
bollu: edwardk
johnw 2017-02-19 08:37:50
if he weren't recuperating from surgery still, he'd be here to tell you himself
bollu 2017-02-19 08:37:58
johnw: I see
Zyxoas 2017-02-19 08:38:03
Basically, the JSON looks something like this "{ dudes: [ {name : foo, surname : meister}, {name : bar, surname : ness} ]}"
Zyxoas 2017-02-19 08:38:35
I need to write an aeson lens which gives me a list [(foo, meister), (bar, ness)]
Zyxoas 2017-02-19 08:39:12
I can do ^? dudes, to get an Aeson Array, but then I get stuck a little...
Zyxoas 2017-02-19 08:39:31
I mean ^? key "dudes"
Zyxoas 2017-02-19 08:40:25
So, I just wanna extract a list of properties from a deeply embeded list of objects, and hopefully extract both properties at the same time...
Zyxoas 2017-02-19 08:41:59
That is, how do I compose ^.. with ^. (or, better yet, ^.. with ^?)??
Zyxoas 2017-02-19 08:43:04
And then, combine two lenses with the (,) function...
