Newest at the top
| 2025-03-27 05:13:20 +0100 | <EvanR> | ultrafinitism would forbid infinite and most of the finite values |
| 2025-03-27 05:12:51 +0100 | <haskellbridge> | <Bowuigi> Why do you need to constraint infinities? |
| 2025-03-27 05:12:37 +0100 | <haskellbridge> | <Bowuigi> Doesn't totality forbid infinitely large values (excluding codata, which can still be encoded, tho not evaluated on its entirety) via Church-Rosser? |
| 2025-03-27 05:11:55 +0100 | Square | (~Square@user/square) Square |
| 2025-03-27 05:11:14 +0100 | <EvanR> | for incredibly small values of infinity, such and such |
| 2025-03-27 05:11:01 +0100 | <haskellbridge> | <Bowuigi> A what |
| 2025-03-27 05:10:43 +0100 | <EvanR> | an ultrafinitist interpretation might get you lower than the lowest common denominator |
| 2025-03-27 05:10:25 +0100 | <haskellbridge> | <Bowuigi> Unless you want to play around with bottoms, which is ok I guess |
| 2025-03-27 05:10:07 +0100 | <haskellbridge> | <Bowuigi> EvanR it gets you the "lowest common denominator" of the members of all the semantics. On a lot of cases these are the most useful |
| 2025-03-27 05:09:10 +0100 | <haskellbridge> | <Bowuigi> But in this case you wanted to get the members of a fixpoint function so assuming totality would be dumb lol |
| 2025-03-27 05:09:03 +0100 | <EvanR> | assuming totality, that seems to call for a whole different semantics |
| 2025-03-27 05:08:46 +0100 | <monochrom> | Oh domains are difficult, it never "helps" to get them involved. But I was going for clarifying *what* to count. |
| 2025-03-27 05:08:24 +0100 | <haskellbridge> | <Bowuigi> Assuming totality and equating using funext/homotopies is an easy way to get most of the useful terms |
| 2025-03-27 05:07:23 +0100 | <EvanR> | so maybe domains didn't help clear up "how to count" as much as you hoped |
| 2025-03-27 05:06:57 +0100 | <haskellbridge> | <Bowuigi> (Assuming the usual 'bottom x = bottom') |
| 2025-03-27 05:06:25 +0100 | <haskellbridge> | <Bowuigi> They are equal under function extensionality |
| 2025-03-27 05:06:22 +0100 | <haskellbridge> | <Liamzee> ah |
| 2025-03-27 05:06:13 +0100 | <haskellbridge> | <Liamzee> also (\x -> bottom) can be evaluated without triggering bottom? |
| 2025-03-27 05:06:11 +0100 | <EvanR> | but you might be right there's no way to observe the difference |
| 2025-03-27 05:06:09 +0100 | <monochrom> | I know Haskell's seq can distinguish them. But I also know that the Haskell Report confesses that this is why seq deviates from denotational semantics. |
| 2025-03-27 05:05:14 +0100 | <EvanR> | one is more defined than the other, obviously |
| 2025-03-27 05:05:06 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-03-27 05:04:59 +0100 | <monochrom> | I have trouble distinguishing ⊥ from \x -> ⊥ |
| 2025-03-27 05:04:15 +0100 | <haskellbridge> | <Bowuigi> Yes |
| 2025-03-27 05:03:57 +0100 | <EvanR> | ⊥, \x -> x, \x -> ⊥, \x -> () |
| 2025-03-27 05:03:56 +0100 | <haskellbridge> | <Bowuigi> Backslashes* |
| 2025-03-27 05:03:37 +0100 | <haskellbridge> | <Bowuigi> Matrix might have eaten some parens |
| 2025-03-27 05:03:22 +0100 | <haskellbridge> | <Bowuigi> Sorry, \x -> bottom and \() -> bottom |
| 2025-03-27 05:02:50 +0100 | <haskellbridge> | <Bowuigi> \x -> bottom and _ -> bottom are the same thing, () -> bottom is \x -> case x of () -> bottom which already returns bottom on every case |
| 2025-03-27 05:02:13 +0100 | <monochrom> | Oh you can always proofread and edit before pressing enter. |
| 2025-03-27 05:01:46 +0100 | <haskellbridge> | <Liamzee> i wish i could delete my imprecise blather |
| 2025-03-27 05:01:38 +0100 | <EvanR> | at the very least, use a universe |
| 2025-03-27 05:01:17 +0100 | <EvanR> | "the cardinality of all types" wwwwwwwwhwhhhhhaaaaaaaat |
| 2025-03-27 05:01:00 +0100 | <haskellbridge> | <Liamzee> i mean if you restrict a, instead of newtyping, it's equal to the cardinality of all types |
| 2025-03-27 05:00:57 +0100 | <haskellbridge> | <Bowuigi> Yeah |
| 2025-03-27 05:00:54 +0100 | <haskellbridge> | <Bowuigi> \x -> () |
| 2025-03-27 05:00:43 +0100 | <EvanR> | \x -> () |
| 2025-03-27 05:00:35 +0100 | <EvanR> | ? |
| 2025-03-27 05:00:33 +0100 | <EvanR> | \() -> ⊥ |
| 2025-03-27 05:00:05 +0100 | <EvanR> | ⊥, \x -> x, \x -> ⊥, |
| 2025-03-27 05:00:01 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-03-27 04:59:16 +0100 | <EvanR> | for () -> () you'd have |
| 2025-03-27 04:58:53 +0100 | <EvanR> | if you use domains, for Nat you'd have ⊥, Z, S ⊥, S Z, S (S ⊥), S (S Z), ... |
| 2025-03-27 04:56:53 +0100 | JuanDaugherty | (~juan@user/JuanDaugherty) JuanDaugherty |
| 2025-03-27 04:56:44 +0100 | <haskellbridge> | <Liamzee> so in that case, the only inhabitant is a value that produces bottom, which i guess is 1 |
| 2025-03-27 04:56:22 +0100 | <haskellbridge> | <Liamzee> sorry, my mistake for not being specific |
| 2025-03-27 04:56:10 +0100 | <EvanR> | newtype Mu a = Mu (Mu a -> a) |
| 2025-03-27 04:54:01 +0100 | <EvanR> | where exactly, since I asked what the type needed to be and you said "function" |
| 2025-03-27 04:53:46 +0100 | <haskellbridge> | <Liamzee> yes, but how would you manufacture a non-bottom value of type a? |
| 2025-03-27 04:53:31 +0100 | <haskellbridge> | <Liamzee> or rather the typechecker |