00:19:52 -!- tromp_ has joined.
00:24:15 -!- tromp_ has quit (Ping timeout: 246 seconds).
00:59:16 -!- tromp has joined.
01:04:05 -!- tromp has quit (Ping timeout: 272 seconds).
02:15:40 -!- imode has joined.
03:35:08 -!- adu has joined.
03:57:28 -!- imode has quit (Ping timeout: 265 seconds).
04:39:23 -!- imode has joined.
04:47:31 -!- ArthurSt1ong has quit (Quit: leaving).
04:47:50 -!- ArthurStrong has joined.
04:56:09 <Sgeo> "One way to think about dependent types is to think of them as “first class” objects in the language, in that they can be assigned to variables, passed around and returned from functions, just like any other construct. But, if they’re truly first class, we should be able to pattern match on them too! Idris 2 allows us to do this. For example"
04:56:24 <Sgeo> I thought pattern matching on types was antithetical to the concept of Idris?
05:12:40 <esowiki> [[Special:Log/newusers]] create * Jcs * New user account
05:17:03 <zzo38> Maybe it is antithetical to Idris but not Idris 2. But, I don't know enough of Idris to really know that, anyways
05:19:16 <esowiki> [[Esolang:Introduce yourself]] https://esolangs.org/w/index.php?diff=73168&oldid=73137 * Jcs * (+151)
05:21:07 <esowiki> [[Esolang:Introduce yourself]] https://esolangs.org/w/index.php?diff=73169&oldid=73168 * Jcs * (-151)
05:42:53 <esowiki> [[User talk:Emerald]] N https://esolangs.org/w/index.php?oldid=73170 * JonoCode9374 * (+525) Created page with "==Tips For Making a Golfing Language== A while ago, there was a thread over on the Code Golf StackExchange (CGCC) about things to consider when making a golfing language: htt..."
06:22:28 <esowiki> [[Special:Log/newusers]] create * NikolayResh * New user account
06:23:49 -!- tromp has joined.
06:28:59 -!- tromp has quit (Ping timeout: 272 seconds).
06:31:14 -!- adu has quit (Quit: adu).
06:36:23 -!- tromp has joined.
06:47:24 <esowiki> [[Esolang:Introduce yourself]] https://esolangs.org/w/index.php?diff=73171&oldid=73169 * NikolayResh * (+231) /* Introductions */
06:50:15 <esowiki> [[Brainfuck implementations]] https://esolangs.org/w/index.php?diff=73172&oldid=72159 * NikolayResh * (+106) /* Normal implementations */
07:10:18 -!- j-bot has quit (Remote host closed the connection).
07:29:48 <shachaf> Sgeo: Do they actually lose parametricity?
07:30:00 <shachaf> I doubt it. I think it's something a bit more subtle than that.
07:32:00 <Sgeo> A function that wants to match on a type has to note that it's accepting a type in its type signature
07:32:17 <Sgeo> https://idris2.readthedocs.io/en/latest/tutorial/multiplicities.html
07:32:22 <Sgeo> "Note that multiplicities on the binders, and the ability to pattern match on non-erased types mean that the following two types are distinct
07:32:31 <Sgeo> notId : {a : Type} -> a -> a
07:37:28 <b_jonas> so that's like when you have an Any class in Haskell, but you can match types on it because the Any class has a method that lets you macth the types, and the class constraint is passed explicitly?
07:52:57 -!- rain1 has joined.
08:03:35 -!- b_jonas has quit (Remote host closed the connection).
08:29:46 -!- imode has quit (Ping timeout: 246 seconds).
08:42:32 <shachaf> Isn't that thing just the way they write forall?
08:49:34 -!- craigo has quit (Ping timeout: 240 seconds).
08:49:55 -!- Sgeo has quit (Read error: Connection reset by peer).
09:20:33 -!- wib_jonas has joined.
09:59:36 -!- ArthurStrong has quit (Ping timeout: 272 seconds).
10:21:56 -!- S_Gautam has joined.
10:46:24 -!- TheLie has joined.
10:49:46 -!- tromp has quit (Remote host closed the connection).
10:56:00 -!- LKoen has joined.
10:59:33 -!- Lord_of_Life_ has joined.
11:00:32 -!- Lord_of_Life has quit (Ping timeout: 256 seconds).
11:00:53 -!- Lord_of_Life_ has changed nick to Lord_of_Life.
11:01:14 -!- cpressey has joined.
11:25:03 -!- Phantom_Hoover has joined.
12:05:30 -!- cpressey has quit (Quit: WeeChat 1.9.1).
12:17:27 <int-e> . o O ( I don't want dependent types. I want dependable types. )
12:54:54 <wib_jonas> "seal" is an abbreviation for "sea lion".
13:11:34 -!- S_Gautam has quit (Quit: Connection closed for inactivity).
13:32:06 -!- cpressey has joined.
13:38:47 <esowiki> [[Cubix]] M https://esolangs.org/w/index.php?diff=73173&oldid=52635 * PythonshellDebugwindow * (+23) /* Links */ category languages
13:42:33 <esowiki> [[Glypho]] M https://esolangs.org/w/index.php?diff=73174&oldid=53687 * PythonshellDebugwindow * (+28) /* External resources */
13:49:21 -!- TheLie has quit (Remote host closed the connection).
14:03:15 -!- rain1 has quit (Quit: leaving).
14:16:08 <esowiki> [[Dogescript]] M https://esolangs.org/w/index.php?diff=73175&oldid=53778 * DmilkaSTD * (+14)
14:47:17 -!- rain1 has joined.
14:50:00 <esowiki> [[User talk:Truttle1]] https://esolangs.org/w/index.php?diff=73176&oldid=68710 * DmilkaSTD * (+110)
14:57:08 -!- tromp has joined.
15:01:42 -!- tromp has quit (Ping timeout: 246 seconds).
15:11:54 <esowiki> [[BF-ASM:8]] https://esolangs.org/w/index.php?diff=73177&oldid=73074 * DmilkaSTD * (-2474) Replaced content with "{{WIP}} ::Got an amazing idea for Brainfuck"
15:19:43 -!- wib_jonas has quit (Quit: Connection closed).
15:23:46 <cpressey> https://mathoverflow.net/a/361870 seems fairly esoteric.
15:29:19 -!- xelxebar has quit (Remote host closed the connection).
15:32:12 -!- xelxebar has joined.
16:00:39 -!- cpressey has quit (Quit: WeeChat 1.9.1).
16:18:22 -!- Cale has quit (Ping timeout: 260 seconds).
16:30:40 -!- Cale has joined.
16:31:46 -!- b_jonas has joined.
16:32:39 -!- tromp has joined.
16:49:33 <rain1> I knew rices theorem was false
16:52:43 -!- adu has joined.
17:05:50 <esowiki> [[BF-ASM:8]] M https://esolangs.org/w/index.php?diff=73178&oldid=73177 * PythonshellDebugwindow * (+24)
17:06:40 <esowiki> [[Mice in a maze/mice.py]] M https://esolangs.org/w/index.php?diff=73179&oldid=58067 * PythonshellDebugwindow * (+30) /* Comments */
17:07:23 <esowiki> [[Streetcode]] M https://esolangs.org/w/index.php?diff=73180&oldid=72083 * PythonshellDebugwindow * (+36) /* Turing-completeness proof */
17:07:39 <esowiki> [[COD]] M https://esolangs.org/w/index.php?diff=73181&oldid=73098 * PythonshellDebugwindow * (+36) /* Raise an error (takes 3 inputs first) */
17:09:27 -!- zseri has joined.
17:21:08 -!- TheLie has joined.
17:30:24 -!- Sgeo has joined.
17:44:50 -!- tromp has quit (Remote host closed the connection).
17:52:58 -!- tromp has joined.
18:11:02 -!- Phantom_Hoover has quit (Ping timeout: 260 seconds).
18:29:19 <b_jonas> fungot, is it logically possible that there exist worlds that are carried by five or more elephants, rather than just the usual four, and how would you resolve the apparent contradiction with the Bible?
18:29:20 <fungot> b_jonas: that's what we get after doing your initial decoding step. but first i need to use another version; i'm advising you to use disorient me!
18:31:20 <b_jonas> yes, I can understand if that radical hypothesis disorients you.
18:32:27 -!- zseri has quit (Quit: zseri).
18:32:47 -!- imode has joined.
18:52:31 -!- Vorpal has quit (Quit: ZNC - http://znc.sourceforge.net).
18:58:07 <zzo38> Maybe I will need to add the possibility of "sections" with their own margins, within a text area, where in some cases other stuff may be aligned and printed within the margins.
18:58:55 <zzo38> For example, it may be applicable to Sagas and planeswalkers in Magic: the Gathering.
19:02:54 -!- user24 has joined.
19:06:10 <int-e> rain1: only if you're imprecise
19:09:13 <int-e> That link is interesting though, I had not heard of Friedberg's theorem.
19:23:48 -!- zseri has joined.
19:24:46 -!- adu has quit (Quit: adu).
19:40:47 -!- craigo has joined.
19:58:00 -!- Phantom_Hoover has joined.
20:13:07 <esowiki> [[BF-ASM:8]] https://esolangs.org/w/index.php?diff=73182&oldid=73178 * DmilkaSTD * (+90)
20:33:51 -!- TheLie has quit (Ping timeout: 246 seconds).
20:39:01 <esowiki> [[BF-ASM:8]] https://esolangs.org/w/index.php?diff=73183&oldid=73182 * DmilkaSTD * (+1058)
20:47:09 <esowiki> [[Special:Log/upload]] upload * DmilkaSTD * uploaded "[[File:BfAsmMemoryManagementGraph.png]]"
20:50:38 <esowiki> [[BF-ASM:8]] https://esolangs.org/w/index.php?diff=73185&oldid=73183 * DmilkaSTD * (+78)
20:59:40 -!- rain1 has quit (Quit: leaving).
21:03:07 -!- TheLie has joined.
21:12:31 <esowiki> [[BF-ASM:8]] M https://esolangs.org/w/index.php?diff=73186&oldid=73185 * PythonshellDebugwindow * (+77) /* Memory management */ catas
21:12:46 -!- user24 has quit (Quit: Leaving).
21:15:48 <esowiki> [[Plugh]] M https://esolangs.org/w/index.php?diff=73187&oldid=67009 * PythonshellDebugwindow * (+100)
21:18:37 -!- aloril_ has quit (Ping timeout: 256 seconds).
21:35:13 -!- j-bot has joined.
21:49:48 -!- aloril has joined.
21:57:46 -!- ArthurStrong has joined.
22:26:27 -!- imode has quit (Ping timeout: 240 seconds).
22:26:47 -!- imode has joined.
22:30:28 -!- ArthurStrong has quit (Quit: leaving).
22:31:24 -!- imode has quit (Ping timeout: 256 seconds).
22:53:21 -!- imode has joined.
23:01:18 -!- Lord_of_Life_ has joined.
23:02:14 -!- Lord_of_Life has quit (Ping timeout: 260 seconds).
23:02:37 -!- Lord_of_Life_ has changed nick to Lord_of_Life.
23:05:57 -!- moony has changed nick to thoony.
23:07:12 -!- TheLie has quit (Remote host closed the connection).
23:07:50 -!- Phantom_Hoover has quit (Ping timeout: 260 seconds).
23:09:53 -!- imode has quit (Ping timeout: 252 seconds).
23:42:38 -!- thoony has quit (Quit: Bye!).
23:44:28 -!- moony has joined.