Newest at the top
| 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 |
| 2025-11-29 23:08:49 +0100 | <Guest56> | no, they have to be the same types |
| 2025-11-29 23:08:30 +0100 | <Rembane> | Guest56: Do they always have to be the same type or is it okay if they are different types sometimes? |
| 2025-11-29 23:06:34 +0100 | <Guest56> | So the actual code is on the lines of: Just (Arrow (MyType var1 var2) (MyType var1’ var3)) = ta |
| 2025-11-29 23:06:02 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-11-29 23:04:58 +0100 | <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 23:03:40 +0100 | szkl | (uid110435@id-110435.uxbridge.irccloud.com) (Quit: Connection closed for inactivity) |
| 2025-11-29 23:01:42 +0100 | <pavonia> | What syntax is the arrow in "let Just (MyType var1 var2 -> MyType var1’ var3) = ta"? |
| 2025-11-29 23:01:31 +0100 | euphores | (~SASL_euph@user/euphores) (Ping timeout: 264 seconds) |
| 2025-11-29 22:54:36 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-11-29 22:48:00 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-11-29 22:43:34 +0100 | <Guest56> | anyone? |
| 2025-11-29 22:37:31 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2025-11-29 22:37:28 +0100 | <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 22:37:28 +0100 | <Guest56> | else |
| 2025-11-29 22:37:27 +0100 | <Guest56> | then … |
| 2025-11-29 22:37:27 +0100 | <Guest56> | In if var1 == var1’ |
| 2025-11-29 22:37:26 +0100 | <Guest56> | let Just (MyType var1 var2 -> MyType var1’ var3) = ta …. Made sure that ta is not a Nothing already |
| 2025-11-29 22:37:26 +0100 | <Guest56> | … some more code |
| 2025-11-29 22:37:25 +0100 | <Guest56> | let ta = typeDeconstruct …. (This function returns a Maybe type) |
| 2025-11-29 22:37:25 +0100 | <Guest56> | … some code … |
| 2025-11-29 22:37:24 +0100 | <Guest56> | type var2 = String |