| 2025-03-30 00:08:45 +0100 | rekahsoft | (~rekahsoft@bras-base-orllon1103w-grc-19-74-12-85-11.dsl.bell.ca) (Ping timeout: 276 seconds) |
| 2025-03-30 00:15:19 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-03-30 00:16:31 +0100 | connrs_ | (~connrs@conners.plus.com) (Remote host closed the connection) |
| 2025-03-30 00:16:39 +0100 | connrs_ | (~connrs@conners.plus.com) |
| 2025-03-30 00:17:05 +0100 | connrs | (~connrs@user/connrs) (Quit: ZNC 1.9.1 - https://znc.in) |
| 2025-03-30 00:17:05 +0100 | connrs_ | connrs |
| 2025-03-30 00:17:11 +0100 | connrs | (~connrs@conners.plus.com) (Remote host closed the connection) |
| 2025-03-30 00:17:19 +0100 | connrs | (~connrs@user/connrs) connrs |
| 2025-03-30 00:26:15 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-03-30 00:28:33 +0100 | connrs | (~connrs@user/connrs) (Remote host closed the connection) |
| 2025-03-30 00:28:41 +0100 | connrs | (~connrs@user/connrs) connrs |
| 2025-03-30 00:31:01 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2025-03-30 00:35:12 +0100 | ljdarj1 | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-03-30 00:35:33 +0100 | peterbecich1 | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-03-30 00:37:54 +0100 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds) |
| 2025-03-30 00:37:54 +0100 | ljdarj1 | ljdarj |
| 2025-03-30 00:38:47 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 244 seconds) |
| 2025-03-30 00:39:06 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-03-30 00:42:04 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-03-30 00:42:24 +0100 | peterbecich1 | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 244 seconds) |
| 2025-03-30 00:50:40 +0100 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) Unicorn_Princess |
| 2025-03-30 00:54:45 +0100 | peterbecich1 | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-03-30 00:56:39 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 244 seconds) |
| 2025-03-30 00:57:42 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-03-30 00:57:46 +0100 | peterbecich1 | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Client Quit) |
| 2025-03-30 01:02:04 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds) |
| 2025-03-30 01:04:24 +0100 | otto_s | (~user@p4ff27624.dip0.t-ipconnect.de) (Ping timeout: 260 seconds) |
| 2025-03-30 01:06:02 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-03-30 01:06:05 +0100 | otto_s | (~user@p5de2f2eb.dip0.t-ipconnect.de) |
| 2025-03-30 01:12:05 +0100 | <haskellbridge> | <thirdofmay18081814goya> does anyone know of an invertible coding function "Int -> Int" for a value of type "Tree Int"? i.e., translate a value "Tree Int" into a value "Int" and have a unique way to translate an "Int" back into a "Tree Int" |
| 2025-03-30 01:12:26 +0100 | <haskellbridge> | <thirdofmay18081814goya> does anyone know of an invertible coding function "Tree Int -> Int"* |
| 2025-03-30 01:13:09 +0100 | <haskellbridge> | <thirdofmay18081814goya> suppose specifically a rose tree with values "Int" |
| 2025-03-30 01:13:38 +0100 | hattckory | (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) (Ping timeout: 248 seconds) |
| 2025-03-30 01:16:30 +0100 | <haskellbridge> | <dmjio> thirdofmay18081814goya did you tree "foldTree" and "unfoldTree" |
| 2025-03-30 01:16:43 +0100 | <haskellbridge> | <dmjio> * try |
| 2025-03-30 01:18:29 +0100 | <haskellbridge> | <Bowuigi> thirdofmay18081814goya I don't see how that could be total, since you have to fit many values of Int in a single one, any of which can be as large as INT_MAX |
| 2025-03-30 01:18:37 +0100 | causal | (~eric@50.35.84.231) causal |
| 2025-03-30 01:18:37 +0100 | <Leary> | thirdofmay: Impossible; |Tree Int| > |Int|. If you wanted an invertible `Tree Integer -> Integer`, then you're essentially doing de/serialisation. |
| 2025-03-30 01:20:45 +0100 | <haskellbridge> | <Bowuigi> If you ignore size concerns and want an invertible "Tree Integer -> Integer", you can get one by treating the output integer as a binary file |
| 2025-03-30 01:20:56 +0100 | <geekosaur> | gödel coding /s |
| 2025-03-30 01:21:36 +0100 | <haskellbridge> | <thirdofmay18081814goya> Leary: this is not the case, note that any element of "Tree Int" is constructible in a finite number of steps, so can be encoded by a function "Nat -> Tree Int", and therefore "Tree Int" has the same size as "Int" (since "| Int | = | Nat |") |
| 2025-03-30 01:22:57 +0100 | <haskellbridge> | <Bowuigi> Wouldn't that mean that it's possible to encode its zipper instead of the actual tree? |
| 2025-03-30 01:23:48 +0100 | tromp | (~textual@2001:1c00:3487:1b00:9865:6ec1:d353:2dc8) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-03-30 01:25:30 +0100 | <haskellbridge> | <thirdofmay18081814goya> Bowuigi: yeah, am just looking for any function that can uniquely specify a tree + an ordering on "Tree Int" that we can use this function with |
| 2025-03-30 01:26:04 +0100 | <haskellbridge> | <Bowuigi> Also note that finite doesn't mean it's inside an Int's bounds |
| 2025-03-30 01:29:34 +0100 | <__monty__> | Int is not Integer. And neither is the same as the mathematical concept. |
| 2025-03-30 01:30:54 +0100 | hattckory | (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) |
| 2025-03-30 01:31:10 +0100 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |
| 2025-03-30 01:32:35 +0100 | <Leary> | thirdofmay: |Int| = 2^64 |
| 2025-03-30 01:33:33 +0100 | <Leary> | (or 2^32 if you live in the past) |
| 2025-03-30 01:34:11 +0100 | <haskellbridge> | <thirdofmay18081814goya> Leary: oh you're fully right then |
| 2025-03-30 01:34:53 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 244 seconds) |
| 2025-03-30 01:35:05 +0100 | <haskellbridge> | <thirdofmay18081814goya> didn't realize "Int" was finite, I thought it was the type of Nat + (Nat - 1) |
| 2025-03-30 01:35:32 +0100 | <haskellbridge> | <thirdofmay18081814goya> * { 0 }) |
| 2025-03-30 01:36:05 +0100 | <haskellbridge> | <thirdofmay18081814goya> a type isomorphic to "Nat + (Nat - { 0 })"* |
| 2025-03-30 01:38:34 +0100 | <haskellbridge> | <thirdofmay18081814goya> then as a matter of fact, "Int !! (| Int | + 1)" will not be a value of type "Int", correct? |
| 2025-03-30 01:38:59 +0100 | <monochrom> | Actually in Haskell we don't have a "Nat", we have Word (Data.Word) and Natural (Numeric.Natural). |
| 2025-03-30 01:39:30 +0100 | <monochrom> | Unpopular opinion: It is more consistent to s/Word/Nat/ because Int : Nat :: Integer :: Natural |
| 2025-03-30 01:39:31 +0100 | <haskellbridge> | <Bowuigi> It would overflow I think, in C it is UB but not sure about it in Haskell |
| 2025-03-30 01:40:53 +0100 | <Leary> | > maxBound + (1 :: Int) == minBound |
| 2025-03-30 01:40:54 +0100 | <lambdabot> | True |
| 2025-03-30 01:41:01 +0100 | <haskellbridge> | <Bowuigi> Word kinda makes sense because of machine words, but UInt or Nat would make more sense |
| 2025-03-30 01:41:05 +0100 | <Leary> | > (succ maxBound :: Int) == minBound |
| 2025-03-30 01:41:07 +0100 | <lambdabot> | *Exception: Prelude.Enum.succ{Int}: tried to take `succ' of maxBound |
| 2025-03-30 01:41:29 +0100 | <monochrom> | You can always try maxBound + 1 |
| 2025-03-30 01:41:42 +0100 | hattckory | (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) (Ping timeout: 276 seconds) |
| 2025-03-30 01:43:00 +0100 | ChaiTRex | (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
| 2025-03-30 01:43:47 +0100 | JuanDaugherty | (~juan@user/JuanDaugherty) JuanDaugherty |
| 2025-03-30 01:43:47 +0100 | <haskellbridge> | <thirdofmay18081814goya> hm so there's an invertible serialization/deserialization function for "Tree Natural"? (or "Tree Word", assuming I understand correctly that "| Word | = | Natural |"?) |
| 2025-03-30 01:44:11 +0100 | <haskellbridge> | <thirdofmay18081814goya> and "| Natural | = | Set of natural numbers |" |
| 2025-03-30 01:44:15 +0100 | <haskellbridge> | <Bowuigi> No, Natural is Integer but unsigned |
| 2025-03-30 01:44:19 +0100 | ChaiTRex | (~ChaiTRex@user/chaitrex) ChaiTRex |
| 2025-03-30 01:44:26 +0100 | <monochrom> | In Haskell2010 it's simulataneously "UB" and "implementation-defined". The exact quote: "The results of exceptional conditions (such as overflow or underflow) on the fixed-precision numeric types are undefined; an implementation may choose error (⊥, semantically), a truncated value, or a special value such as infinity, indefinite, etc." |
| 2025-03-30 01:45:56 +0100 | <haskellbridge> | <Bowuigi> Also is Natural the same size as the set of natural numbers? It has bottoms too |
| 2025-03-30 01:46:53 +0100 | <haskellbridge> | <thirdofmay18081814goya> no it seems, assuming "Natural" has the size of the set of unsigned integers, it is a finite set too |
| 2025-03-30 01:47:06 +0100 | <haskellbridge> | <Bowuigi> Not only implementation-wise, but also because every computation of type Natural is a Natural, including "1 + undefined" |
| 2025-03-30 01:47:48 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-03-30 01:48:23 +0100 | <haskellbridge> | <thirdofmay18081814goya> so is there no type that has the size of the set of natural numbers in haskell? |
| 2025-03-30 01:48:30 +0100 | <monochrom> | > 10^100 :: Natural |
| 2025-03-30 01:48:31 +0100 | <lambdabot> | 1000000000000000000000000000000000000000000000000000000000000000000000000000... |
| 2025-03-30 01:48:33 +0100 | <Leary> | thirdofmay: |Word| = |Int|; |Natural| = |Integer| = omega |
| 2025-03-30 01:48:49 +0100 | <haskellbridge> | <thirdofmay18081814goya> ah that clears it up, ty |
| 2025-03-30 01:50:32 +0100 | <haskellbridge> | <thirdofmay18081814goya> so rephrasing: there is an invertible serialization function for "Tree Natural", correct? |
| 2025-03-30 01:51:12 +0100 | <haskellbridge> | <thirdofmay18081814goya> what would be the API to access it? |
| 2025-03-30 01:55:26 +0100 | <geekosaur> | that's a somewhat weird way to put it. I would say that you can define such a function, not that one exists with a particular API |
| 2025-03-30 01:55:38 +0100 | <geekosaur> | how you define it would depend on what you intend to do with it |
| 2025-03-30 01:56:20 +0100 | <geekosaur> | (My comment about Gödel coding was only half a joke; it would certainly work but would be overkill and probably extremely inefficient for your purpose) |
| 2025-03-30 01:58:14 +0100 | <haskellbridge> | <thirdofmay18081814goya> wrt Godel coding, beginning to read http://foibg.com/ijita/vol17/ijita17-1-p02.pdf |
| 2025-03-30 01:58:23 +0100 | <haskellbridge> | <thirdofmay18081814goya> not terribly preoccupied with efficiency atm |
| 2025-03-30 01:59:37 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-03-30 03:00:49 +0200 | causal | (~eric@50.35.84.231) (Quit: WeeChat 4.5.1) |
| 2025-03-30 03:01:37 +0200 | sprotte24_ | (~sprotte24@p200300d16f1c4e0098c546d077431e36.dip0.t-ipconnect.de) (Quit: Leaving) |
| 2025-03-30 03:03:53 +0200 | <monochrom> | Unpopular opinion: But Gödel numbers is terribly preoccupied with gross inefficiency. |
| 2025-03-30 03:04:49 +0200 | <geekosaur> | ^ |
| 2025-03-30 03:05:43 +0200 | <haskellbridge> | <thirdofmay18081814goya> monochrom: what's an alternative? |
| 2025-03-30 03:05:52 +0200 | <haskellbridge> | <thirdofmay18081814goya> any alternative |
| 2025-03-30 03:06:13 +0200 | <monochrom> | You should look at the binary package and what it does to "instance Binary (Tree e)" |
| 2025-03-30 03:06:20 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) (Quit: ChaiTRex) |
| 2025-03-30 03:06:42 +0200 | <haskellbridge> | <thirdofmay18081814goya> "Data.Binary" that is? |
| 2025-03-30 03:07:23 +0200 | <monochrom> | Sure, if module names are still unambiguous like 20 years ago. |
| 2025-03-30 03:07:53 +0200 | <haskellbridge> | <thirdofmay18081814goya> will do, thanks a lot for the reference. am literally looking for anything that works lol |
| 2025-03-30 03:11:28 +0200 | <geekosaur> | heh. let's put it this way: countably infinite Gödel numbers are considered a feature for their use case |
| 2025-03-30 03:11:51 +0200 | <geekosaur> | (only a slight overstatement) |
| 2025-03-30 03:12:16 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-03-30 03:12:28 +0200 | <geekosaur> | well, arguably so are uncountably infinite ones, at least as results 🙂 |
| 2025-03-30 03:13:11 +0200 | hattckory | (~hattckory@70.27.118.207) |
| 2025-03-30 03:18:01 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) ChaiTRex |
| 2025-03-30 03:21:35 +0200 | harveypwca | (~harveypwc@2601:246:d080:f6e0:27d6:8cc7:eca9:c46c) |
| 2025-03-30 03:25:46 +0200 | <haskellbridge> | <jv> 'd |
| 2025-03-30 03:26:51 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 246 seconds) |
| 2025-03-30 03:32:58 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 244 seconds) |
| 2025-03-30 03:38:24 +0200 | toby-bro | (~toby-bro@user/toby-bro) (Ping timeout: 272 seconds) |
| 2025-03-30 03:46:27 +0200 | roconnor | (~quassel@rocq/roconnor) (Ping timeout: 246 seconds) |
| 2025-03-30 03:47:08 +0200 | roconnor | (~quassel@rocq/roconnor) roconnor |
| 2025-03-30 03:48:18 +0200 | <EvanR> | thirdofmay18081814goya, data Nat = Z | S !Nat |
| 2025-03-30 03:49:01 +0200 | <EvanR> | ignoring bottoms |
| 2025-03-30 03:49:03 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
| 2025-03-30 03:49:10 +0200 | <haskellbridge> | <thirdofmay18081814goya> right |
| 2025-03-30 03:50:48 +0200 | <EvanR> | data Int = Nat :- Nat |
| 2025-03-30 03:51:50 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) (Quit: ChaiTRex) |
| 2025-03-30 03:51:53 +0200 | tremon | (~tremon@83.80.159.219) (Quit: getting boxed in) |
| 2025-03-30 03:52:58 +0200 | acidjnk | (~acidjnk@p200300d6e71c4f5684d81f92e812b9d0.dip0.t-ipconnect.de) (Ping timeout: 272 seconds) |
| 2025-03-30 03:56:36 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) (Read error: Connection timed out) |
| 2025-03-30 03:59:51 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) ChaiTRex |
| 2025-03-30 04:00:40 +0200 | <EvanR> | data Rat = Over { numer :: Int, denomMinusOne :: Nat } |
| 2025-03-30 04:01:46 +0200 | <geekosaur> | I was going to say you got that backwards, but in hindsight I guess it depends on how you interpret that name |
| 2025-03-30 04:02:18 +0200 | <EvanR> | data Real = Rat Rat | Lim (Rat -> Real) |
| 2025-03-30 04:05:04 +0200 | op_4 | (~tslil@user/op-4/x-9116473) (Remote host closed the connection) |
| 2025-03-30 04:05:15 +0200 | roconnor | (~quassel@rocq/roconnor) (Ping timeout: 252 seconds) |
| 2025-03-30 04:05:35 +0200 | op_4 | (~tslil@user/op-4/x-9116473) op_4 |
| 2025-03-30 04:05:47 +0200 | roconnor | (~quassel@rocq/roconnor) roconnor |
| 2025-03-30 04:07:23 +0200 | <EvanR> | data Surreal = Cut (Tree Surreal) (Tree Surreal) |
| 2025-03-30 04:11:44 +0200 | <JuanDaugherty> | issat knuth's? |
| 2025-03-30 04:12:51 +0200 | <JuanDaugherty> | https://en.wikipedia.org/wiki/Surreal_number confirmed |
| 2025-03-30 04:13:11 +0200 | <JuanDaugherty> | (and credit where credit due to Conway) |
| 2025-03-30 04:13:30 +0200 | JuanDaugherty | (~juan@user/JuanDaugherty) (Quit: praxis.meansofproduction.biz (juan@acm.org)) |
| 2025-03-30 04:15:08 +0200 | <EvanR> | I will gratefully deposit 0x$1.00 ($2.56) to the account of the first person who finds and reports anything that remains technically, historically, typographically, or politically incorrect. -- knuth |
| 2025-03-30 04:15:13 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2025-03-30 04:27:48 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-03-30 04:28:43 +0200 | euphores | (~SASL_euph@user/euphores) (Ping timeout: 245 seconds) |
| 2025-03-30 04:33:22 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds) |
| 2025-03-30 04:33:55 +0200 | j1n37 | (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 2025-03-30 04:35:13 +0200 | euphores | (~SASL_euph@user/euphores) euphores |
| 2025-03-30 04:37:48 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-03-30 04:43:52 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-03-30 04:50:46 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-03-30 04:56:22 +0200 | j1n37 | (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 2025-03-30 04:56:57 +0200 | <EvanR> | thirdofmay18081814goya, "any element of Tree Int can be constructed in a finite number of steps" ... |
| 2025-03-30 04:57:16 +0200 | <EvanR> | what's a step |
| 2025-03-30 04:58:15 +0200 | <monochrom> | A step is a finite number of substeps. >:) |
| 2025-03-30 04:59:23 +0200 | <EvanR> | did I construct let xs = 1 : xs in xs in a finite number of steps, or is it even successfully constructed |
| 2025-03-30 05:01:39 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-03-30 05:02:45 +0200 | haritz | (~hrtz@user/haritz) (Remote host closed the connection) |
| 2025-03-30 05:02:55 +0200 | haritz | (~hrtz@2a02:8010:65b5:0:5d9a:9bab:ee5e:b737) |
| 2025-03-30 05:02:57 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-03-30 05:03:06 +0200 | <haskellbridge> | <thirdofmay18081814goya> EvanR: a step is a natural number that designates a pair, given by a natural number and its successor, such that when fed into a function "Nat -> Tree Int", produce a tree that is at most different by a single application of the datatype constructor |
| 2025-03-30 05:03:35 +0200 | <haskellbridge> | <thirdofmay18081814goya> (tentative definition) |
| 2025-03-30 05:03:49 +0200 | <EvanR> | what |
| 2025-03-30 05:04:26 +0200 | <haskellbridge> | <thirdofmay18081814goya> replace "at most one application of the datatype constructor" by "exactly one application" |
| 2025-03-30 05:04:28 +0200 | <EvanR> | are you only allowing finite trees |
| 2025-03-30 05:04:44 +0200 | <haskellbridge> | <thirdofmay18081814goya> yeah in this case, only inductively defined trees |
| 2025-03-30 05:04:46 +0200 | haritz | (~hrtz@2a02:8010:65b5:0:5d9a:9bab:ee5e:b737) (Changing host) |
| 2025-03-30 05:04:46 +0200 | haritz | (~hrtz@user/haritz) haritz |
| 2025-03-30 05:05:14 +0200 | <EvanR> | alright so a step is a constructor |
| 2025-03-30 05:05:38 +0200 | <EvanR> | and there's only finitely many of them |
| 2025-03-30 05:05:50 +0200 | <EvanR> | based |
| 2025-03-30 05:06:29 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-03-30 05:08:00 +0200 | <haskellbridge> | <thirdofmay18081814goya> EvanR: well, I think we need the whole thing: 1. a natural number 2. designating a natural number and its succesor 3. such that fed to a function that indexes constructor applications, 4. produce a tree different by exactly a single application of the "Branch" constructor (if our tree datatype is defined by a "Node" and "Branch" constructor) |
| 2025-03-30 05:09:35 +0200 | <EvanR> | isn't the result of Branch t1 t2 always "a tree different by exactly a single application of the Branch constructor" |
| 2025-03-30 05:10:10 +0200 | <EvanR> | from the pair of trees |
| 2025-03-30 05:12:24 +0200 | <haskellbridge> | <thirdofmay18081814goya> hm true, but supposing the function indexing applications is "ITA" (abbreviating "IndexedTreeApplication"), we want a step to designate the difference between "Branch (ITA n) (ITA m)" and "ITA n", where "m" is strictly smaller than "n" |
| 2025-03-30 05:13:12 +0200 | <haskellbridge> | <thirdofmay18081814goya> or analogously the difference between "Branch (ITA m) (ITA n)" |
| 2025-03-30 05:13:19 +0200 | <haskellbridge> | <thirdofmay18081814goya> and "ITA n" |
| 2025-03-30 05:13:41 +0200 | <EvanR> | I have no idea what the objective was, I just cherry picked this one idea of getting any "Tree Int" in a finite number of steps, which didn't make sense to me in general, but now it does since finite |
| 2025-03-30 05:14:05 +0200 | <haskellbridge> | <thirdofmay18081814goya> heheh right |
| 2025-03-30 05:17:28 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-03-30 05:18:21 +0200 | <EvanR> | true or false: any geometric diagram can be constructed in a finite number of steps |
| 2025-03-30 05:19:44 +0200 | <haskellbridge> | <thirdofmay18081814goya> can we specify the geometric diagram as "[(Integer, Integer)]"? |
| 2025-03-30 05:20:07 +0200 | <haskellbridge> | <thirdofmay18081814goya> in that case I would think so |
| 2025-03-30 05:20:08 +0200 | <EvanR> | a linked list of coordinates? no |
| 2025-03-30 05:20:20 +0200 | <haskellbridge> | <thirdofmay18081814goya> why not |
| 2025-03-30 05:20:31 +0200 | <EvanR> | you could even draw a line that way |
| 2025-03-30 05:20:33 +0200 | <EvanR> | couldn't |
| 2025-03-30 05:20:56 +0200 | <haskellbridge> | <thirdofmay18081814goya> well yeah: the ordering of the linked list specifies which lines exist |
| 2025-03-30 05:21:18 +0200 | <EvanR> | ok you can't draw a circle |
| 2025-03-30 05:21:20 +0200 | <haskellbridge> | <thirdofmay18081814goya> so if the list is "[(0,0), (1,1), (2,2)]", we have two lines |
| 2025-03-30 05:21:47 +0200 | <haskellbridge> | <thirdofmay18081814goya> EvanR: you can't draw a circle, but you can approximate a circle with abritrary precision (including to an extent indistinguishable to the human eye) |
| 2025-03-30 05:22:18 +0200 | Eoco | (~ian@128.101.131.218) (Quit: WeeChat 4.4.2) |
| 2025-03-30 05:22:34 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-03-30 05:22:53 +0200 | <geekosaur> | are (visualizations of) Mandelbröt sets geometric diagrams? |
| 2025-03-30 05:22:57 +0200 | <haskellbridge> | <thirdofmay18081814goya> with this idea, you can specify a circle as a function "approximate :: Nat -> CircleApproximation", where "approximate n" approximates the circle more closely than "approximate (n + 1)" |
| 2025-03-30 05:22:57 +0200 | <geekosaur> | 😈 |
| 2025-03-30 05:22:58 +0200 | <EvanR> | this is gratuitously low quality xD |
| 2025-03-30 05:23:28 +0200 | <haskellbridge> | <thirdofmay18081814goya> uh, the contrary, "approximate (n + 1)" has lower error than "approximate n" |
| 2025-03-30 05:23:31 +0200 | <EvanR> | Mandelbrot "set" is actually a Locus so yes |
| 2025-03-30 05:23:51 +0200 | <haskellbridge> | <thirdofmay18081814goya> then "circle = approximate" :D |
| 2025-03-30 05:24:05 +0200 | <EvanR> | a theory of approximations wasn't called for |
| 2025-03-30 05:24:35 +0200 | <EvanR> | actual circles have been accepted as "geometric" since forever |
| 2025-03-30 05:25:22 +0200 | Eoco | (~ian@128.101.131.218) Eoco |
| 2025-03-30 05:26:47 +0200 | <haskellbridge> | <thirdofmay18081814goya> i secretely will use "approximate (100!^100!)" and will tell you it's a circle and you won't be able to tell it's secretly a polygon, so you'll agree with me 😈 |
| 2025-03-30 05:26:48 +0200 | <EvanR> | that's a good one, the mandlebrot set seems to need an infinite number of steps, to keep adding lobes |
| 2025-03-30 05:27:14 +0200 | <EvanR> | (and then it would probably miss a lot in the end) |
| 2025-03-30 05:28:24 +0200 | <haskellbridge> | <thirdofmay18081814goya> actually, there is an "n :: Natural" such that "approximate" cannot designate a circle that is physically closer to any other approximation (due to the size of atoms, or alternatively your screen resolution) |
| 2025-03-30 05:28:31 +0200 | <haskellbridge> | <Bowuigi> Fractals in general do that AFAIK |
| 2025-03-30 05:28:41 +0200 | <EvanR> | ultrafinitist confirmed |
| 2025-03-30 05:29:28 +0200 | <EvanR> | straight line segments are really bad at approximating curves btw, at least use parabolic segments |
| 2025-03-30 05:31:04 +0200 | <haskellbridge> | <thirdofmay18081814goya> right, well the point where mathematical and cs-theoretical perfection coincides is to consider "approximate" itself as the circle, instead of "approximate n" for a given n |
| 2025-03-30 05:31:14 +0200 | Eoco | (~ian@128.101.131.218) (Quit: WeeChat 4.4.2) |
| 2025-03-30 05:31:18 +0200 | <haskellbridge> | <thirdofmay18081814goya> then you can do stuff by function composition |
| 2025-03-30 05:31:42 +0200 | Eoco | (~ian@128.101.131.218) Eoco |
| 2025-03-30 05:31:52 +0200 | <EvanR> | it would be better if you do the approximation at the end of the program than at the beginning |
| 2025-03-30 05:32:08 +0200 | <haskellbridge> | <thirdofmay18081814goya> yeah |
| 2025-03-30 05:32:51 +0200 | <EvanR> | (if necessary) |
| 2025-03-30 05:33:14 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-03-30 05:36:00 +0200 | infinity0 | (~infinity0@pwned.gg) (Ping timeout: 246 seconds) |
| 2025-03-30 05:37:18 +0200 | <EvanR> | instead of "human eye" test I wonder if you could instead specify the limit of precision by saying lines and shapes have a minimum "pen size" so if you keep trying to draw the mandlebrot set you'll just start getting the same blob over again |
| 2025-03-30 05:37:29 +0200 | <EvanR> | at which point you stop |
| 2025-03-30 05:37:34 +0200 | harveypwca | (~harveypwc@2601:246:d080:f6e0:27d6:8cc7:eca9:c46c) (Read error: Connection reset by peer) |
| 2025-03-30 05:38:18 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2025-03-30 05:39:06 +0200 | infinity0 | (~infinity0@pwned.gg) infinity0 |
| 2025-03-30 05:41:32 +0200 | harveypwca | (~harveypwc@2601:246:d080:f6e0:27d6:8cc7:eca9:c46c) |
| 2025-03-30 05:47:13 +0200 | <haskellbridge> | <thirdofmay18081814goya> speaking of which |
| 2025-03-30 05:47:22 +0200 | <haskellbridge> | <thirdofmay18081814goya> is there a standard wrt rendering 2D in haskell? |
| 2025-03-30 05:47:48 +0200 | <haskellbridge> | <thirdofmay18081814goya> or, how do people usually do 2D rendering in haskell |
| 2025-03-30 05:49:16 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-03-30 05:50:57 +0200 | <geekosaur> | gloss and relativrd |
| 2025-03-30 05:51:02 +0200 | <geekosaur> | *relatives |
| 2025-03-30 05:52:40 +0200 | <EvanR> | there's the diagrams library |
| 2025-03-30 05:53:02 +0200 | <EvanR> | there are bindings to SDL, glfw |
| 2025-03-30 05:53:09 +0200 | <EvanR> | ... and gtk ... |
| 2025-03-30 05:54:07 +0200 | <EvanR> | three penny gui was an early web-based thing |
| 2025-03-30 05:54:28 +0200 | <EvanR> | now there's ghcjs so you can use whatever is in the browser |
| 2025-03-30 05:54:43 +0200 | <haskellbridge> | <thirdofmay18081814goya> neat thanks for all the references! |
| 2025-03-30 05:55:08 +0200 | <haskellbridge> | <dmjio> thirdofmay18081814goya check out diagrams |
| 2025-03-30 05:55:41 +0200 | <haskellbridge> | <thirdofmay18081814goya> will do ty! |
| 2025-03-30 05:55:59 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-03-30 05:56:24 +0200 | <EvanR> | diagrams is great |
| 2025-03-30 06:01:33 +0200 | remexre | (~remexre@user/remexre) (Ping timeout: 268 seconds) |
| 2025-03-30 06:01:38 +0200 | nek0 | (~nek0@user/nek0) (Quit: The Lounge - https://thelounge.chat) |
| 2025-03-30 06:02:48 +0200 | Eoco | (~ian@128.101.131.218) (Ping timeout: 272 seconds) |
| 2025-03-30 06:03:28 +0200 | hgolden | (~hgolden@2603:8000:9d00:3ed1:6ff3:8389:b901:6363) (Remote host closed the connection) |
| 2025-03-30 06:04:30 +0200 | Eoco | (~ian@128.101.131.218) Eoco |
| 2025-03-30 06:07:18 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-03-30 06:07:30 +0200 | <haskellbridge> | <dmjio> Anything Brent Yorgey is great, especially the typeclassopdia |
| 2025-03-30 06:08:21 +0200 | hgolden | (~hgolden@2603:8000:9d00:3ed1:6ff3:8389:b901:6363) hgolden |
| 2025-03-30 06:12:03 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2025-03-30 06:12:04 +0200 | remexre | (~remexre@user/remexre) remexre |
| 2025-03-30 06:21:33 +0200 | talisman` | (~user@2601:644:937c:ed10::ae5) |
| 2025-03-30 06:21:57 +0200 | talismanick | (~user@2601:644:937c:ed10::ae5) (Remote host closed the connection) |
| 2025-03-30 06:21:57 +0200 | talisman` | (~user@2601:644:937c:ed10::ae5) (Read error: Connection reset by peer) |
| 2025-03-30 06:23:06 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-03-30 06:25:28 +0200 | tromp | (~textual@2001:1c00:3487:1b00:9865:6ec1:d353:2dc8) |
| 2025-03-30 06:26:02 +0200 | tromp | (~textual@2001:1c00:3487:1b00:9865:6ec1:d353:2dc8) (Client Quit) |
| 2025-03-30 06:28:33 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-03-30 06:33:48 +0200 | mulk | (~mulk@p5b112905.dip0.t-ipconnect.de) (Ping timeout: 244 seconds) |
| 2025-03-30 06:35:44 +0200 | mulk | (~mulk@pd95149c0.dip0.t-ipconnect.de) mulk |
| 2025-03-30 06:38:52 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-03-30 06:42:13 +0200 | jmcantrell | (~weechat@user/jmcantrell) (Quit: WeeChat 4.6.0) |
| 2025-03-30 06:43:40 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-03-30 06:50:34 +0200 | aman | (~aman@user/aman) aman |
| 2025-03-30 06:54:39 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-03-30 06:59:48 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
| 2025-03-30 07:10:26 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-03-30 07:11:25 +0200 | j1n37 | (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 2025-03-30 07:13:57 +0200 | harveypwca | (~harveypwc@2601:246:d080:f6e0:27d6:8cc7:eca9:c46c) (Quit: Leaving) |
| 2025-03-30 07:16:33 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-03-30 07:19:46 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-03-30 07:19:55 +0200 | j1n37 | (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 2025-03-30 07:25:04 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-03-30 07:33:15 +0200 | takuan | (~takuan@d8D86B601.access.telenet.be) |
| 2025-03-30 07:34:45 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 248 seconds) |
| 2025-03-30 07:35:28 +0200 | Garbanzo | (~Garbanzo@2602:304:6eac:dc10::2e) (Remote host closed the connection) |
| 2025-03-30 07:35:52 +0200 | Garbanzo | (~Garbanzo@2602:304:6eac:dc10::2e) |
| 2025-03-30 07:35:53 +0200 | weary-traveler | (~user@user/user363627) (Remote host closed the connection) |
| 2025-03-30 07:38:12 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-03-30 07:53:12 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 246 seconds) |
| 2025-03-30 07:54:04 +0200 | tavare | (~tavare@user/tavare) tavare |
| 2025-03-30 08:14:58 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-03-30 08:16:07 +0200 | berberman | (~berberman@user/berberman) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2025-03-30 08:16:35 +0200 | berberman | (~berberman@user/berberman) berberman |
| 2025-03-30 08:17:46 +0200 | <haskellbridge> | <thirdofmay18081814goya> what's a case where "Either" wasn't enough for your error handling needs? |
| 2025-03-30 08:23:57 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-03-30 08:24:53 +0200 | berberman | (~berberman@user/berberman) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2025-03-30 08:25:16 +0200 | berberman | (~berberman@user/berberman) berberman |
| 2025-03-30 08:26:09 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-03-30 08:31:24 +0200 | comonad | (~comonad@p200300d027488b00f8b6e4e070ffbc0b.dip0.t-ipconnect.de) (Ping timeout: 268 seconds) |
| 2025-03-30 08:31:38 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
| 2025-03-30 08:32:37 +0200 | comonad | (~comonad@p200300d027481500ef699452775b3984.dip0.t-ipconnect.de) |
| 2025-03-30 08:38:33 +0200 | zmt01 | (~zmt00@user/zmt00) (Remote host closed the connection) |
| 2025-03-30 08:38:57 +0200 | zmt01 | (~zmt00@user/zmt00) zmt00 |
| 2025-03-30 08:42:11 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-03-30 08:42:54 +0200 | vgtw_ | (~vgtw@user/vgtw) vgtw |
| 2025-03-30 08:43:07 +0200 | vgtw | (~vgtw@user/vgtw) (Ping timeout: 268 seconds) |
| 2025-03-30 08:46:12 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 272 seconds) |
| 2025-03-30 08:47:54 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-03-30 09:00:02 +0200 | caconym | (~caconym@user/caconym) (Quit: bye) |
| 2025-03-30 09:00:02 +0200 | tt12310978324354 | (~tt1231@2603:6010:8700:4a81:219f:50d3:618a:a6ee) (Quit: The Lounge - https://thelounge.chat) |
| 2025-03-30 09:00:56 +0200 | caconym | (~caconym@user/caconym) caconym |
| 2025-03-30 09:04:20 +0200 | tt12310978324354 | (~tt1231@2603:6010:8700:4a81:219f:50d3:618a:a6ee) tt1231 |
| 2025-03-30 09:05:11 +0200 | Garbanzo | (~Garbanzo@2602:304:6eac:dc10::2e) (Read error: Connection reset by peer) |
| 2025-03-30 09:05:43 +0200 | Garbanzo | (~Garbanzo@2602:304:6eac:dc10::2e) |
| 2025-03-30 09:06:52 +0200 | Garbanzo | (~Garbanzo@2602:304:6eac:dc10::2e) (Read error: Connection reset by peer) |
| 2025-03-30 09:07:09 +0200 | Garbanzo | (~Garbanzo@2602:304:6eac:dc10::2e) |
| 2025-03-30 09:08:05 +0200 | tromp | (~textual@2001:1c00:3487:1b00:9865:6ec1:d353:2dc8) |
| 2025-03-30 09:08:19 +0200 | hattckory | (~hattckory@70.27.118.207) (Ping timeout: 260 seconds) |
| 2025-03-30 09:14:47 +0200 | oneeyedalien | (~oneeyedal@user/oneeyedalien) oneeyedalien |
| 2025-03-30 09:15:49 +0200 | Lord_of_Life_ | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2025-03-30 09:16:17 +0200 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 2025-03-30 09:17:02 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 268 seconds) |
| 2025-03-30 09:17:15 +0200 | Lord_of_Life_ | Lord_of_Life |
| 2025-03-30 09:17:45 +0200 | oneeyedalien | (~oneeyedal@user/oneeyedalien) (Remote host closed the connection) |
| 2025-03-30 09:18:39 +0200 | cawfee | (root@2001:19f0:4400:79a1::babe) (Quit: WeeChat 4.5.1) |
| 2025-03-30 09:19:03 +0200 | cawfee | (root@2001:19f0:4400:79a1::babe) qjqqyy |
| 2025-03-30 09:43:27 +0200 | werneta | (~werneta@syn-071-083-160-242.res.spectrum.com) (Ping timeout: 246 seconds) |