Home freenode/#haskell: Logs Calendar

Logs: freenode/#haskell

←Prev  Next→
Page 1 .. 681 682 683 684 685 686 687 688 689 690 691 .. 5022
— 502,152 events total
2020-10-16 19:00:25 <larou> but its still "data" as opposed to "codata"
2020-10-16 19:00:30 <larou> whatever that is...
2020-10-16 19:01:05 <larou> list is both isnt it, both foldable and unfoldable...
2020-10-16 19:01:07 <monochrom> > unfoldr (\s -> if s==10 then Nothing else Just (even s, s+1)) 0
2020-10-16 19:01:10 <lambdabot> [True,False,True,False,True,False,True,False,True,False]
2020-10-16 19:01:35 → pjb joins (~t@2a01cb04063ec50091a4fa1f69281349.ipv6.abo.wanadoo.fr)
2020-10-16 19:02:07 <larou> and what about Free cf. Free Monads, for Free f, where f is a Functor
2020-10-16 19:02:08 <monochrom> My example can be narrated as: I have an internal state, initially 0. If the state value hits 10, end; else, emit one more message "even s" and the next state is s+1.
2020-10-16 19:02:28 <zincy__> So is this kinda like - machines produce data and unfoldr is our machine and lists are data?
2020-10-16 19:02:40 <larou> (monoids in the category of endofunctors.... algebra?)
2020-10-16 19:02:40 <monochrom> So I have a little automaton that has an internal state and emits messages accordingly for several steps.
2020-10-16 19:02:47 <monochrom> Yes
2020-10-16 19:02:51 <zincy__> Oh cool
2020-10-16 19:03:05 <larou> :t build
2020-10-16 19:03:07 <lambdabot> error:
2020-10-16 19:03:07 <lambdabot> • Variable not in scope: build
2020-10-16 19:03:07 <lambdabot> • Perhaps you meant ‘buildG’ (imported from Data.Graph)
2020-10-16 19:03:15 × berberman_ quits (~berberman@unaffiliated/berberman) (Ping timeout: 272 seconds)
2020-10-16 19:03:31 → berberman joins (~berberman@unaffiliated/berberman)
2020-10-16 19:03:44 <larou> :t \f -> foldr f (:) []
2020-10-16 19:03:45 <lambdabot> (a1 -> (a2 -> [a2] -> [a2]) -> a2 -> [a2] -> [a2]) -> a2 -> [a2] -> [a2]
2020-10-16 19:04:03 <larou> oh no, i got that very wrong...
2020-10-16 19:04:37 <larou> but like "unfold" isnt the machine... nor is the argument to it. its both the unfold and its argument, that produces the list
2020-10-16 19:04:44 <larou> :t unfoldr
2020-10-16 19:04:45 <lambdabot> (b -> Maybe (a, b)) -> b -> [a]
2020-10-16 19:05:04 <larou> so i guess its just anything thats (b -> [a])
2020-10-16 19:05:25 <larou> ah, i was thinking of Church encoding, not build
2020-10-16 19:05:30 <larou> like, a partially applied fold
2020-10-16 19:05:49 <larou> :t foldr undefined
2020-10-16 19:05:50 <lambdabot> Foldable t => b -> t a -> b
2020-10-16 19:06:06 → boo joins (d03b9e15@208.59.158.21)
2020-10-16 19:06:08 <larou> oh, i guess it needs the initial data too...
2020-10-16 19:06:12 <larou> :t foldr undefined undefined
2020-10-16 19:06:13 <lambdabot> Foldable t => t a -> b
2020-10-16 19:06:25 × xerox_ quits (~xerox@unaffiliated/xerox) (Ping timeout: 240 seconds)
2020-10-16 19:06:37 boo is now known as Guest98072
2020-10-16 19:06:38 <monochrom> larou, you're being anal about "unfoldr is the machine". Clearly, you could have also picked on "the State monad" --- there is no State monad, you always have to pick a type T and say "the State T monad".
2020-10-16 19:06:38 <larou> which is dual to (b -> t a) from the partially applied unfold
2020-10-16 19:07:08 × Franciman quits (~francesco@host-82-48-166-25.retail.telecomitalia.it) (Ping timeout: 260 seconds)
2020-10-16 19:07:35 <larou> well, just considering; f a -> b, and b -> f a, its clear one of them produces data and one of them consumes it
2020-10-16 19:07:42 × thir quits (~thir@p200300f27f02580074cf2a3fa9ab5ee7.dip0.t-ipconnect.de) (Ping timeout: 260 seconds)
2020-10-16 19:08:33 <larou> anyway, where does the "adjoint" enter?
2020-10-16 19:08:41 <larou> its supposed to generalise over this right/
2020-10-16 19:09:42 × nineonine quits (~nineonine@50.216.62.2) (Ping timeout: 272 seconds)
2020-10-16 19:10:01 <monochrom> There is a URL, you could use it.
2020-10-16 19:10:28 × Rudd0 quits (~Rudd0@185.189.115.108) (Ping timeout: 256 seconds)
2020-10-16 19:11:01 <monochrom> Like I said the value of your messages is dropping under 0.
2020-10-16 19:11:13 <larou> nice summary
2020-10-16 19:11:35 × gehmehgeh quits (~ircuser1@gateway/tor-sasl/gehmehgeh) (Remote host closed the connection)
2020-10-16 19:12:21 <larou> can you explain though? i dont know enough theory to understand this paper...
2020-10-16 19:12:53 <larou> some vague intuition to serve as a foundation to grasp at the abstract concepts?
2020-10-16 19:13:03 → kenran joins (~maier@b2b-37-24-119-190.unitymedia.biz)
2020-10-16 19:13:22 <monochrom> Learn adjoint functors, then?
2020-10-16 19:13:33 <larou> what are those for?
2020-10-16 19:13:33 → xerox_ joins (~xerox@unaffiliated/xerox)
2020-10-16 19:13:39 <monochrom> Adjunction itself takes a while to learn already.
2020-10-16 19:13:47 <monochrom> For reading Hinze's paper?
2020-10-16 19:13:52 <larou> ...
2020-10-16 19:14:16 <monochrom> I certainly avoided learning adjunction until I found Hinze's paper. I learned adjunction for it.
2020-10-16 19:14:35 <larou> ah, that must have given you the ability to explain it in less technical terms!
2020-10-16 19:14:40 <monochrom> It's a good enough justification for me.
2020-10-16 19:15:03 <monochrom> Do I owe you something?
2020-10-16 19:15:48 → nineonine joins (~nineonine@50.216.62.2)
2020-10-16 19:16:01 <larou> its like Kan extensions, there is this commuting diagram
2020-10-16 19:16:07 <larou> ok....
2020-10-16 19:17:38 × kenran quits (~maier@b2b-37-24-119-190.unitymedia.biz) (Ping timeout: 265 seconds)
2020-10-16 19:18:48 × wroathe quits (~wroathe@75-146-43-37-Minnesota.hfc.comcastbusiness.net) (Ping timeout: 260 seconds)
2020-10-16 19:18:56 → kenran joins (~maier@87.123.205.83)
2020-10-16 19:20:36 × conal quits (~conal@64.71.133.70) (Quit: Computer has gone to sleep.)
2020-10-16 19:20:37 → mirrorbird joins (~psutcliff@m83-187-163-53.cust.tele2.se)
2020-10-16 19:21:54 → gehmehgeh joins (~ircuser1@gateway/tor-sasl/gehmehgeh)
2020-10-16 19:22:55 <larou> so we have datatypes as the fixed points of base functors...
2020-10-16 19:24:18 <larou> F(uF) = uF
2020-10-16 19:24:36 → conal joins (~conal@64.71.133.70)
2020-10-16 19:25:03 <larou> vF = F(vF)
2020-10-16 19:25:08 → wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net)
2020-10-16 19:25:18 <larou> those cant be equals signs, they must be some kind of arrow
2020-10-16 19:25:41 <larou> thats like monoids in endofunctors by the looks of it
2020-10-16 19:25:50 <larou> or comonoids... for the dual
2020-10-16 19:26:58 hackage silkscreen 0.0.0.3 - Prettyprinting transformers. https://hackage.haskell.org/package/silkscreen-0.0.0.3 (robrix)
2020-10-16 19:27:08 <larou> it says that in haskell, the inductive and coinductive data coincide, unlike Charity or Coq
2020-10-16 19:28:08 <larou> (since we can pattern match on the constructor - foldables are unfoldables?)
2020-10-16 19:30:05 × dhil quits (~dhil@195.213.192.122) (Ping timeout: 240 seconds)
2020-10-16 19:30:19 <larou> it references this; https://www.cs.tufts.edu/~nr/cs257/archive/tim-sheard/two-level-unification.pdf
2020-10-16 19:31:03 <larou> "The first of these is the definition of recursive
2020-10-16 19:31:03 <larou> data types using two levels: a structure defining level, and
2020-10-16 19:31:04 <larou> a recursive knot-tying level"
2020-10-16 19:31:14 <larou> woop woop!
2020-10-16 19:31:33 × conal quits (~conal@64.71.133.70) (Quit: Computer has gone to sleep.)
2020-10-16 19:31:54 × tensorpudding quits (~michael@unaffiliated/tensorpudding) (Quit: ZNC - http://znc.in)
2020-10-16 19:32:45 × ephemera_ quits (~E@122.34.1.187) (Remote host closed the connection)
2020-10-16 19:34:03 → ephemera_ joins (~E@122.34.1.187)
2020-10-16 19:34:14 → conal joins (~conal@64.71.133.70)
2020-10-16 19:34:34 <larou> hmm, then it says something about termination. seems like folds need to terminate, so inductive data is finite - while unfolds are potentially infinite
2020-10-16 19:34:43 <larou> i guess thats why we have lazy evaluation
2020-10-16 19:36:54 <monochrom> Haha "class Pretty a" "Overloaded conversion to Doc." "Laws: 1. output should be pretty. :-)"
2020-10-16 19:37:10 × fragamus quits (~michaelgo@73.93.153.117) (Ping timeout: 256 seconds)
2020-10-16 19:37:12 <dsal> *objectively*
2020-10-16 19:39:10 <larou> argh! then it does trees as mutually recursive base functors as a categorical product
2020-10-16 19:41:07 <larou> it says " Haskell has no concept of pairs on the type level, that is, no product
←Prev  Next→
Page 1 .. 681 682 683 684 685 686 687 688 689 690 691 .. 5022

All times are in UTC.