Newest at the top
2024-10-06 15:24:36 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
2024-10-06 15:23:51 +0200 | <ncf> | you should probably read the references at https://ncatlab.org/nlab/show/W-type#CategoricalSemanticsOfWTypesReferences |
2024-10-06 15:23:44 +0200 | <ncf> | it is how they're defined. whether what you get is a "well-founded" object or not probably depends on the category and what you mean by that |
2024-10-06 15:21:25 +0200 | <haskellbridge> | <thirdofmay18081814goya> ncf: is this true over Cpo? |
2024-10-06 15:20:44 +0200 | <ncf> | W-types are initial algebras for polynomial endofunctors |
2024-10-06 15:20:14 +0200 | <haskellbridge> | <Bowuigi> You can also get sized types using Nat recursion over the type level, but unless you use singletons you can't iterate on that type |
2024-10-06 15:19:27 +0200 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
2024-10-06 15:19:10 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Remote host closed the connection) |
2024-10-06 15:18:42 +0200 | <haskellbridge> | <Bowuigi> Termination and a size |
2024-10-06 15:17:13 +0200 | <haskellbridge> | <thirdofmay18081814goya> e.g. what sort of constraints do we need on the domain to guarantee a functor provides a w-type |
2024-10-06 15:16:45 +0200 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
2024-10-06 15:16:27 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Remote host closed the connection) |
2024-10-06 15:16:24 +0200 | <haskellbridge> | <Bowuigi> They are mostly present in dependent stuff so I don't know how useful they are in a practical sense |
2024-10-06 15:16:15 +0200 | <haskellbridge> | <thirdofmay18081814goya> Bowuigi: yeah those are what i'm thinking about |
2024-10-06 15:15:28 +0200 | <haskellbridge> | <Bowuigi> thirdofmay18081814goya you might want to look at well-founded trees, AKA W types |
2024-10-06 15:14:00 +0200 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
2024-10-06 15:13:41 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
2024-10-06 14:58:39 +0200 | <haskellbridge> | <thirdofmay18081814goya> ncf: types i'm interested in are well-founded ones |
2024-10-06 14:56:07 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
2024-10-06 14:50:30 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
2024-10-06 14:48:15 +0200 | sawilagar | (~sawilagar@user/sawilagar) sawilagar |
2024-10-06 14:47:50 +0200 | sawilagar | (~sawilagar@user/sawilagar) (Remote host closed the connection) |
2024-10-06 14:47:42 +0200 | Smiles | (uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
2024-10-06 14:47:10 +0200 | alp_ | (~alp@2001:861:e3d6:8f80:9437:9b0:9ccc:15a4) |
2024-10-06 14:45:54 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
2024-10-06 14:38:50 +0200 | mantraofpie | (~mantraofp@user/mantraofpie) mantraofpie |
2024-10-06 14:35:00 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds) |
2024-10-06 14:31:07 +0200 | <tomsmeding> | but with the downside that an unsuspecting user who forgets the type application will get ambiguous types |
2024-10-06 14:30:51 +0200 | <tomsmeding> | I mean, something that doesn't require 9.10 is -XAllowAmbiguousTypes and require a type application |
2024-10-06 14:29:52 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
2024-10-06 14:29:41 +0200 | Digit | (~user@user/digit) (Ping timeout: 248 seconds) |
2024-10-06 14:29:36 +0200 | Digitteknohippie | (~user@user/digit) Digit |
2024-10-06 14:27:38 +0200 | <haskellbridge> | <eldritchcookie> yes its a hack but hopefully it is forward compatible what we wil do |
2024-10-06 14:24:18 +0200 | <int-e> | oh *that* was the question |
2024-10-06 14:23:27 +0200 | <tomsmeding> | admittedly it's a bit of a hack |
2024-10-06 14:23:12 +0200 | <tomsmeding> | eldritchcookie: https://play.haskell.org/saved/6TcPRARS |
2024-10-06 14:22:13 +0200 | <int-e> | heh, heisenbridge? |
2024-10-06 14:21:27 +0200 | <haskellbridge> | ... long message truncated: https://kf8nh.com/_heisenbridge/media/kf8nh.com/PkaCnRCyIJXsiIbMXlrywuss/bOMDyOoAcr8 (22 lines) |
2024-10-06 14:21:27 +0200 | <haskellbridge> | <eldritchcookie> src/Qon/Bits.hs:25:3: error: [GHC-39999] |
2024-10-06 14:21:20 +0200 | <tomsmeding> | hm, lemme try |
2024-10-06 14:21:10 +0200 | <tomsmeding> | I see |
2024-10-06 14:20:53 +0200 | <haskellbridge> | <eldritchcookie> yes but naively trying this on a class method doesn't work |
2024-10-06 14:20:18 +0200 | <tomsmeding> | ghc >= 9.10 though |
2024-10-06 14:20:02 +0200 | <tomsmeding> | eldritchcookie ^ |
2024-10-06 14:19:57 +0200 | <yahb2> | f Bool :: Bool -> Bool |
2024-10-06 14:19:56 +0200 | <tomsmeding> | % :t f Bool |
2024-10-06 14:19:54 +0200 | <yahb2> | f Int :: Int -> Int |
2024-10-06 14:19:54 +0200 | <tomsmeding> | % :t f Int |
2024-10-06 14:19:51 +0200 | <yahb2> | <no output> |
2024-10-06 14:19:51 +0200 | <tomsmeding> | % f :: forall a -> a -> a ; f t x = x |