Home freenode/#haskell: Logs Calendar

Logs: freenode/#haskell

←Prev  Next→
Page 1 .. 127 128 129 130 131 132 133 134 135 136 137 .. 5022
— 502,152 events total
2020-09-22 04:26:21 × abhixec quits (~abhixec@c-67-169-141-95.hsd1.ca.comcast.net) (Quit: leaving)
2020-09-22 04:26:49 × dead10cc quits (63f22acf@gateway/web/cgi-irc/kiwiirc.com/ip.99.242.42.207) (Quit: Connection closed)
2020-09-22 04:26:55 × dolio quits (~dolio@haskell/developer/dolio) (Read error: Connection reset by peer)
2020-09-22 04:27:03 <edwardk> here i'm building functions that take singletons to singletons. all it can do is sort of case on the input singleton of which there is only one, and produce a result, also in a singleton of which there is only one
2020-09-22 04:27:34 <edwardk> so such functions are just a recipe of oh, uncons this part and plumb the head here and tail there, and here is the result
2020-09-22 04:27:46 <edwardk> these are done for individual singletons
2020-09-22 04:28:01 → abhixec joins (~abhixec@c-67-169-141-95.hsd1.ca.comcast.net)
2020-09-22 04:28:26 <edwardk> and in Meta I can work with singletons that are types, natural numbers, arbitrary integers, anything with structural equality so i can promote it once and forall
2020-09-22 04:28:48 <edwardk> and i can build a category of such boring (Sing i -> Sing j) functions
2020-09-22 04:29:00 <edwardk> and then look at bundles. i and j there can have different kinds
2020-09-22 04:29:15 <edwardk> so if we quantify away i universally and j existentially but leave the kinds... we're left with hask
2020-09-22 04:29:35 → dolio joins (~dolio@haskell/developer/dolio)
2020-09-22 04:29:40 × Orbstheorem quits (~roosember@hellendaal.orbstheorem.ch) (Ping timeout: 244 seconds)
2020-09-22 04:29:56 <edwardk> basically its all the functions that look at parts of their inputs (remember it has to work forall (i::a) and returns some (j::b) now, which is just what a function is
2020-09-22 04:30:13 <edwardk> in category theory this notion of sort of exploding your objects is something called the grothendieck construction
2020-09-22 04:30:18 × falafel quits (~falafel@2605:e000:1527:d491:f090:20fe:cddf:2a1a) (Remote host closed the connection)
2020-09-22 04:30:36 <edwardk> well there are many grothendieck constructions, but this is the one that folks talk about when talking about categories
2020-09-22 04:31:19 <edwardk> so it was pretty cool to me that i could build this super-laborious category, build functors for it, etc. manipulate the guts of basically anything made out of types, constraints, numbers, inductive data types, etc.
2020-09-22 04:31:23 <edwardk> then reassemble the result
2020-09-22 04:31:33 <edwardk> and get an Arrow that internally does way more weird stuff than you'd expect
2020-09-22 04:31:46 × sepi quits (49dc4892@c-73-220-72-146.hsd1.ca.comcast.net) (Remote host closed the connection)
2020-09-22 04:31:55 <edwardk> and it has all the power of normal functions (it is ArrowApply, etc)
2020-09-22 04:32:14 <edwardk> so i could view this as a sort of 'ultimate form' for something like compiling to categories
2020-09-22 04:32:39 <edwardk> if i want said compilation to categories to handle dictionaries, representations of types, etc. correctly
2020-09-22 04:35:13 <edwardk> not sure how coherent that is
2020-09-22 04:35:17 <edwardk> but that is sort of the thought
2020-09-22 04:35:42 × DataComputist quits (~lumeng@static-50-43-26-251.bvtn.or.frontiernet.net) (Quit: Leaving...)
2020-09-22 04:37:46 → eric_ joins (~eric@2804:431:c7d4:b4fa:173:5d88:9ad1:a8df)
2020-09-22 04:38:55 → DataComputist joins (~lumeng@static-50-43-26-251.bvtn.or.frontiernet.net)
2020-09-22 04:39:05 × abhixec quits (~abhixec@c-67-169-141-95.hsd1.ca.comcast.net) (Ping timeout: 240 seconds)
2020-09-22 04:40:08 → __Joker joins (~Joker@180.151.104.210)
2020-09-22 04:44:50 × __Joker quits (~Joker@180.151.104.210) (Ping timeout: 272 seconds)
2020-09-22 04:45:14 × darjeeling_ quits (~darjeelin@122.245.219.58) (Ping timeout: 260 seconds)
2020-09-22 04:46:00 × DataComputist quits (~lumeng@static-50-43-26-251.bvtn.or.frontiernet.net) (Quit: Leaving...)
2020-09-22 04:47:03 × vicfred quits (~vicfred@unaffiliated/vicfred) (Quit: Leaving)
2020-09-22 04:49:16 × fresheyeball quits (~isaac@c-71-237-105-37.hsd1.co.comcast.net) (Ping timeout: 272 seconds)
2020-09-22 04:49:44 → DataComputist joins (~lumeng@static-50-43-26-251.bvtn.or.frontiernet.net)
2020-09-22 04:53:04 × toorevitimirp quits (~tooreviti@117.182.182.33) (Ping timeout: 272 seconds)
2020-09-22 04:54:01 → toorevitimirp joins (~tooreviti@117.182.182.33)
2020-09-22 04:54:06 × macrover quits (~macrover@ip70-189-231-35.lv.lv.cox.net) (Ping timeout: 260 seconds)
2020-09-22 04:55:15 <edwardk> anyways MarcelineVQ the other major need for constraints to live in Sing is that i may want to take singleton types over ADTs. i can singleton ~ constraints, but i need to be able to singleton up whatever dictionaries they may package up in their constructors
2020-09-22 04:55:24 <edwardk> that covers the existential fragment
2020-09-22 04:55:49 <edwardk> and i need to be able to take limits over things to handle the (forall x. whatever x) kinda fragments as well that pop up in ADTs a lot
2020-09-22 04:55:56 × dxld quits (~dxld@2a01:4f8:201:89ff:7479:df6a:7ab8:8305) (Quit: Bye)
2020-09-22 04:56:01 × merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 264 seconds)
2020-09-22 04:56:02 <edwardk> otherwise my ability to introspect on singletons is quite limited
2020-09-22 04:56:26 <edwardk> the goal is to "fully" allow promotion of all haskell data types, not just the convenient ones like in byorgey's paper
2020-09-22 04:57:13 <edwardk> er data constructors
2020-09-22 04:57:15 <edwardk> not data types
2020-09-22 04:57:18 <edwardk> the types promote fine
2020-09-22 04:57:22 <edwardk> they just lack most of the stuff in them
2020-09-22 04:58:46 × sand_dull quits (~theuser@62.182.99.37) (Ping timeout: 260 seconds)
2020-09-22 05:01:24 <siraben> What do people use here for proving correctness of programs in Haskell? Is liquid haskell still a good choice?
2020-09-22 05:01:34 <siraben> Also, introspection testing, and so on.
2020-09-22 05:01:46 <edwardk> liquid haskell works well if all your constraints are easy things to feed a sat solver involving numbers
2020-09-22 05:01:58 <edwardk> otherwise there are a couple of haskell to coq toolchains and something for isabelle, etc.
2020-09-22 05:02:34 → vicfred joins (~vicfred@unaffiliated/vicfred)
2020-09-22 05:04:52 → falafel joins (~falafel@2605:e000:1527:d491:f090:20fe:cddf:2a1a)
2020-09-22 05:07:55 → justanotheruser joins (~justanoth@unaffiliated/justanotheruser)
2020-09-22 05:13:32 → alp joins (~alp@2a01:e0a:58b:4920:43b:dddd:19e5:4b3)
2020-09-22 05:15:17 → mariatsji joins (~mariatsji@2a01:79d:53aa:c66c:342b:5324:f59b:5b0e)
2020-09-22 05:17:02 → Lord_of_Life_ joins (~Lord@unaffiliated/lord-of-life/x-0885362)
2020-09-22 05:17:27 × alxgnon1 quits (~alxgnon@185.204.1.185) (Remote host closed the connection)
2020-09-22 05:18:32 × steve_ quits (~quassel@ool-18b99d28.dyn.optonline.net) (Remote host closed the connection)
2020-09-22 05:19:18 × Lord_of_Life quits (~Lord@unaffiliated/lord-of-life/x-0885362) (Ping timeout: 260 seconds)
2020-09-22 05:19:18 Lord_of_Life_ is now known as Lord_of_Life
2020-09-22 05:19:43 → steve_ joins (~quassel@ool-18b99d28.dyn.optonline.net)
2020-09-22 05:19:58 → ishutin joins (~Ishutin@178-164-206-35.pool.digikabel.hu)
2020-09-22 05:20:11 × mariatsji quits (~mariatsji@2a01:79d:53aa:c66c:342b:5324:f59b:5b0e) (Ping timeout: 272 seconds)
2020-09-22 05:20:57 <shafox> I use ghcup to install ghc and cabal and use it in my project. However there are other tools that needs to be installed such as ghcid, hoogle, language-server etc which are bound by the ghc version to play well with the project. So I have started to look for a solution which can integrate all the tools that is needed for development env (for now), stumbled across on nix, however I am not sure whether nix can install all the dependency for a particular
2020-09-22 05:20:57 <shafox> ghc and I can use that in the project. Is there any blog posts or gist/github links where a env with developement tools are being used so that I can steal the config ?
2020-09-22 05:22:44 <Axman6> I don't know how it works, but at work we have something which will activate an environment, including nix stuff, when you cd into the project directory so everything Just Works
2020-09-22 05:23:18 × ishutin_ quits (~Ishutin@94-21-82-48.pool.digikabel.hu) (Ping timeout: 260 seconds)
2020-09-22 05:23:19 <shafox> Axman6, please share more about it.
2020-09-22 05:23:42 <Axman6> I can't share much, but I'll see if I can find names of things
2020-09-22 05:23:48 → __Joker joins (~Joker@180.151.104.210)
2020-09-22 05:24:04 <shafox> Alright.
2020-09-22 05:24:41 × iscke quits (~black@60.225.157.201) (Remote host closed the connection)
2020-09-22 05:24:44 × oxide quits (~lambda@unaffiliated/mclaren) (Ping timeout: 272 seconds)
2020-09-22 05:24:59 → thir joins (~thir@p200300f27f0fc600ed2222922a5678d5.dip0.t-ipconnect.de)
2020-09-22 05:25:00 → iscke joins (~black@60.225.157.201)
2020-09-22 05:25:19 <Axman6> looks like it uses something called direnv
2020-09-22 05:25:24 → peach_liqueur joins (~black@60.225.157.201)
2020-09-22 05:26:16 → oxide joins (~lambda@unaffiliated/mclaren)
2020-09-22 05:26:21 × whiteline quits (~whiteline@unaffiliated/whiteline) (Remote host closed the connection)
2020-09-22 05:26:39 → whiteline joins (~whiteline@unaffiliated/whiteline)
2020-09-22 05:27:08 <shafox> Axman6, yes. direnv doesnt actually solve what I have stated.
2020-09-22 05:27:11 × peach_liqueur quits (~black@60.225.157.201) (Remote host closed the connection)
2020-09-22 05:27:29 → peach_liqueur joins (~black@60.225.157.201)
2020-09-22 05:28:13 <Axman6> well, time for you to go and learn nix
2020-09-22 05:28:13 × Foritus quits (~buggery@cpc91334-watf11-2-0-cust153.15-2.cable.virginm.net) (Read error: Connection reset by peer)
2020-09-22 05:28:31 <Axman6> it can solve the problems you have, and there's plenty of examples of people doing it on the net
2020-09-22 05:28:38 → merijn joins (~merijn@83-160-49-249.ip.xs4all.nl)
2020-09-22 05:28:49 × sasssss quits (54ed377d@84.237.55.125) (Ping timeout: 245 seconds)
2020-09-22 05:29:10 × inkbottle quits (~inkbottle@aaubervilliers-654-1-101-24.w86-212.abo.wanadoo.fr) (Quit: Konversation terminated!)
2020-09-22 05:29:27 × thir quits (~thir@p200300f27f0fc600ed2222922a5678d5.dip0.t-ipconnect.de) (Ping timeout: 260 seconds)
2020-09-22 05:29:27 → jedws joins (~jedws@121.209.139.222)
2020-09-22 05:29:28 → Foritus joins (~buggery@cpc91334-watf11-2-0-cust153.15-2.cable.virginm.net)
2020-09-22 05:29:41 × peach_liqueur quits (~black@60.225.157.201) (Remote host closed the connection)
2020-09-22 05:29:44 × iscke quits (~black@60.225.157.201) (Ping timeout: 260 seconds)
←Prev  Next→
Page 1 .. 127 128 129 130 131 132 133 134 135 136 137 .. 5022

All times are in UTC.