Newest at the top
| 2025-11-29 23:42:21 +0100 | <Guest56> | I'm basically trying to replace the let expression as let will not let me repeat bindings. |
| 2025-11-29 23:41:28 +0100 | tcard_ | (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) |
| 2025-11-29 23:41:15 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2025-11-29 23:41:11 +0100 | tcard_ | (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) (Remote host closed the connection) |
| 2025-11-29 23:40:08 +0100 | <Rembane> | Guest56: Yup, lets see. |
| 2025-11-29 23:39:37 +0100 | <Guest56> | Rembane you there? |
| 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? |