2025/03/27

Newest at the top

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 +0100merijn(~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 +0100merijn(~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 +0100JuanDaugherty(~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
2025-03-27 04:53:30 +0100 <EvanR> you could have used a non-bottom value in the body of your function earlier
2025-03-27 04:52:57 +0100 <EvanR> Mu a is a type and bottom is a value... so Mu a -> bottom is causing the computer to self destruct now
2025-03-27 04:52:14 +0100 <haskellbridge> <Liamzee> but for all intents and purposes, i guess, (Mu a -> a) given parametricity has either 0 or 1 inhabitants, because it's always (Mu a -> bottom)
2025-03-27 04:51:55 +0100 <EvanR> id . id is different from id as terms, but are equal by function extensionality
2025-03-27 04:51:08 +0100 <haskellbridge> <Liamzee> it feels like pretending id.id is distinct from id and then claiming that a -> a has multiple inhabitants
2025-03-27 04:50:28 +0100 <EvanR> kind of like if you need a Nat, you can always say Z
2025-03-27 04:49:11 +0100 <EvanR> Liamzee, if in someplace you need something of function type, and you don't have any other options, you can always say "lambda such and such"
2025-03-27 04:49:08 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds)
2025-03-27 04:48:45 +0100 <monochrom> Oh, parametricity always collapses the space. But that's a disgression.