Newest at the top
| 2025-11-29 23:39:04 +0100 | <Guest56> | else Nothing |
| 2025-11-29 23:39:04 +0100 | <Guest56> | else Nothing |
| 2025-11-29 23:39:03 +0100 | <Guest56> | then Just $ RGN tr1 ta |
| 2025-11-29 23:39:03 +0100 | <Guest56> | in if gr2 == gr2' && gr2' == gr2'' && gr2'' == gr2''' && gr2''' == gr2'''' && gr2'''' == gr2''''' |
| 2025-11-29 23:39:02 +0100 | <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 23:39:02 +0100 | <Guest56> | in if (S.member tr1 d) && (S.member ta d) && isJust tv |
| 2025-11-29 23:39:01 +0100 | <Guest56> | let tv = (inferType d g . valToExp) v |
| 2025-11-29 23:39:01 +0100 | <Guest56> | inferType d g (ELetRGN tr1 ta v) = |
| 2025-11-29 23:38:13 +0100 | <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 23:37:13 +0100 | jmcantrell | (~weechat@user/jmcantrell) (Ping timeout: 264 seconds) |
| 2025-11-29 23:36:54 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-11-29 23:35:40 +0100 | divlamir_ | divlamir |
| 2025-11-29 23:34:49 +0100 | divlamir_ | (~divlamir@user/divlamir) divlamir |
| 2025-11-29 23:34:48 +0100 | <Guest56> | Gimme a sec please it ain't easy writing down all those Arrows lol |
| 2025-11-29 23:34:46 +0100 | divlamir | (~divlamir@user/divlamir) (Read error: Connection reset by peer) |
| 2025-11-29 23:32:47 +0100 | tcard | (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) (Read error: Connection reset by peer) |
| 2025-11-29 23:32:37 +0100 | tcard_ | (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) |
| 2025-11-29 23:31:00 +0100 | <Guest56> | I guess I can share a snippet of my code |
| 2025-11-29 23:31:00 +0100 | jmcantrell | (~weechat@user/jmcantrell) jmcantrell |
| 2025-11-29 23:29:34 +0100 | <Guest56> | yup lol |
| 2025-11-29 23:29:18 +0100 | <Rembane> | That's some spicy notation! |
| 2025-11-29 23:26:13 +0100 | <Guest56> | Go down to page 20. I'm trying to model the type checker for letRGN |
| 2025-11-29 23:26:12 +0100 | <Guest56> | https://www.cs.cornell.edu/people/fluet/research/rgn-monad/JFP06/jfp06.pdf |
| 2025-11-29 23:26:00 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-11-29 23:25:06 +0100 | <Guest56> | oh wait lol I can refer you to the actual paper. That is public domain lmao |
| 2025-11-29 23:24:23 +0100 | <Rembane> | That's exciting and seems quite hard to read. |
| 2025-11-29 23:24:02 +0100 | <Guest56> | The actual code has like 8 `t1`s. |
| 2025-11-29 23:21:25 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-11-29 23:21:09 +0100 | <Guest56> | whoops typo... t1' == t1'' not t2' |
| 2025-11-29 23:20:51 +0100 | <Guest56> | else Nothing |
| 2025-11-29 23:20:51 +0100 | <Guest56> | else Nothing |
| 2025-11-29 23:20:50 +0100 | <Guest56> | then SpecialType (TVar t2) (TVar t2’) (TVar t2’’) |
| 2025-11-29 23:20:50 +0100 | <Guest56> | in if t1 == t1’ && t1’ == t2’ |
| 2025-11-29 23:20:49 +0100 | <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 23:20:49 +0100 | <Guest56> | In if isJust te |
| 2025-11-29 23:20:48 +0100 | <Guest56> | typeCheck (ESpecial e) = let te = inferType e |
| 2025-11-29 23:20:48 +0100 | <Guest56> | typeCheck :: Exp -> Type |
| 2025-11-29 23:20:47 +0100 | <Guest56> | Exp = ESimple (Either Int Bool) | EArrow Type Type | (EVar String) | ESpecial Exp |
| 2025-11-29 23:20:47 +0100 | <Guest56> | Type = TSimple (Either Int Bool) | TArrow Type Type | (TVar String) | SpecialType Type Type Type |
| 2025-11-29 23:20:43 +0100 | <Guest56> | This is as close I can get to an MRE |
| 2025-11-29 23:16:03 +0100 | <Rembane> | https://play.haskell.org/saved/8UUN33oD <- this is probably too simple, but I like thinking out loud |
| 2025-11-29 23:13:46 +0100 | <Guest56> | uh, I'm writing an MRE. This should help. Gimme a couple minutes please :) |
| 2025-11-29 23:13:37 +0100 | L29Ah | (~L29Ah@wikipedia/L29Ah) (Read error: Connection reset by peer) |
| 2025-11-29 23:13:22 +0100 | <Rembane> | Nice, where you can find out if two arguments are the same type? |
| 2025-11-29 23:11:22 +0100 | <Guest56> | It is an extension of System F |
| 2025-11-29 23:11:13 +0100 | <Rembane> | Guest56: What are you trying to model with your machinery? |
| 2025-11-29 23:11:05 +0100 | <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 23:10:34 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds) |
| 2025-11-29 23:09:30 +0100 | <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 23:09:08 +0100 | <Guest56> | var1 and var2 are just Type renames for strings |