00:01:23 -!- drdanmaku has quit (Quit: Connection closed for inactivity). 00:02:42 I think I can implement van Laarhoven lenses in a dynamically typed language without difficultly faking typeclasses, but not sure about other van Laarhoven optics 00:03:15 lasers 00:03:20 Instead of f a, could just give a function that's effectively flip fmap 00:03:28 I think 00:03:49 There's not much else you can do with an unknown Functor 00:03:59 tomb of the unknown functor 00:07:02 -!- Phantom_Hoover has quit (Ping timeout: 252 seconds). 00:10:57 One of my friends is playing a 1080p movie via sshfs to a server in France 00:12:02 I have pretty much moved from streaming with sshfs to transfering with git-annex. 00:13:10 Traversals need traversable, which needs foldable and functor... I don't think I can represent opaque traversables as literally one function 00:15:43 Hold on, there are default definitions for the Functor and Foldable part... but would I ever need to pass in a functor or foldable that's not a traversable 00:18:04 Sgeo: um lens traversals are analogous to traversables, not based on them... 00:18:33 you get them by switching Functor with Applicative in the lens version 00:18:44 Ah 00:18:52 ...Applicative may be a bit problematic 00:19:43 Or... ok, not thinking about this fully at the moment 00:21:13 although perhaps you _can_ do it with traversables, in some "dual" representation 00:22:05 * oerjan wonders what a Lensable would look like 00:22:43 the thing that would be a typeclass corresponding to lenses and Functor in the same way Traversable corresponds to traversals and Applicative 00:23:07 and Functor corresponds to getters and ...um, something? 00:23:27 :t (^.) 00:23:28 s -> Getting a s a -> a 00:23:49 um sorry, *setters 00:24:01 oerjan, Getter needs (Functor f, Contravariant f) 00:24:32 oh 00:25:41 Getter might correspond to Pointed as a class, maybe 00:28:57 Surely Copointed? 00:29:25 oh right because Const r is the "only" thing that is both. 00:29:26 -!- boily has quit (Read error: Connection reset by peer). 00:30:08 -!- boily has joined. 00:30:30 wait what is Copointed 00:32:20 Foldable corresponds to folds and something 00:32:49 Foldable is Functor + Monoid a => f a -> a 00:33:57 that's not the part i'm interested in 00:35:09 hm Contravariant and Applicative 00:35:20 * oerjan thinks his brain is running out of steam again 00:35:42 also i didn't finish the logs 00:37:28 oerjan, Copointed is f a -> a 00:38:02 kmc: it involves categorical logic <-- have you reinvented cartesian closed categories 00:38:22 Taneb: hm right 00:38:36 I think it's Traversable : Traversal :: Copointed : Getter 00:39:03 Every Copointed is trivially Foldable 00:39:07 yeah sounds reasonable 00:40:52 Functor+Contravariant means phantom 00:41:08 shachaf: aka Const 00:41:08 You could make class Phantom f where coerce :: f a -> f b (we used to have that) 00:41:31 Const r or something isomorphic to it, sure. 00:41:54 ok Setter uses a complicated brew of contexts that enforce the functor being Identity. 00:41:57 Anyway, we just use Functor+Contravariant to express that using non-lens classes. 00:42:01 Right. 00:48:52 i think taintedDot is named for what it does to people who come by it unwarily. 00:51:26 -!- nisstyre has quit (Quit: WeeChat 0.4.3). 00:54:37 oh, here was a fun one I thought of today: can we get a minor-closed class of graphs, membership in which is undecideable? <-- no. https://en.wikipedia.org/wiki/Robertson%E2%80%93Seymour_theorem 00:56:22 taintedDot is still a thing? 00:56:23 whoa 00:56:49 i'm sorry :'( 00:57:25 i'm wondering why they're bothering with all that machinery for something that's supposed to be Identity 00:58:10 the trouble is that newtype Id a = Id { runId :: a }, (Id x) is operationally the same as x 00:58:30 and Id is operationally the same as, uh, id 00:58:49 but (Id . f) is operationally the same as (\x -> Id (f x)) = (\x -> id (f x)) = (\x -> f x) 00:58:58 which isn't the same as f (when f is _|_) 01:00:13 ok that explains the seqs i guess but not why they bother to list all the superclasses 01:00:59 and even to _use_ them in the implementation 01:01:31 ahem 01:01:39 have a look at a thing called Conjoined 01:02:28 are you talking about the default implementations? 01:02:54 those can't use unsafeCoerce because maybe the user will give a type that isn't Id and then you can derive a real unsafeCoerce from the default instance 01:06:05 oh wait it's actually just Applicative which is used 01:06:16 -!- edwardk has joined. 01:08:37 If a Functor is a function that takes one argument, an Applicative could be a function that takes several arguments. Except I lose pure 01:09:08 (And currently guessing as to whether that several arguments thing would work, but it makes a kind of intuitive sense) 01:10:25 Harder to have one that you add to later though 01:12:20 augur_: oh wait ski not lambda calculus 01:13:26 Sgeo: maybe you can make that Traversal1 thing i found just earlier 01:13:59 AFK, I'll look when I get back 01:34:37 -!- Slereah_ has joined. 01:38:43 -!- Slereah has quit (Ping timeout: 252 seconds). 01:49:01 -!- adu has joined. 01:53:35 -!- nooodl has quit (Quit: Ik ga weg). 02:00:07 > "aha" 02:00:09 can't find file: L.hs 02:00:16 *cough* 02:00:18 > "aha" 02:00:19 "aha" 02:02:54 -!- oerjan has set topic: The channel with the > bot | PSA: fizzie is running the wiki now, contact him for any problems | https://dl.dropboxusercontent.com/u/2023808/wisdom.pdf http://codu.org/logs/_esoteric/ http://tunes.org/~nef/logs/esoteric/. 02:05:52 -!- boily has quit (Quit: WeeChat 0.4.2). 02:09:17 "So. It’s World Penguin Day & DNA Day… AND World Malaria Day & Ed Balls Day." kmc you know what to do <-- ok kmc how is your penguin/mosquito chimæra going? 02:10:38 -!- rodgort has quit (Quit: ERC Version 5.3 (IRC client for Emacs)). 02:13:16 We got idris-ircslave to stop using > ? 02:13:49 amazing, isn't it 02:15:09 -!- rodgort has joined. 02:15:13 -!- zzo38 has joined. 02:15:34 Has anyone written a roguelike game in SQL before? 02:15:58 -!- rodgort has quit (Remote host closed the connection). 02:19:08 -!- rodgort has joined. 02:19:21 -!- adu has quit (Quit: adu). 02:20:44 -!- rodgort has quit (Remote host closed the connection). 02:23:13 Where's that thing explaining how to make a lens from scratch? 02:23:34 which one? 02:23:46 http://ftp.newartisans.com/pub/Lenses.mp4 is simon's talk 02:23:55 Was hoping for a page 02:24:00 mth.io/talks/lens-from-the-ground-up/ is mark hibberd's talk 02:24:29 https://github.com/ekmett/lens/wiki/Derivation is my original page in the wiki starting from motivation to theory 02:24:48 Thanks 02:25:55 zzo38: that sounds terrible. go for it ;) 02:26:16 -!- rodgort has joined. 02:26:18 Instead of 02:26:31 Functor f => (b -> f b) -> a -> f a 02:26:40 I'm thinking that I could have something like 02:27:40 ... 02:27:54 :t flip fmap 02:27:55 Functor f => f a -> (a -> b) -> f b 02:29:15 oerjan: yeah, I realized in retrospect it was a dumb question 02:29:58 I meant to ask the slightly more interesting question "is it possible that there's a minor-closed graphs for which we are unable (in the sense of independence) to find the forbidden minors? 02:30:02 " 02:30:29 i'd expect that to be true 02:31:13 The only way to construct that f a that the lens must output is to use fmap with the result of (b -> f b), right? 02:31:14 edwardk: Are you sure it is terrible? 02:31:34 sgeo: the problem with that form is it doesn't compose as well 02:31:47 oerjan: but we can enumerate all of the possible sets of forbidden minors 02:32:33 coppro: yes, but we cannot check whether any particular of those sets gives the original set of graphs, i think 02:32:33 Are there likely to be significant limitations if I keep not going the van Laarhoven route in a dynamically typed language? 02:32:46 My code is so verbose :/ 02:33:02 Also, it would be fun to show it could be done 02:33:21 > map (zip [1, 2, 3]) $ [4, 5, 6] 02:33:23 No instance for (GHC.Show.Show b0) 02:33:23 arising from a use of ‘M245150698743640559410341.show_M2451506987436405594... 02:33:23 The type variable ‘b0’ is ambiguous 02:33:23 Note: there are several potential instances: 02:33:23 instance [safe] GHC.Show.Show 02:33:31 why 02:33:56 > map (zip [1,2,3]) $ [[4,5,6]] 02:33:57 [[(1,4),(2,5),(3,6)]] 02:34:06 Bike: zip [1, 2, 3] 4 doesn't make much sense 02:34:07 > map (zip [1, 2, 3 :: Int]) $ [4,5,6] 02:34:08 No instance for (GHC.Show.Show b0) 02:34:08 arising from a use of ‘M814034439476907821810375.show_M8140344394769078218... 02:34:08 The type variable ‘b0’ is ambiguous 02:34:08 Note: there are several potential instances: 02:34:08 instance [safe] GHC.Show.Show 02:34:18 coppro: although this is really about _descriptions_ of sets of graphs, not sets of graphs themselves 02:34:22 > map (zip [1,2,3]) [4::Int,5,6] 02:34:24 Couldn't match expected type ‘[b]’ with actual type ‘GHC.Types.Int’ 02:34:44 oerjan: true 02:35:01 ... were you able to determine beforehand without GHCi or similar that that would be a clearer error message somehow? 02:35:10 coppro: oh wait am i thinking about this wrongly 02:35:45 :t zip 02:35:46 [a] -> [b] -> [(a, b)] 02:35:47 oerjan: I don't think so. We can describe any minor-closed set of graphs by its forbidden minors 02:35:51 oh right. 02:35:52 hm no 02:36:03 (that wasn't a response) 02:36:21 So the question is "is there some way to describe a minor-closed set of graphs in such a way that we are unable to associate them with a description of that set by its forbidden minors." 02:40:12 seems like you just need to encode a gödel sentence or something 02:40:46 oh well 02:43:20 oerjan: yeah, you need to encode something like that. but I'm not quite sure how you would do so in a useful way that still leaves you minor-closed 02:43:33 oh wait, I guess you could, nevermind 02:43:56 hmm... better. membership in the class needs to be decideable 02:44:33 that would seem more interesting 02:46:03 -!- FreeFull_ has joined. 02:48:00 -!- FreeFull has quit (Ping timeout: 265 seconds). 03:08:16 * Sgeo is still trying to figure out the functor thing 03:08:34 All I can think is maybe it's an infinitely big type trying to write it out like that 03:09:13 http://twanvl.nl/blog/haskell/overloading-functional-references ? 03:09:35 you were asking about lenses, these are twan's original posts 03:10:46 Is it possible to write a function that gives infinitely many arguments in Haskell? 03:10:48 *takes 03:10:52 id 03:11:55 Hmm, even if the type involved is opaque to my lenses, it can't be opaque to the driver 03:13:39 But it doesn't need to be just a function, it itself shouldn't be getting composed, right? 03:13:50 wouldn't const id or however you spell it take infinitely many arguments 03:13:52 Only the lenses that treat it as opaque get composed 03:14:10 > const id 3 4 03:14:11 4 03:14:17 > const id 3 4 5 03:14:18 Could not deduce (GHC.Num.Num (a0 -> t)) 03:14:18 arising from the ambiguity check for ‘e_1345’ 03:14:18 from the context (GHC.Num.Num (a -> t), GHC.Num.Num a) 03:14:18 bound by the inferred type for ‘e_1345’: 03:14:18 (GHC.Num.Num (a -> t), GHC.Num.Num a) => t 03:14:23 ...dangit numbers 03:14:26 uh? 03:14:29 > const id '3' '4' '5' 03:14:31 Couldn't match expected type ‘GHC.Types.Char -> t’ 03:14:31 with actual type ‘GHC.Types.Char’ 03:14:33 :t const id 03:14:34 b -> a -> a 03:14:47 no, wait, i'm thinking wrong, yeah. 03:15:14 i just want a function that ignores its argument and returns itself. 03:15:29 Hey, I've finally learned the difference between expected and actual 03:15:31 :t let f x = f 03:15:32 : not an expression: ‘let f x = f’ 03:15:38 :t let f x = f in f 03:15:39 Occurs check: cannot construct the infinite type: t3 ~ t2 -> t3 03:15:39 Relevant bindings include 03:15:39 x :: t2 (bound at :1:7) 03:15:46 boring! 03:16:13 > fix id 03:16:17 Conceptually, an infinite type can be well-typed even if Haskell doesn't understand it, right? 03:16:17 mueval-core: Time limit exceeded 03:16:28 > undefined 3 4 5 6 7 03:16:30 *Exception: Prelude.undefined 03:16:33 fix kills an argument 03:16:35 owned!!! 03:21:12 -!- huh has joined. 03:21:27 @let import Data.NumInstances 03:21:28 Defined. 03:21:33 > 1 2 3 4 5 03:21:34 1 03:23:43 note that if a value has the type a = b -> a then you can never get any information out of it 03:24:44 @src Mu 03:24:44 newtype Mu f = In { out :: f (Mu f) } 03:25:17 that should be called Fix :'( 03:25:50 :t let f x = out f in f 03:25:51 Couldn't match expected type ‘Mu f1’ 03:25:51 with actual type ‘t1 -> f1 (Mu f1)’ 03:25:51 Relevant bindings include 03:25:56 :t let f x = In f in f 03:25:57 t -> Mu ((->) t) 03:26:15 To write a roguelike game in SQL does not sound too terrible to me; you will not have to deal with encoding data in a save file, since SQL will do that automatically (you don't even need to tell it to save; that is automatic too), 03:26:32 @let newtype Fix f = Fix { runFix :: f (Fix f) } 03:26:33 Defined. 03:28:05 :t coerce 03:28:06 (Contravariant f, Functor f) => f a -> f b 03:28:23 NOT THE ONE I WAS LOOKING FOR 03:28:53 coerjan 03:29:40 cœrce 03:30:46 "t GHC.Prim.coerce 03:30:49 :t GHC.Prim.coerce 03:30:49 GHC.Types.Coercible a b => a -> b 03:30:57 aha 03:31:08 (exported via GHC.Exts) 03:32:59 @let f x = GHC.Prim.coerce (In f) 03:32:59 .L.hs:147:7: Not in scope: ‘GHC.Prim.coerce’ 03:33:00 03:33:00 .L.hs:147:27: 03:33:00 Ambiguous occurrence ‘f’ 03:33:00 It could refer to either ‘L.f’, defined at .L.hs:147:1 03:33:08 darn 03:33:23 @let a = GHC.Exts.coerce 42 03:33:24 .L.hs:144:5: Not in scope: ‘GHC.Exts.coerce’ 03:33:42 GHC.Exts is not very safe :P 03:33:54 coerce is meant to be safe :( 03:35:25 which i guess means that's the wrong module to export that from... 03:35:25 oerjan: I can if the language allows functions to be more than merely functions 03:35:44 Sgeo: oh right you're not working in haskell 03:36:23 Sgeo: you can't make a truly infinite function type in Haskell. You can, of course, fake it. 03:36:39 @run let a = (); a # b = 0 in let a# b = 1 in a# () 03:36:40 1 03:36:58 hmm. no. 03:37:04 @run let a = (); a# b = 0 in let a # b = 1 in a# () 03:37:06 0 03:37:29 That's a proper test for MagicHash. 03:37:58 @run 0# 03:38:00 Kind incompatibility when matching types: 03:38:00 a0 :: * 03:38:00 GHC.Prim.Int# :: # 03:38:16 @run I# 0# 03:38:17 Not in scope: data constructor ‘I#’ 03:38:17 Perhaps you meant ‘In’ (imported from Lambdabot.Plugin.Haskell.Eval.Trusted) 03:39:27 And I guess that's harmless since you can't operate on such unboxed values anyway. 03:39:45 (with the modules that lambdabot imports) 03:39:47 So prety 03:39:51 (let f () f) 03:42:00 @let class CountArgs a where {countArgs :: Int -> a}; instance CountArgs Int where {countArgs = id}; instance CountArgs a => CountArgs (b -> a) where {countArgs n _ = countArgs $! n + 1} 03:42:01 Defined. 03:42:31 > countArgs 0 "hi" False [Nothing] :: Int 03:42:32 3 03:43:07 imagine working on the first try 03:56:04 -!- tromp has quit (Remote host closed the connection). 03:56:36 Half wondering if it would just make more sense to abuse impurity to turn a modifier into something able to get 03:56:37 -!- tromp has joined. 03:56:51 That... seems almost related to what the functor allows for anyway 03:59:46 `coins 03:59:47 solvescoin pingcoin mazancoin reatcoin barcoin godsmacoin cntalcoin mutlastacoin odtizediuspietcoin giumcoin lo'scoin pcordfuckercoin vowcoin dilaxatcoin goto+coin grancoin eucacoin qalcoin con-textendecoin graphicoin 03:59:49 In some book I have, it describes a virtual machine called "Ada/CS Object Machine". It is a similar to IBM mainframe instruction sets. 03:59:53 (f a) where f is an unknown Functor is iso to (forall b. (a -> b) -> f b), if that's what you've been asking. 04:00:09 yes 04:00:11 thanks 04:00:52 Which is iso to an infinitely large type, I guess 04:01:00 elliott: Isn't that the right Yoneda lemma though? 04:01:01 ? 04:01:02 -!- tromp has quit (Ping timeout: 255 seconds). 04:01:02 -!- Sorella has quit (Quit: It is tiem!). 04:01:15 it's iso to the intersection of ((a -> B) -> f B) for all concrete B, sure. 04:01:29 but that doesn't seem like a terribly useful thing here. 04:02:15 There is also a left Yoneda lemma (is that useful here at all?) 04:13:06 http://ww2.chemistry.gatech.edu/~bostwick/stms/raw.txt Anyone recognize where the language on the bottom could be from, phylogenically? It's probably a DSL 04:18:03 looks like a kind of BASIC to me 04:19:22 Yes, something like BASIC 04:20:20 But unusual; it is using ! for comments 04:20:37 yeah i noticed that 04:21:00 but "PRINT USING" is very basic 04:21:38 Yes, I know, I can write programs in BASIC. 04:22:16 I can write a program in BASIC. Specifically, the empty program. 04:23:12 Yes, that will work and is valid 04:23:50 basic has that #-y print string thing? 04:24:24 If you put #1 or whatever after PRINT it mean, to send it to the file, instead of to the screen. 04:24:43 In a PRINT USING, the # is a placeholder for a digit. 04:25:02 Type suffix in some version of BASIC can be # for double precision floating points. 04:25:04 ah, i see. 04:25:29 "You can use any text editor to write a macro. In the following examples, it is assumed that Microsoft(R) Windows Notepad is used." 04:28:10 -!- Sprocklem has joined. 04:32:23 I think Haskell is about to teach me MVC 04:34:21 -!- Patashu_ has changed nick to Patashu. 04:47:44 What is the specification of the qsort function in C about the exact pointing of the arguments to the comparison function? 04:48:07 what 04:48:44 Does it point to existing objects, create a copy, point to their original location, etc, such as, what will their pointer difference be? 04:51:27 zzo38: it doesn't say. you can't rely on the pointer values at all, just on the contents. 04:52:51 int-e: Though there's no sane way that qsort can do *any* dynamic allocation at all. 04:53:02 (qsort cannot fail) 04:55:06 I suppose that doesn't mean that, say, the arguments to the comparator can't point into buffers on the stack. 04:55:18 Just that there's only so crazy you can go. 04:55:27 pikhq: what of trying to allocate, the allocation failing, and it falling back to something worse than if it was able to allocate? 04:55:41 Huh. Actually, 7.20.5 (C99) says that the pointers being passed are supposed to lie inside the array being sorted. 04:55:58 int-e: Ah, huh. 04:56:07 Not everything that uses malloc has to have a non-0 chance of failing, I think 04:56:10 Sgeo: I guess that's *valid*, if utterly moronic. 04:56:30 int-e: pikhq ??? 04:57:17 Awesom, I can tab-complete huh now. Although I ended up trying to tab-complete ttab-coomplet.e 04:57:36 Particularly with qsort. In-place sorting isn't exactly hard. 05:00:58 -!- huh has quit (Quit: Segmentation fault). 05:02:31 pikhq: hmm. but quicksort is the only viable option that remains. 05:03:51 No. Smoothsort, heapsort, in-place merge sort. 05:04:27 Are you sure qsort cannot fail, even if the comparison function is not implemented correctly? (For example, if it returns a random number regardless of its inputs) 05:04:41 zzo38: That's UB. :) 05:05:05 heapsort is terrible for caches. 05:05:58 And quicksort has pathological behavior on certain inputs. 05:06:27 glibc defaults to a merge sort with n/2 elements worth of temporary space, and falls back to quicksort if allocation fails 05:06:42 That's... not what glibc does. 05:06:59 pikhq: it needs O(log n) stack space according to Wikipedia 05:07:14 Sgeo: Yes. Or about two ints. 05:07:34 Sgeo: Remember, log_2 2^64 is is 64. 05:07:52 Actually... huh. How does that work, exactly, If it's not known until runtime how much stack space.... oh, hmm.... 05:08:04 ... The maximum is well-known. 05:08:30 Maximum on modern computers 05:08:31 pikhq: what do you mean, "that's not what glibc does"? 05:08:53 int-e: I mean that that's not the algorithm used in stdlib/qsort.c. 05:09:15 pikhq: indeed. and that's not qsort. look at msort.c in the same directory. 05:09:38 * pikhq takes a moment to flip off glibc 05:09:58 glibc, the new openssl? 05:10:25 That is... utterly, positively moronic, BTW. 05:10:52 So, on out-of-memory it goes pathological. 05:11:17 Rather than, y'know, just using smoothsort. 05:11:26 There's no Identity Applicative, is there? 05:11:33 What would pure... oh. I'm dumb. 05:11:44 Sgeo: Pretty much. glibc is positively insane. 05:11:54 I managed to forget that pure takes an argument. 05:12:01 wouldn't it be the old ssl 05:12:16 i don't know if return to libc counts as a heartbleed 05:18:02 libc broke his heart 05:18:03 employees must wash hands before returning to libc 05:33:02 oerjan: turns out the answer is you can't 05:33:36 can't which way? 05:34:13 actually, wait, hmm... not sure the reasoning holds 05:34:52 but if you had only finitely many candidate sets of forbidden minors, you could just enumerate the class of graphs and check each of the sets 05:36:04 well sure 05:36:23 in fact you only needed to test the members of the candidate sets 05:37:13 the problem is when you cannot prove there is a much larger forbidden graph than the ones you have tested 05:37:18 yeah 05:38:00 *there isn't 05:38:40 ah here we are 05:38:43 Sgeo,Bike : "Is it possible to write a function that gives infinitely many arguments in Haskell?","i just want a function that ignores its argument and returns itself.","Conceptually, an infinite type can be well-typed even if Haskell doesn't understand it, right?" -- can be done with `ocaml -rectypes', e.g.. this is "equi-recursive" types, as opposed to "iso-recursive" ones 05:39:21 (lambda (f) (lambda (o) ((f (car o)) (lambda (mc) (cons mc (cdr o)))))) 05:39:28 ^^not tested 05:39:33 suppose S were a minimal set of sets of forbidden minors that you couldn't prove were/weren't the set for your class. Then at least one set contains a minor of a graph in another class. You can test those two graphs and eliminate one set from consideration, which contradicts the selection of S. 05:39:44 i used ocaml rectypes for my unlambda implementation 05:39:44 so it relies again on the GMt 05:39:47 well you can obviously do it in scheme 05:40:46 * Sgeo wonders if that's a bit verbose 05:40:55 you can also do it in unlambda. although i never tested out my theoretical "stop at the first argument that is d" idea 05:41:01 Compared to just using a modifier on the targetted car 05:41:05 [wiki] [[User:Quincunx]] http://esolangs.org/w/index.php?diff=39405&oldid=39086 * Quincunx * (+144) /* Circuit Diagram 10 */ 05:43:02 coppro: um your line is too ambiguous for me to interpret 05:43:28 So... twisty, almost. You apply the f too get a functor, which is then wrapped in a modifer that produces a functor, which is then applied to get a functor, etc. etc. 05:43:35 s/too/to/ 05:43:56 in fact i have no idea if "set of sets" is a typo 05:44:15 Somehow this is making the idea behind van Laarhoven lenses a bit more intuitive to me 05:44:19 Is that weird? 05:44:42 For getting, (f (car o)) is a function that just ignores its argument 05:44:52 oerjan: ok, let's say I have a minor-closed class \mathcal G. Let S be the set of sets F such that the statement "F is the set of forbidden minors of \mathcal G" is independent of ZFC. Then by the GMT, there exist, G, H in members of F, one which is a forbidden minor of the other 05:45:03 -!- Vorpal has joined. 05:45:03 -!- Vorpal has quit (Changing host). 05:45:03 -!- Vorpal has joined. 05:45:04 -forbidden 05:46:05 then you can just test G and H for membership in \mathcal G. If either is in \mathcal G, then that isn't a forbidden minor, eliminating one set from consideration. If neither is, then assuming G is a minor of H, then H is not a forbidden minor. either way, our choice of S was wrong, because we proved that some F was not the set of forbidden minors. 05:46:42 should "in members of F" be "in members of S" 05:46:53 no. 05:46:57 oh wait, yes 05:47:21 ski: in Haskell you can play the usual newtype trick. newtype W a = W { apply :: a -> W a }; w = W (\x -> w) 05:47:29 Should I be sad that this is almost certainly not going to be R5RS Scheme? 05:47:45 the tl;dr is that the Graph Minors Theorem is trolling us even more 05:47:57 because it tells us that not only is the set of minors finite, there exists a proof of this fact. 05:48:12 err 05:48:16 there exists a proof of *which* set it is 05:48:39 i am not convinced 05:48:43 Sgeo: what the hell are you trying to do even 05:48:44 but i am also tired 05:49:02 Port something close to van Laarhoven lenses and miscelleny to Racket 05:49:13 well nevermind me then 05:49:38 -!- oerjan has quit (Quit: Too tired, in fact). 05:50:09 int-e : indeed .. but that's kinda obvious 05:50:10 It almost makes sense what f being an applicative maker instead of just a functor maker would do 05:50:20 (and not quite what the OP asked for) 05:50:42 perhaps you can do some classy trick as well 05:50:56 And what pure looks like 05:51:04 Ok, besides Functor and Applicative, what else do I want? 05:51:09 What are prisms actually? 05:51:40 When you save the macro it becomes a file on the computer hard disk. 05:52:08 Bike: so few people have HDs though, aren't they more likely to be saving to floppy? 05:52:16 good point 05:52:37 (I had a book on DOS when I was a kid) 05:52:47 And a laptop that ran DOS 05:53:10 I think the battery died 05:53:59 pikhq: So smoothsort looks complicated (not just the theory, but also the implementation) and bad in the benchmark that I found. I'll look at it some more, but only as an intellectual exercise. 06:01:26 I believe this is what both looks like 06:02:28 (lambda (f) (lambda (o) ((f (car o) (cdr o)) cons))) 06:02:42 Bike : save macro where ? 06:02:53 onto the computer hard disk 06:03:06 i mean, in which system ? 06:06:02 oh some chromotagraphy system 06:10:03 what kind of macro ? 06:10:11 an ui macro ? 06:11:16 more like a shell script. 06:12:07 kmc: https://www.sciencenews.org/article/name-fungus article about fungus sex. you probably know most of it but it's still neat 06:12:08 in an OS ? 06:12:19 for this chromatography machine. 06:16:14 in an OS made for that chromatography machine ? 06:17:44 http://www.chem.agilent.com/Library/usermanuals/Public/MACROS.PDF go crazy 06:29:38 -!- shikhin has joined. 06:29:38 -!- shikhin has quit (Changing host). 06:29:38 -!- shikhin has joined. 06:36:19 fungus 06:36:24 fungots fall on fungot falls 06:36:24 kmc: that is just a value of type is created containing the syntax for mark if he was really gonna get worse and worse each week, i fnord kara to hold me until i fell over to 5 videos and then i jizzed. in other places... problem, about the copyrights: i have put this in the near future, that are just the ordinary ( for call/ cc))) hangs 06:36:46 fungot: tmi 06:36:46