IRCBrowseLink

2025/03/30

2025-03-30 00:08:45 +0100rekahsoft(~rekahsoft@bras-base-orllon1103w-grc-19-74-12-85-11.dsl.bell.ca) (Ping timeout: 276 seconds)
2025-03-30 00:15:19 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
2025-03-30 00:16:31 +0100connrs_(~connrs@conners.plus.com) (Remote host closed the connection)
2025-03-30 00:16:39 +0100connrs_(~connrs@conners.plus.com)
2025-03-30 00:17:05 +0100connrs(~connrs@user/connrs) (Quit: ZNC 1.9.1 - https://znc.in)
2025-03-30 00:17:05 +0100connrs_connrs
2025-03-30 00:17:11 +0100connrs(~connrs@conners.plus.com) (Remote host closed the connection)
2025-03-30 00:17:19 +0100connrs(~connrs@user/connrs) connrs
2025-03-30 00:26:15 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-30 00:28:33 +0100connrs(~connrs@user/connrs) (Remote host closed the connection)
2025-03-30 00:28:41 +0100connrs(~connrs@user/connrs) connrs
2025-03-30 00:31:01 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds)
2025-03-30 00:35:12 +0100ljdarj1(~Thunderbi@user/ljdarj) ljdarj
2025-03-30 00:35:33 +0100peterbecich1(~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich
2025-03-30 00:37:54 +0100ljdarj(~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds)
2025-03-30 00:37:54 +0100ljdarj1ljdarj
2025-03-30 00:38:47 +0100peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 244 seconds)
2025-03-30 00:39:06 +0100peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich
2025-03-30 00:42:04 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-30 00:42:24 +0100peterbecich1(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 244 seconds)
2025-03-30 00:50:40 +0100Unicorn_Princess(~Unicorn_P@user/Unicorn-Princess/x-3540542) Unicorn_Princess
2025-03-30 00:54:45 +0100peterbecich1(~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich
2025-03-30 00:56:39 +0100peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 244 seconds)
2025-03-30 00:57:42 +0100peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich
2025-03-30 00:57:46 +0100peterbecich1(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Client Quit)
2025-03-30 01:02:04 +0100peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds)
2025-03-30 01:04:24 +0100otto_s(~user@p4ff27624.dip0.t-ipconnect.de) (Ping timeout: 260 seconds)
2025-03-30 01:06:02 +0100peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich
2025-03-30 01:06:05 +0100otto_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 +0100hattckory(~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 +0100causal(~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 +0100tromp(~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 +0100hattckory(~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 +0100peterbecich(~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 +0100hattckory(~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) (Ping timeout: 276 seconds)
2025-03-30 01:43:00 +0100ChaiTRex(~ChaiTRex@user/chaitrex) (Remote host closed the connection)
2025-03-30 01:43:47 +0100JuanDaugherty(~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 +0100ChaiTRex(~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 +0100merijn(~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 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-30 03:00:49 +0200causal(~eric@50.35.84.231) (Quit: WeeChat 4.5.1)
2025-03-30 03:01:37 +0200sprotte24_(~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 +0200ChaiTRex(~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 +0200peterbecich(~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 +0200hattckory(~hattckory@70.27.118.207)
2025-03-30 03:18:01 +0200ChaiTRex(~ChaiTRex@user/chaitrex) ChaiTRex
2025-03-30 03:21:35 +0200harveypwca(~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 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 246 seconds)
2025-03-30 03:32:58 +0200ljdarj(~Thunderbi@user/ljdarj) (Ping timeout: 244 seconds)
2025-03-30 03:38:24 +0200toby-bro(~toby-bro@user/toby-bro) (Ping timeout: 272 seconds)
2025-03-30 03:46:27 +0200roconnor(~quassel@rocq/roconnor) (Ping timeout: 246 seconds)
2025-03-30 03:47:08 +0200roconnor(~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 +0200Tuplanolla(~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 +0200ChaiTRex(~ChaiTRex@user/chaitrex) (Quit: ChaiTRex)
2025-03-30 03:51:53 +0200tremon(~tremon@83.80.159.219) (Quit: getting boxed in)
2025-03-30 03:52:58 +0200acidjnk(~acidjnk@p200300d6e71c4f5684d81f92e812b9d0.dip0.t-ipconnect.de) (Ping timeout: 272 seconds)
2025-03-30 03:56:36 +0200L29Ah(~L29Ah@wikipedia/L29Ah) (Read error: Connection timed out)
2025-03-30 03:59:51 +0200ChaiTRex(~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 +0200op_4(~tslil@user/op-4/x-9116473) (Remote host closed the connection)
2025-03-30 04:05:15 +0200roconnor(~quassel@rocq/roconnor) (Ping timeout: 252 seconds)
2025-03-30 04:05:35 +0200op_4(~tslil@user/op-4/x-9116473) op_4
2025-03-30 04:05:47 +0200roconnor(~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 +0200JuanDaugherty(~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 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds)
2025-03-30 04:27:48 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-30 04:28:43 +0200euphores(~SASL_euph@user/euphores) (Ping timeout: 245 seconds)