00:28:19 -!- kmc has set topic: shiny racoons | https://dl.dropboxusercontent.com/u/2023808/wisdom.pdf http://codu.org/logs/_esoteric/ http://tunes.org/~nef/logs/esoteric/. 00:29:36 -!- tromp has joined. 00:32:59 kmc: "radiant raccoon" would sound like an Ubuntu release. 00:33:34 rocky raccoon? 00:33:49 rocks aren't shiny in general 00:33:56 https://www.youtube.com/watch?v=wNRH7_Kd5Yc 00:35:10 ("radiant" is also not synonymous to "shiny", of course, but closer than "rocky", imho) 00:37:27 -!- Bike has joined. 00:55:13 * boily is killing unique pandemonium lords ♪ ^^ 01:08:41 -!- Slereah_ has joined. 01:10:18 -!- Slereah__ has quit (Ping timeout: 240 seconds). 01:29:26 int-e: indeed 01:31:07 what will they do when they reach the end of the alphabet with animals 01:31:10 imo start over with mushrooms 01:31:29 Ascendent Amanita, Beautiful Bolete, Charming Chanterelle 01:32:15 -!- nooodl has quit (Quit: Ik ga weg). 01:32:32 dazzling deathcap (http://crawl.chaosforge.org/Deathcap) 01:36:13 * oerjan swats boily for just beating him to the deathcap -----### 01:36:20 -!- tromp has quit (Remote host closed the connection). 01:36:26 oh wait 01:36:53 -!- tromp has joined. 01:37:25 i see "just" is a bit exaggerated here. 01:39:23 there is an actual mushroom called the death cap 01:39:27 amanita phalloides 01:40:37 often poisons asian immigrants to the western us who are used to picking the very similar lookng volvariella volvacea 01:41:00 I knew that. 01:41:06 cool 01:41:11 * kmc -> afk 01:41:19 -!- tromp has quit (Ping timeout: 264 seconds). 01:41:45 `echo hi 01:41:46 No output. 01:43:45 `` echo hi 01:43:45 No output. 01:43:49 `` ls 01:43:49 No output. 01:43:57 `echo No output. 01:43:58 No output. 01:44:08 `? TEST 01:44:09 No output. 01:44:12 okay. 01:44:41 HackEgo is censoring overzealously. 01:45:01 maybe e's just meditating. 01:45:22 `` wake up 01:45:22 No output. 01:45:27 `wake up 01:45:27 No output. 01:46:08 it does not even complain about commands not being found. perhaps the find-a-command script is broken? 01:47:43 `help 01:47:43 Runs arbitrary code in GNU/Linux. Type "`", or "`run " for full shell commands. "`fetch " downloads files. Files saved to $PWD are persistent, and $PWD/bin is in $PATH. $PWD is a mercurial repository, "`revert " can be used to revert to a revision. See http://codu.org/projects/hackbot/fshg/ 01:48:04 sounds likely. 01:48:15 `run echo hi 01:48:16 No output. 01:49:21 `fetch http://esolangs.org/wiki/Wierd 01:49:23 2014-03-16 01:49:22 URL:http://esolangs.org/wiki/Wierd [18043] -> "Wierd" [1] 01:49:39 oh, the builtins don't use the sandbox machinery, right? 01:49:45 showed up in the repository browser too 01:49:50 indeed. 01:49:53 Gregor: ^ 01:50:07 and then he's idle again. 01:50:21 `revert 01:50:26 Done. 01:50:49 `revert 1 01:50:50 hm the revert did _not_ show. 01:51:14 Done. 01:51:31 ...that did. 01:51:36 `run echo hi 01:51:37 No output. 01:51:43 works perfectly now 01:51:59 O KAY 01:52:03 `revert 01:52:16 Done. 01:52:18 elliott: what did that do? the commit looks awfully big ... 01:52:26 int-e: went back some trillion years 01:52:37 back to when hackego roamed with the dinosaurs 01:53:29 http://codu.org/projects/hackbot/fshg/index.cgi/file/03afb1619ef2/wisdom ... wow. 01:53:37 so few entries. 01:54:07 `revert 4528 01:54:08 Done. 01:54:35 ok, every second revert gets through? 01:54:38 int-e: what was that for? 01:55:04 I'd hope that 4528 is http://codu.org/projects/hackbot/fshg/index.cgi/rev/c8d06895aeef 01:55:37 well it's the number of the revision before i fetched Wierd 01:56:09 In any case, I missed your `revert. 01:56:28 I stare at IRC, I stare at the web browser, I lose context. 01:56:42 fiendish 01:57:14 anyway, all the non-sandbox commands seem to work _sometimes_. 01:58:08 -!- yorick has quit (Remote host closed the connection). 02:04:23 -!- Bike has quit (Ping timeout: 245 seconds). 02:08:02 -!- Slereah_ has quit (Read error: Connection reset by peer). 02:08:22 -!- Slereah_ has joined. 02:17:02 -!- Bike has joined. 02:18:00 MWAH AH AH AH AH AH AH! 02:19:10 i knew it, the saneness was just a ruse 02:19:49 sorry. I just killed the fourth unique Pandemonium Lord. 02:20:00 (eviscerating demons is a fun activity!) 02:20:14 fourth? that doesn't sound very unique. 02:20:22 ( let muahaha = the (Stream String) "haha" : muahaha 02:20:22 (input):1:42: error: expected: "$", 02:20:22 "$>", "&&", "&&&", "*", "***", 02:20:22 "+", "++", "-", "->", ".", "/", 02:20:22 "/=", ":+", "::", "<", "<$", 02:20:22 "<$>", "<*>", "<+>", "<->",↵… 02:20:28 ( let muahaha = the (Stream String) "haha" : muahaha in muahaha 02:20:28 (input):1:42: error: expected: "$", 02:20:28 "$>", "&&", "&&&", "*", "***", 02:20:28 "+", "++", "-", "->", ".", "/", 02:20:30 "/=", ":+", "::", "<", "<$", 02:20:31 ? 02:20:32 "<$>", "<*>", "<+>", "<->",↵… 02:20:40 ( let muahaha = the (Stream String) ("haha" : muahaha in muahaha) 02:20:40 (input):1:19: error: expected: "$", 02:20:41 "$>", "&&", "&&&", "*", "***", 02:20:41 "+", "++", "-", "->", ".", "/", 02:20:41 "/=", ":+", "::", "<", "<$", 02:20:42 "<$>", "<*>", "<+>", "<->",↵… 02:20:46 Sgeo_: STOP 02:21:10 oerjan: in DCSS, there are an infinity of pandemonium levels, each with a randomized pandemonium lord. 02:21:35 oerjan: of these infinite levels, four have a predefined fixed vault, with a fixed unique and a fixed rune. 02:21:43 therefour, they are four, but unique. 02:21:54 Sgeo_: CONTINUE 02:21:57 Sgeo_: it doesn't work for two different reasons, one of which i tried out earlier and it doesn't work inside let. 02:22:08 or in expressions. 02:22:26 (basically let is _not_ recursive in idris.) 02:22:34 Ah 02:22:55 is idris not lazy...? 02:24:26 It's strict by default, but has laziness annotations. I don't know how those interact with codata. 02:25:15 i tried applying laziness too, it didn't help with the lack of recursion. 02:25:25 admittedly i haven't read any actual tutorial. 02:25:47 weird. 02:26:31 Melvar said something about recursion being allowed in where clauses, but i couldn't find out how to put one in. 02:27:59 maybe you can only put them on top level declarations, or something. 02:28:17 ( :doc where 02:28:17 (input):1:1: error: expected: end of input, 02:28:17 operator 02:28:17 :doc where 02:28:17 ^ 02:33:10 -!- zzo38 has joined. 02:36:15 sup zzo 02:39:11 sdown? 02:40:08 no 02:40:53 hezzo38. 02:52:28 -!- boily has quit (Quit: UNDEMONIAC CHICKEN). 02:53:29 -!- tertu has joined. 03:01:23 -!- oerjan has quit (Quit: Najt). 03:14:16 -!- tromp has joined. 03:50:19 -!- shikhin has quit (Ping timeout: 264 seconds). 04:29:29 -!- tromp has quit (Remote host closed the connection). 04:30:10 -!- tromp has joined. 04:34:24 -!- tromp has quit (Ping timeout: 240 seconds). 04:48:43 -!- manueliitho has joined. 04:53:50 http://imgur.com/a/sAIe6 05:06:54 I'm lost 05:16:32 -!- shikhin has joined. 05:18:09 -!- Sorella has quit (Quit: It is tiem!). 05:21:59 try going left 05:34:48 `welcome manueliitho 05:34:48 No output. 05:35:08 `swat Gregor 05:35:09 No output. 05:35:17 I expected as much 05:36:13 manueliitho: welcome to the esoteric channel of, uh, shiny racoons 05:36:53 -!- Bike has quit (Ping timeout: 245 seconds). 05:41:08 -!- manueliitho has left. 05:46:53 http://i.imgur.com/ALjs0rf.jpg 06:00:26 -!- abirvalg has joined. 06:05:04 -!- password2 has joined. 06:09:37 -!- abirvalg has quit (Quit: http://quassel-irc.org - ????????????? ??????. ?????.). 06:15:12 -!- nisstyre has quit (Quit: WeeChat 0.4.3). 06:24:02 -!- ^v has quit (Ping timeout: 252 seconds). 06:24:21 -!- password2 has quit (Quit: Leaving). 06:25:47 I believe that allowing triggers to be indexed would be a good idea to add into SQL, in case you have one hundred triggers on one view, that you can speed up finding the correct trigger to execute. 06:27:04 -!- password2 has joined. 06:47:50 -!- Sellyme has quit (Excess Flood). 06:49:26 -!- Sellyme has joined. 06:50:05 -!- tertu has quit (Ping timeout: 252 seconds). 06:57:02 -!- conehead has joined. 07:19:51 -!- chaiomanot has quit (Remote host closed the connection). 07:40:25 -!- Sellyme has quit (Excess Flood). 07:44:26 -!- Sellyme has joined. 08:06:42 -!- AnotherTest has joined. 08:48:32 -!- Sellyme has quit (Excess Flood). 08:50:55 -!- Sellyme has joined. 09:02:29 -!- conehead has quit (Quit: Computer has gone to sleep.). 09:12:53 -!- Sellyme has quit (Excess Flood). 09:14:25 -!- Sellyme has joined. 09:28:23 -!- Sellyme has quit (Excess Flood). 09:29:25 -!- Sellyme has joined. 10:01:50 -!- shikhout has joined. 10:02:41 -!- Koen_ has joined. 10:04:43 -!- shikhin has quit (Ping timeout: 264 seconds). 10:04:44 -!- shikhout has changed nick to shikhin. 10:55:59 -!- nooodl has joined. 11:18:46 -!- password2 has quit (Remote host closed the connection). 11:22:49 Sgeo_: Would you please not try to produce an infinite recursion? It locks up the REPL, taking down the bot. 11:25:16 -!- nordee14 has joined. 11:25:54 ( take 20 (Stream.repeat "haha") 11:25:54 ["haha", "haha", "haha", "haha", "haha", "haha", "haha", "haha", "haha", "haha", "haha", "haha", "haha", "haha", "haha", "haha", "haha", "haha", "haha", "haha"] : Vect 20 String 11:29:31 -!- nordee14 has left. 11:39:02 Melvar: Some sort of timeout should probably be added 11:39:13 ( take 11:39:13 Can't disambiguate name: Prelude.List.take, Prelude.Stream.take, Prelude.Vect.take 11:39:19 ( Stream.take 11:39:19 (input):0:0:Incomplete term take 11:39:23 ( :t Stream.take 11:39:23 Prelude.Stream.take : (n : Nat) -> (Stream a) -> Vect n a 11:55:33 FreeFull: The bot has a timeout. The REPL it communicates with does not. 12:01:21 Melvar: How do you produce an infinite loop anyway? I want to test something, locally 12:05:23 -!- boily has joined. 12:14:14 hoily 12:20:54 Jafet: someone was apparently not looking for shiny racoons 12:23:23 heloooodl. 12:23:32 olsnhellor. 12:23:41 still shiny racooning? 12:29:37 -!- Sellyme has quit (Excess Flood). 12:29:56 -!- Sellyme has joined. 12:32:12 -!- Koen_ has quit (Read error: Connection reset by peer). 12:32:27 -!- Koen_ has joined. 12:32:39 -!- yorick has joined. 12:42:39 -!- Koen_ has quit (Quit: Koen_). 13:08:01 -!- Slereahphone has quit (Quit: Colloquy for iPhone - http://colloquy.mobi). 13:10:01 -!- Slereahphone has joined. 13:32:14 -!- oerjan has joined. 13:37:21 ( :t scanl 13:37:21 No such variable scanl 13:37:28 wat. 13:37:41 I WANT MY FIBONACCI DAMMIT 13:37:47 ( :t scan 13:37:48 No such variable scan 13:39:23 ( :t foldr 13:39:23 Prelude.Foldable.foldr : Foldable t => (elt -> acc -> acc) -> acc -> (t elt) -> acc 13:40:10 Would any folks here happen to have free access to http://www.sciencedirect.com/science/article/pii/0734189X88901144 13:41:53 I don't seem to have any access anymore :( 13:42:32 clearly false advertising, how can it be direct if people don't have access 13:44:29 There may be more false advertising involved: I'm actually looking for a different article which is supposed to be on pages 14–27 of that issue while the linked article should only cover pages 1–13 13:44:57 But sciencedirect doesn't even mention the other one so I'm wondering if they're both in the PDF of that one or what's up 13:48:32 I see 1-27. 13:48:46 Yes, that's what sciencedirect claims 13:48:57 Or did you see the PDF itself? 13:50:04 It has the same number of pages as http://46.4.207.77/a.pdf 13:51:08 Right, so some merging took place on Elsevier's end, thanks 13:51:51 bah last darths & droids was clearly false alarm. i guess they didn't have the picture frames for it. 13:55:34 -!- Sorella has joined. 13:56:09 ( :t with Stream foldr (::) [] 13:56:09 Can't unify 13:56:09 a -> (Lazy (Stream a)) -> Stream a 13:56:09 with 13:56:09 elt -> acc -> acc 13:56:09 Specifically:↵… 13:56:36 ( :t with Stream foldr (\x y -> x :: Delay y) [] 13:56:36 Can't disambiguate name: Data.HVect.Nil, Prelude.List.Nil, Data.Vect.Quantifiers.Nil, Prelude.Vect.Nil 13:56:56 oh right there's no stream Nil. 13:57:50 ( :t with Stream foldr (\x y -> x :: Delay y) 13:57:50 No such variable \ 13:57:56 ( :t with Stream foldr (\x y => x :: Delay y) 13:57:56 (input):1:1: error: expected: end of input, 13:57:56 operator 13:57:56 :t with Stream foldr (\x y => x :: Delay y) 13:57:56 ^ 13:57:57 parse error on input `=>' 13:58:18 wtf 13:58:20 ( :t x^2 13:58:20 (input):1:1: error: expected: end of input, 13:58:20 operator 13:58:20 :t x^2 13:58:20 ^ 13:58:21 parse error (possibly incorrect indentation or mismatched brackets) 13:58:36 :t x^2 -- 13:58:37 Expr 13:58:41 ( :t x^2 -- 13:58:44 (input):1:1: error: expected: end of input, 13:58:44 operator 13:58:44 :t x^2 -- 13:58:44 ^ 13:58:44 Expr 13:58:58 Potential botloop there... 13:59:14 fancy 13:59:18 `? botlops 13:59:19 No output. 13:59:44 There is no type beginning with a ( , is there. 13:59:57 You can with type operators 14:00:01 sure there is. 14:00:10 :t fix 14:00:11 (a -> a) -> a 14:00:20 That begins with (a. 14:00:25 but i don't think you'll be able to get a space. 14:00:59 (:t 7 14:01:18 :( 14:01:43 (we don't want idris-ircslave to give error messages everyone writes like this.) 14:01:56 *+everytime someone 14:02:00 *-+ 14:02:09 i think my brain needs service. 14:02:15 *+-/^ 14:10:42 -!- shikhin has quit (Read error: Connection reset by peer). 14:12:07 -!- tertu has joined. 14:13:24 a dog is barking. some asshole got a new one. time to buy poison. 14:14:13 hm that misses a season. make that "barking dog in spring." 14:15:32 let's hope it's just visiting. 14:16:02 -!- shikhin has joined. 14:17:53 yesterday night, around 11pm EDT, my neighbours randomly guffawed. it was... more weird than anything else. 14:18:59 -!- FreeFull has quit (Read error: Operation timed out). 14:30:07 -!- boily has quit (Quit: SHOWERED CHICKEN). 14:33:09 sadly, it's not just visiting. it's in the apartment next to mine that has been vacant all until now. 14:33:58 i have to move. 14:34:29 imo move to York 14:35:58 keep the viking theme 15:20:04 oerjan: Lambda arguments currently require commas between, i.e. (\x y => …) doesn’t parse, it needs to be (\x,y => …). I think somebody really really wants to change that, but I don’t know if or when that change might show up. 15:20:25 Taneb: There currently is no (^) operator in the prelude. 15:20:40 ( :t pow 15:20:41 Prelude.pow : Num a => a -> Nat -> a 15:21:09 That does exist though. Should be renamed or aliased. 15:35:20 yay the dog stopped while i was shaving. i think its humans came back 15:41:02 ( :t with Stream foldr (\x, y => x :: Delay y) 15:41:02 Can't resolve type class Foldable t 15:41:36 ( :t with Stream foldr (\x, y => the (Stream a) (x :: Delay y)) 15:41:37 (input):1:44:No such variable a 15:41:44 ( :t with Stream foldr (\x, y => the (Stream _) (x :: Delay y)) 15:41:44 Can't resolve type class Foldable t 15:41:55 i guess Stream just isn't foldable. 15:42:38 although obviously there _are_ codata versions of folds in some cases... 15:43:35 oh wait hm 15:44:15 ( :t \z => with Stream foldr (\x, y => the (Stream _) (x :: Delay y)) z z 15:44:15 Can't resolve type class Foldable Stream 15:44:20 nope. 15:44:52 ( the (Foldable List) %instance 15:44:52 constructor of Prelude.Foldable.Foldable (\{meth0} => \{meth1} => \{meth2} => \{meth3} => \{meth4} => List instance of Prelude.Foldable.Foldable, method foldr meth meth meth) : Foldable List 15:45:07 ( the (Foldable Stream) %instance 15:45:08 Can't resolve type class Foldable Stream 15:45:31 ( :t %instance 15:45:32 (input):0:0:Incomplete term refl 15:46:12 ( :doc Foldable 15:46:13 Type class Foldable 15:46:13 Methods: 15:46:13 foldr : Foldable t => (elt -> acc -> acc) -> acc -> (t elt) -> acc 15:46:13 Arguments: 15:46:13 Class constraint Foldable t↵… 15:47:00 oerjan: %instance means “fill this term in using instance search”. 15:47:04 ( :doc Traversable 15:47:04 Type class Traversable 15:47:05 Methods: 15:47:05 traverse : Traversable t => Applicative f => (a -> f b) -> (t a) -> f (t b) 15:47:05 Arguments: 15:47:05 Class constraint Traversable t↵… 15:47:42 And type class instances are actual values. 15:47:44 ( :t State 15:47:44 No such variable State 15:47:48 ( :t StateT 15:47:48 No such variable StateT 15:48:09 Not imported at present. 15:48:49 i think idris-ircslave has deviously dropped everything that could be used to create a fibonacci stream. 15:49:55 -!- idris-ircslave has quit (Quit: Terminated). 15:50:10 -!- idris-ircslave has joined. 15:50:21 i cannot guarantee that State would work though, maybe it's too strict. 15:50:27 ( :t State 15:50:28 No such variable State 15:50:53 ( :t STATE 15:50:54 No such variable STATE 15:51:05 ( :t ZZ 15:51:06 No such variable ZZ 15:51:10 monads are all caps? 15:51:14 Okay, something went wrong. 15:51:28 No, just checking for somethinge else that should have been there. 15:52:13 ( :t fix 15:52:13 No such variable fix 15:52:19 ( :t (+) 15:52:20 Prelude.Classes.+ : Num a => a -> a -> a 15:53:17 -!- idris-ircslave has quit (Client Quit). 15:53:34 -!- idris-ircslave has joined. 15:53:40 ( :t ZZ 15:53:41 No such variable ZZ 15:53:50 Dang. One moment. 15:54:13 -!- idris-ircslave has quit (Client Quit). 15:54:29 -!- idris-ircslave has joined. 15:54:35 ( :t ZZ 15:54:36 No such variable ZZ 15:54:42 Fffff… 15:56:10 >.< 15:58:57 I recently added an unrelated incorrect import and didn’t test it after that. 15:59:19 fanZZy 16:00:03 Not the ZZ, I thought there was still Data.Uninhabited, but that got moved into Prelude sometime. 16:00:22 -!- tromp has joined. 16:00:31 ( :doc Uninhabitated 16:00:31 No documentation for Uninhabitated 16:00:40 ( :doc Uninhabited 16:00:41 Type class Uninhabited 16:00:41 Methods: 16:00:41 uninhabited : Uninhabited t => t -> _|_ 16:00:41 If I have a t, I've had a contradiction 16:00:41 Arguments:↵… 16:01:18 ( :t absurd 16:01:19 Prelude.Uninhabited.absurd : Uninhabited t => t -> a 16:02:04 -!- shikhout has joined. 16:02:10 (Which is just (FalseElim . uninhabited).) 16:03:01 So, I took the opportunity to update my Idris, I’ll restart once more in a moment and hopefully we’ll have our imports again. 16:03:39 oerjan: Also, yes, the State is almost certainly too strict for generating a Stream in its state. 16:04:28 darn 16:05:19 -!- shikhin has quit (Ping timeout: 264 seconds). 16:05:20 -!- shikhout has changed nick to shikhin. 16:05:47 -!- idris-ircslave has quit (Quit: Terminated). 16:06:02 -!- idris-ircslave has joined. 16:06:17 Hmm. 16:06:49 ( :t State 16:06:49 Effect.State.State : Effect 16:06:49 Control.Monad.State.State : Type -> Type -> Type 16:07:03 Yay. 16:08:23 (Funny how those are opposite-colored.) 16:08:38 ( State 16:08:38 Can't disambiguate name: Effect.State.State, Control.Monad.State.State 16:08:49 ( Monad.State.State 16:08:49 State : Type -> Type -> Type 16:09:04 ( \x y => Monad.State.State x y 16:09:04 (input):1:2: error: expected: lambda expression 16:09:04 \x y => Monad.State.State x y 16:09:05 ^ 16:09:09 ( \x, y => Monad.State.State x y 16:09:09 \x => \y => StateT x Identity y : Type -> Type -> Type 16:09:42 ( Effect 16:09:43 (x : Type) -> Type -> (x -> Type) -> Type : Type 16:10:00 ( :doc Stream 16:10:00 Data type Stream : Type -> Type 16:10:00 An infinite stream 16:10:01 Arguments: 16:10:01 __pi_arg : Type 16:10:01 Constructors:↵… 16:11:22 ( let fib 0 = 1; fib 1 = 1; fib n = fib (n-1) + fib (n-2) in fib (the Integer 3) 16:11:22 (input):1:14: error: expected: "$", 16:11:22 "$>", "&&", "&&&", "*", "***", 16:11:22 "+", "++", "-", "->", ".", "/", 16:11:22 "/=", ":+", ":-", "::", ":::", 16:11:22 ":=", "<", "<$", "<$>", "<*>",↵… 16:12:12 someone said idris allowed ; in place of whitespace, they were confused. 16:12:39 I don’t think you can have multiple clauses in let. 16:12:41 or just another missing syntax i guess. 16:12:50 wat. 16:12:54 -!- MoALTz has joined. 16:13:24 ok get back to me when idris is no longer subtly broken everywhere twh 16:13:35 For multiple bindings, I think you have to nest lets. 16:13:55 ( let next (a,b) = (b,a+b) in take 10 (iterate next (Z,S Z)) 16:13:55 (input):1:19:No such variable b 16:14:17 ooh iterate 16:14:45 all is not lost 16:15:16 ( let next = \(a,b) => (b,a+b) in take 10 (iterate next (Z,S Z)) 16:15:16 [(0, 1), (1, 1), (1, 2), (2, 3), (3, 5), (5, 8), (8, 13), (13, 21), (21, 34), (34, 55)] : Vect 10 (Nat, Nat) 16:15:43 ( let next = \(a,b) => (b,a+b) in map head $ take 10 (iterate next (Z,S Z)) 16:15:44 (input):1:42:Can't disambiguate name: Prelude.List.head, Prelude.Stream.head, Prelude.Vect.head 16:15:59 It’s fst, not head. 16:16:03 oh hm 16:16:10 ( let next = \(a,b) => (b,a+b) in map fst $ take 10 (iterate next (Z,S Z)) 16:16:12 [0, 1, 1, 2, 3, 5, 8, 13, 21, 34] : Vect 10 Nat 16:16:29 although i find it quite silly to have both overloading and type classes. 16:16:30 ( let next = \(a,b) => (b,a+b) in take 10 (map fst (iterate next (Z,S Z))) 16:16:30 [0, 1, 1, 2, 3, 5, 8, 13, 21, 34] : Vect 10 Nat 16:17:29 Type classes are useful for abstracting across, but sometimes you need a different signature. 16:17:43 ( :t (<$>) 16:17:43 Prelude.Applicative.<$> : Applicative f => (f (a -> b)) -> (f a) -> f b 16:17:43 Effects.<$> : (Eff m (a -> b) xs (\v => xs)) -> (Eff m a xs (\v1 => xs)) -> Eff m b xs (\v2 => xs) 16:18:36 yes, but are those heads _really_ that incompatible. 16:18:42 ( :t List.head 16:18:44 Prelude.List.head : (l : List a) -> (isCons l = True) -> a 16:18:50 ( :t Stream.head 16:18:50 Prelude.Stream.head : (Stream a) -> a 16:18:51 ( :t head 16:18:51 Prelude.List.head : (l : List a) -> (isCons l = True) -> a 16:18:51 Prelude.Stream.head : (Stream a) -> a 16:18:51 Prelude.Vect.head : (Vect (S n) a) -> a 16:18:55 oh 16:19:28 hm i guess the List one doesn't quite fit. 16:19:29 For a list, you need a proof it is nonempty. For a stream, there is no condition. For a Vect, it needs to be indexed by a successor. 16:20:00 eek, someone restarted the dog. 16:24:00 List.head is almost useless this way; the type for the proof is a poor choice for actual use. Generally, better to just pattern match and be done. 16:24:26 ( :t group 16:24:26 No such variable group 16:24:46 ( :t groupBy 16:24:48 No such variable groupBy 16:25:03 those always give nonempty elements. 16:25:16 (if they exist somewhere) 16:26:16 Probably why nobody has added them yet: They’ll want a type involving nonempty lists. 16:26:44 ah 16:27:14 (And we don’t have a standard type for nonempty lists yet.) 16:27:31 ( :t index 16:27:31 Data.HVect.index : (i : Fin k) -> (HVect ts) -> index i ts 16:27:31 Prelude.List.index : (n : Nat) -> (l : List a) -> (lt n (length l) = True) -> a 16:27:31