Newest at the top
| 2025-01-18 00:03:19 +0100 | <haskellbridge> | <thirdofmay18081814goya> well if a theory is a set of axioms and derivable sentences, then we should admit such a language (the one having the judgment 'x is a value of type Real Number') |
| 2025-01-18 00:03:02 +0100 | <EvanR> | usually you need a language for that |
| 2025-01-18 00:02:56 +0100 | <EvanR> | as far as real numbers go it's a pretty nutty way to specify one xD |
| 2025-01-18 00:02:47 +0100 | <monochrom> | We know of at least two theories (aka models) of programming, and they disagree on countability as well as other things. The moral is that you choose a theory to suit a purpose, not for Platonic "absolute" "truth". |
| 2025-01-18 00:02:29 +0100 | paul_j | (~user@8.190.187.81.in-addr.arpa) (Quit: Asta la vista) |
| 2025-01-18 00:02:23 +0100 | <EvanR> | jumping to another level of abstraction, beyond the syntax |
| 2025-01-18 00:02:04 +0100 | <EvanR> | that's mixing concepts |
| 2025-01-18 00:01:38 +0100 | <haskellbridge> | <thirdofmay18081814goya> right, e.g. a language with the judgment 'x is a value of type Real Number' does not have countably many statements I think |
| 2025-01-18 00:01:18 +0100 | simplystuart | (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 244 seconds) |
| 2025-01-18 00:00:52 +0100 | <EvanR> | haskell being an example of one |
| 2025-01-18 00:00:45 +0100 | <monochrom> | "I thank GHC for suggesting this newtype." |
| 2025-01-18 00:00:41 +0100 | <EvanR> | formal languages come with grammar rules which limit you to a countable number of sentences |
| 2025-01-18 00:00:19 +0100 | <monochrom> | And on second thought, I am not even sure I can take credit. My purpose was to make a newtype to allow the like of (\x -> x x), and the error message literally inspires that definition! |
| 2025-01-18 00:00:01 +0100 | <EvanR> | countable and constructible is certainly not the same thing |
| 2025-01-17 23:59:57 +0100 | <haskellbridge> | <thirdofmay18081814goya> I am not convinced there are countably many statements in any mathematical theory |
| 2025-01-17 23:59:36 +0100 | <EvanR> | which doesn't stop people believing in uncountability |
| 2025-01-17 23:59:34 +0100 | <haskellbridge> | <thirdofmay18081814goya> for the sake of specificity I'll say countable but I think constructible may be used rigorously interchangeably |
| 2025-01-17 23:59:22 +0100 | <EvanR> | there are countably many haskell programs, and countably many statements in any mathematical theory |
| 2025-01-17 23:59:12 +0100 | <monochrom> | c_wraith: My mind breaks with Hyper. I have only thought up and used newtype D a = Ctor (D a -> a). |
| 2025-01-17 23:59:00 +0100 | <EvanR> | constructible or countable? |
| 2025-01-17 23:58:40 +0100 | <haskellbridge> | <thirdofmay18081814goya> a countable universe |
| 2025-01-17 23:58:27 +0100 | <haskellbridge> | <thirdofmay18081814goya> EvanR: oh ok well, the statement is that terms/values of a polymorphic function type are indexable by the indexability of a constructible universe |
| 2025-01-17 23:58:24 +0100 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 2025-01-17 23:57:03 +0100 | <c_wraith> | Also, there are only countably many Haskell values for practical reasons like programs being countable and the total amount of input a program can receive being countable. |
| 2025-01-17 23:56:20 +0100 | pavonia | (~user@user/siracusa) siracusa |
| 2025-01-17 23:54:24 +0100 | <EvanR> | when you said "this one" there was nothing posted before you then said "this is not necessarily the case" maybe the bridge lost it |
| 2025-01-17 23:54:14 +0100 | <c_wraith> | It's secretly useful! |
| 2025-01-17 23:54:09 +0100 | <c_wraith> | have fun with that one. |
| 2025-01-17 23:54:03 +0100 | <c_wraith> | newtype Hyper a b = H (Hyper b a -> b) |
| 2025-01-17 23:53:43 +0100 | <EvanR> | how do you traverse a function value with or without finite time |
| 2025-01-17 23:53:34 +0100 | <haskellbridge> | <thirdofmay18081814goya> this is not necessarily the case for e.g. values of coinductive types |
| 2025-01-17 23:53:33 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 2025-01-17 23:53:28 +0100 | tnt2 | tnt1 |
| 2025-01-17 23:53:28 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 272 seconds) |
| 2025-01-17 23:53:28 +0100 | <EvanR> | "traversability of a value" is a bit weird |
| 2025-01-17 23:53:20 +0100 | tnt2 | (~Thunderbi@user/tnt1) tnt1 |
| 2025-01-17 23:53:16 +0100 | <haskellbridge> | <thirdofmay18081814goya> this one |
| 2025-01-17 23:52:50 +0100 | <haskellbridge> | <thirdofmay18081814goya> so there might be infinitely possible values, but as long as any given value is traversable in finite time, it is a datatype |
| 2025-01-17 23:52:49 +0100 | <EvanR> | what statement |
| 2025-01-17 23:52:30 +0100 | <haskellbridge> | <thirdofmay18081814goya> hm right but the statement specifically targets types whose terms are finitely traversable |
| 2025-01-17 23:51:50 +0100 | <EvanR> | infinite data might have non-countable possible values, for some value of possible |
| 2025-01-17 23:51:25 +0100 | simplystuart | (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) |
| 2025-01-17 23:51:13 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 245 seconds) |
| 2025-01-17 23:50:46 +0100 | <EvanR> | limiting yourself to finite data i haskell is a bit limiting goya |
| 2025-01-17 23:47:32 +0100 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-01-17 23:46:35 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-17 23:44:18 +0100 | symdrome | (~user@2804:1e78:2201:58b0::416) symdrome |
| 2025-01-17 23:35:46 +0100 | j1n37 | (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 2025-01-17 23:35:40 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2025-01-17 23:31:13 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |