Logs: liberachat/#haskell
| 2025-11-29 21:37:26 | <Guest56> | let Just (MyType var1 var2 -> MyType var1’ var3) = ta …. Made sure that ta is not a Nothing already |
| 2025-11-29 21:37:27 | <Guest56> | In if var1 == var1’ |
| 2025-11-29 21:37:27 | <Guest56> | then … |
| 2025-11-29 21:37:28 | <Guest56> | else |
| 2025-11-29 21:37:28 | <Guest56> | I want to be able to do Just (MyType var1 var2 -> MyType var1 var3) …. Is there an extension for this? The actual code has over 8 places in which var1 is used and it is not realistic to keep adding apostrophes and do 56 comparisons |
| 2025-11-29 21:37:31 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2025-11-29 21:43:34 | <Guest56> | anyone? |
| 2025-11-29 21:48:00 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-11-29 21:54:36 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-11-29 22:01:31 | × | euphores quits (~SASL_euph@user/euphores) (Ping timeout: 264 seconds) |
| 2025-11-29 22:01:42 | <pavonia> | What syntax is the arrow in "let Just (MyType var1 var2 -> MyType var1’ var3) = ta"? |
| 2025-11-29 22:03:40 | × | szkl quits (uid110435@id-110435.uxbridge.irccloud.com) (Quit: Connection closed for inactivity) |
| 2025-11-29 22:04:58 | <Guest56> | it's supposed to return a function type. I have added arrows in there for easy viewing. My type definitions for arrows are: Arrow MyType MyType |
| 2025-11-29 22:06:02 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-11-29 22:06:34 | <Guest56> | So the actual code is on the lines of: Just (Arrow (MyType var1 var2) (MyType var1’ var3)) = ta |
| 2025-11-29 22:08:30 | <Rembane> | Guest56: Do they always have to be the same type or is it okay if they are different types sometimes? |
| 2025-11-29 22:08:49 | <Guest56> | no, they have to be the same types |
| 2025-11-29 22:09:08 | <Guest56> | var1 and var2 are just Type renames for strings |
| 2025-11-29 22:09:30 | <Guest56> | I'm sorry, I cannot show the actual code but I can come up with an MRE as close as possible. |
| 2025-11-29 22:10:34 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds) |
| 2025-11-29 22:11:05 | <Rembane> | Guest56: No worries, then I think you could use newtypes instead of types to give the type checker something more to work with and use functional dependencies or maybe type families (which I'm not familiar with more than the name) to get the same types. |
| 2025-11-29 22:11:13 | <Rembane> | Guest56: What are you trying to model with your machinery? |
| 2025-11-29 22:11:22 | <Guest56> | It is an extension of System F |
| 2025-11-29 22:13:22 | <Rembane> | Nice, where you can find out if two arguments are the same type? |
| 2025-11-29 22:13:37 | × | L29Ah quits (~L29Ah@wikipedia/L29Ah) (Read error: Connection reset by peer) |
| 2025-11-29 22:13:46 | <Guest56> | uh, I'm writing an MRE. This should help. Gimme a couple minutes please :) |
| 2025-11-29 22:16:03 | <Rembane> | https://play.haskell.org/saved/8UUN33oD <- this is probably too simple, but I like thinking out loud |
| 2025-11-29 22:20:43 | <Guest56> | This is as close I can get to an MRE |
| 2025-11-29 22:20:47 | <Guest56> | Type = TSimple (Either Int Bool) | TArrow Type Type | (TVar String) | SpecialType Type Type Type |
| 2025-11-29 22:20:47 | <Guest56> | Exp = ESimple (Either Int Bool) | EArrow Type Type | (EVar String) | ESpecial Exp |
| 2025-11-29 22:20:48 | <Guest56> | typeCheck :: Exp -> Type |
| 2025-11-29 22:20:48 | <Guest56> | typeCheck (ESpecial e) = let te = inferType e |
| 2025-11-29 22:20:49 | <Guest56> | In if isJust te |
| 2025-11-29 22:20:49 | <Guest56> | then let Just (TArrow (SpecialType (TArrow (TVar t1) (TVar t2)) (TArrow (TVar t1) (TVar t2’)) (TArrow (TVar t1) (TVar t2’’))) (SpecialType (TVar t2) (TVar t2’) (TVar t2’’))) = te |
| 2025-11-29 22:20:50 | <Guest56> | in if t1 == t1’ && t1’ == t2’ |
| 2025-11-29 22:20:50 | <Guest56> | then SpecialType (TVar t2) (TVar t2’) (TVar t2’’) |
| 2025-11-29 22:20:51 | <Guest56> | else Nothing |
| 2025-11-29 22:20:51 | <Guest56> | else Nothing |
| 2025-11-29 22:21:09 | <Guest56> | whoops typo... t1' == t1'' not t2' |
| 2025-11-29 22:21:25 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-11-29 22:24:02 | <Guest56> | The actual code has like 8 `t1`s. |
| 2025-11-29 22:24:23 | <Rembane> | That's exciting and seems quite hard to read. |
| 2025-11-29 22:25:06 | <Guest56> | oh wait lol I can refer you to the actual paper. That is public domain lmao |
| 2025-11-29 22:26:00 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-11-29 22:26:12 | <Guest56> | https://www.cs.cornell.edu/people/fluet/research/rgn-monad/JFP06/jfp06.pdf |
| 2025-11-29 22:26:13 | <Guest56> | Go down to page 20. I'm trying to model the type checker for letRGN |
| 2025-11-29 22:29:18 | <Rembane> | That's some spicy notation! |
| 2025-11-29 22:29:34 | <Guest56> | yup lol |
| 2025-11-29 22:31:00 | → | jmcantrell joins (~weechat@user/jmcantrell) |
| 2025-11-29 22:31:00 | <Guest56> | I guess I can share a snippet of my code |
| 2025-11-29 22:32:37 | → | tcard_ joins (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) |
| 2025-11-29 22:32:47 | × | tcard quits (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) (Read error: Connection reset by peer) |
| 2025-11-29 22:34:46 | × | divlamir quits (~divlamir@user/divlamir) (Read error: Connection reset by peer) |
| 2025-11-29 22:34:48 | <Guest56> | Gimme a sec please it ain't easy writing down all those Arrows lol |
| 2025-11-29 22:34:49 | → | divlamir_ joins (~divlamir@user/divlamir) |
| 2025-11-29 22:35:40 | divlamir_ | is now known as divlamir |
| 2025-11-29 22:36:54 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-11-29 22:37:13 | × | jmcantrell quits (~weechat@user/jmcantrell) (Ping timeout: 264 seconds) |
| 2025-11-29 22:38:13 | <Guest56> | ok, there we go. This will not compile because all those `gr2`s need to be different and then checked for equality. |
| 2025-11-29 22:39:01 | <Guest56> | inferType d g (ELetRGN tr1 ta v) = |
| 2025-11-29 22:39:01 | <Guest56> | let tv = (inferType d g . valToExp) v |
| 2025-11-29 22:39:02 | <Guest56> | in if (S.member tr1 d) && (S.member ta d) && isJust tv |
| 2025-11-29 22:39:02 | <Guest56> | then let FForall gr2 (FArrow (FArrow (FArrow (RGN tr1 (FVar gr2)) (RGN (FVar gr2) (gr2))) (RGNHandle (FVar gr2))) (RGN (FVar gr2) ta)) = tv |
| 2025-11-29 22:39:03 | <Guest56> | in if gr2 == gr2' && gr2' == gr2'' && gr2'' == gr2''' && gr2''' == gr2'''' && gr2'''' == gr2''''' |
| 2025-11-29 22:39:03 | <Guest56> | then Just $ RGN tr1 ta |
| 2025-11-29 22:39:04 | <Guest56> | else Nothing |
| 2025-11-29 22:39:04 | <Guest56> | else Nothing |
| 2025-11-29 22:39:37 | <Guest56> | Rembane you there? |
| 2025-11-29 22:40:08 | <Rembane> | Guest56: Yup, lets see. |
| 2025-11-29 22:41:11 | × | tcard_ quits (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) (Remote host closed the connection) |
| 2025-11-29 22:41:15 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2025-11-29 22:41:28 | → | tcard_ joins (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) |
| 2025-11-29 22:42:21 | <Guest56> | I'm basically trying to replace the let expression as let will not let me repeat bindings. |
| 2025-11-29 22:42:44 | <Rembane> | Guest56: You can replace it with a case and pattern match on Just |
| 2025-11-29 22:43:12 | <Rembane> | Guest56: But I have a feeling there's either incredible inherent complexity in the problem or that there's an easier way to model this in Haskell. |
| 2025-11-29 22:43:14 | <Guest56> | oh? |
| 2025-11-29 22:43:36 | <Guest56> | hmm... how else should I model this? |
| 2025-11-29 22:45:05 | <Rembane> | Guest56: https://play.haskell.org/saved/2Ogh8nQy <- example for case |
| 2025-11-29 22:45:12 | <Rembane> | Guest56: No idea, I'm way too tired for that. :) |
| 2025-11-29 22:46:00 | × | tromp quits (~textual@2001:1c00:3487:1b00:5005:5ee4:6658:fef3) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-11-29 22:46:22 | <Guest56> | understandable |
| 2025-11-29 22:46:29 | <Guest56> | thanks for the case example though :) |
| 2025-11-29 22:48:48 | <__monty__> | Clint: Don't see how it deals with depending on different versions in different projects then. |
| 2025-11-29 22:49:33 | <Rembane> | Guest56: Another version, which uses guards on case which removes some of the nesting: https://play.haskell.org/saved/omzWcKUF |
| 2025-11-29 22:49:53 | <Rembane> | Guest56: No worries. Good luck! :) |
| 2025-11-29 22:52:17 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-11-29 22:52:52 | × | simplystuart quits (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 244 seconds) |
| 2025-11-29 22:53:35 | <Guest56> | Thank you so much! |
| 2025-11-29 22:54:58 | → | tromp joins (~textual@2001:1c00:3487:1b00:5005:5ee4:6658:fef3) |
| 2025-11-29 22:56:35 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2025-11-29 22:59:04 | → | simplystuart joins (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) |
| 2025-11-29 22:59:25 | → | aaronm04 joins (~user@user/aaronm04) |
| 2025-11-29 23:02:07 | → | ljdarj1 joins (~Thunderbi@user/ljdarj) |
| 2025-11-29 23:03:01 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 264 seconds) |
| 2025-11-29 23:03:01 | ljdarj1 | is now known as ljdarj |
| 2025-11-29 23:03:24 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 2025-11-29 23:04:56 | <aaronm04> | on OpenBSD 7.8, I cannot build splitmix-0.1.3.1 due to not finding the sys/random.h header. Is there a fix for this? |
| 2025-11-29 23:05:20 | <aaronm04> | the specific error location is cbits-unix/init.c:3:10 in case that helps |
| 2025-11-29 23:05:59 | × | tromp quits (~textual@2001:1c00:3487:1b00:5005:5ee4:6658:fef3) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-11-29 23:07:47 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
All times are in UTC.