Newest at the top
| 2025-01-17 22:26:56 +0100 | <haskellbridge> | <thirdofmay18081814goya> just to be clear: the statement is about datatypes, understood as type whose terms are turing-machine processable. it's not true of all types |
| 2025-01-17 22:25:32 +0100 | <tomsmeding> | https://hackage.haskell.org/package/unordered-containers-0.2.20/docs/Data-HashMap-Strict.html#t:Ha… |
| 2025-01-17 22:25:21 +0100 | <tomsmeding> | referring specifically to toList being different |
| 2025-01-17 22:25:03 +0100 | <tomsmeding> | energizer: the unordered-containers library has the following note in its docs: "Note that, in the presence of hash collisions, equal HashMaps may behave differently, i.e. extensionality may be violated:" |
| 2025-01-17 22:24:29 +0100 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-01-17 22:24:14 +0100 | <energizer> | if two HashSets are equal, do their toList values necessarily produce lists in the same order? how does that work? |
| 2025-01-17 22:23:00 +0100 | simplystuart | (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 246 seconds) |
| 2025-01-17 22:21:29 +0100 | <haskellbridge> | <thirdofmay18081814goya> so any polymorphic function is indexable by its countable universe (if we're talking datatypes, not types in general) |
| 2025-01-17 22:21:23 +0100 | j1n37 | (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 2025-01-17 22:21:10 +0100 | <haskellbridge> | <thirdofmay18081814goya> the universe is countable by virtue of limited machine memory |
| 2025-01-17 22:21:05 +0100 | <geekosaur> | (well, strictly speaking you could Gödelize, but that leads to out of memory conditions) |
| 2025-01-17 22:20:31 +0100 | <geekosaur> | thirdofmay, no they don't. what's the injection for a polymorphic function? |
| 2025-01-17 22:20:06 +0100 | <geekosaur> | HashSet in unordered-containers, but that replaces Ord with Hashable |
| 2025-01-17 22:19:20 +0100 | <haskellbridge> | <thirdofmay18081814goya> all datatypes have an injection into the naturals, don't think so |
| 2025-01-17 22:18:57 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2025-01-17 22:18:55 +0100 | <energizer> | (eg by using hashing instead of ordering) |
| 2025-01-17 22:18:52 +0100 | simplystuart | (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) |
| 2025-01-17 22:18:44 +0100 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-01-17 22:18:11 +0100 | <energizer> | is there a set type that doesn't have the Ord requirement? |
| 2025-01-17 22:17:30 +0100 | <geekosaur> | because a Set is a tree stored in ascending key order |
| 2025-01-17 22:17:12 +0100 | <geekosaur> | Ord is there because the elements must be Ord (comparable) to make a Set of them |
| 2025-01-17 22:16:20 +0100 | <haskellbridge> | <thirdofmay18081814goya> edited and unedited it back heheh |
| 2025-01-17 22:16:13 +0100 | <energizer> | https://hackage.haskell.org/package/containers-0.7/docs/src/Data.Set.Internal.html#toList what does this Ord stuff mean? can i only toList a Set if its elements are Ord? |
| 2025-01-17 22:15:39 +0100 | <geekosaur> | also I see an edit of a large message back there, please be careful |
| 2025-01-17 22:15:35 +0100 | <haskellbridge> | <thirdofmay18081814goya> ah neato |
| 2025-01-17 22:15:24 +0100 | <geekosaur> | irc gets a media link |
| 2025-01-17 22:13:37 +0100 | j1n37 | (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 2025-01-17 22:12:08 +0100 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-01-17 22:11:00 +0100 | <haskellbridge> | <thirdofmay18081814goya> where "B" is a binary type-level operator |
| 2025-01-17 22:10:21 +0100 | <haskellbridge> | ... long message truncated: https://kf8nh.com/_heisenbridge/media/kf8nh.com/bfslQLLKLEWmGEEOBGPzXZoN/W2_SWeb9p5U (4 lines) |
| 2025-01-17 22:10:21 +0100 | <haskellbridge> | <thirdofmay18081814goya> uh not sure if irc gets images, here: |
| 2025-01-17 22:10:08 +0100 | ephilalethes | (~noumenon@182.0.203.121) noumenon |
| 2025-01-17 22:10:08 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-17 22:09:56 +0100 | <haskellbridge> | <thirdofmay18081814goya> https://kf8nh.com/_heisenbridge/media/matrix.org/kBqPWoKqZUTyiUEsoYvUgTHC/_qzQbc_U3jo/image.png |
| 2025-01-17 22:09:54 +0100 | <haskellbridge> | <thirdofmay18081814goya> ultimately am trying to get an analog to |
| 2025-01-17 22:09:23 +0100 | <haskellbridge> | <thirdofmay18081814goya> anyone have suggestions on how we could encode such a type family? |
| 2025-01-17 22:08:55 +0100 | <haskellbridge> | <thirdofmay18081814goya> hm yes, "forall (a :: Type) (b :: Type). a -> b" does not itself have type "Type" |
| 2025-01-17 22:08:25 +0100 | j1n37 | (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 2025-01-17 22:08:05 +0100 | wootehfoot | (~wootehfoo@user/wootehfoot) (Ping timeout: 248 seconds) |
| 2025-01-17 22:07:51 +0100 | <haskellbridge> | <thirdofmay18081814goya> hm wait, is it? |
| 2025-01-17 22:06:00 +0100 | <haskellbridge> | ... long message truncated: https://kf8nh.com/_heisenbridge/media/kf8nh.com/neYpbolADunqHNZVAEVEzVmd/tkzoiq-k2Wo (3 lines) |
| 2025-01-17 22:06:00 +0100 | <haskellbridge> | <thirdofmay18081814goya> is it possible to write something like this in haskell? |
| 2025-01-17 22:05:55 +0100 | <haskellbridge> | <thirdofmay18081814goya> which makes sense because that's one universe higher than "Type" |
| 2025-01-17 22:05:49 +0100 | ss4 | (~wootehfoo@user/wootehfoot) wootehfoot |
| 2025-01-17 22:05:36 +0100 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-01-17 22:05:33 +0100 | <haskellbridge> | <thirdofmay18081814goya> I get illegal polymorphic type |
| 2025-01-17 22:05:14 +0100 | <haskellbridge> | <thirdofmay18081814goya> +:: Type |
| 2025-01-17 22:04:56 +0100 | <haskellbridge> | ... long message truncated: https://kf8nh.com/_heisenbridge/media/kf8nh.com/nrHaYMVNJVTbkERRMZVHrUfZ/MuJn5bDBuW0 (3 lines) |
| 2025-01-17 22:04:56 +0100 | <haskellbridge> | <thirdofmay18081814goya> is it possible to write something like this in haskell? |
| 2025-01-17 22:04:46 +0100 | <haskellbridge> | <thirdofmay18081814goya> hm |
