Newest at the top
| 2026-04-15 17:46:27 +0000 | <janus> | while in haskell, they're not. so now i have to juggle variants and recursiveness at the same time |
| 2026-04-15 17:45:45 +0000 | <janus> | i am confused by variants being anonymous in TAPL, i guess.. |
| 2026-04-15 17:45:07 +0000 | <janus> | it's just that in TAPL, they say that unfold/fold are primitives , and if they should work with recursive records in haskell, i don't see how it fits with what you're saying, because there is no name for the unwrapped Mu |
| 2026-04-15 17:44:11 +0000 | uli-fem | (~uli-fem@203.87.114.209) (Ping timeout: 252 seconds) |
| 2026-04-15 17:42:45 +0000 | <ncf> | e.g. in data Mu f = Mu { unMu :: f (Mu f) } you have Mu f ≃ f (Mu f) up to an isomorphism (witnessed by Mu and unMu), not an actual type equality |
| 2026-04-15 17:41:53 +0000 | <ncf> | janus: wdym? haskell's recursive types are isorecursive |
| 2026-04-15 17:39:40 +0000 | uli-fem | (~uli-fem@203.87.114.209) |
| 2026-04-15 17:27:33 +0000 | jle` | (~jle`@2603:8001:3b00:11:4360:f9b:cc52:4598) jle` |
| 2026-04-15 17:26:35 +0000 | jle` | (~jle`@2603:8001:3b00:11:2d70:9f38:ba84:72d9) (Ping timeout: 252 seconds) |
| 2026-04-15 17:24:08 +0000 | Square3 | (~Square4@user/square) Square |
| 2026-04-15 17:19:24 +0000 | Googulator | (~Googulato@94-21-172-213.pool.digikabel.hu) |
| 2026-04-15 17:19:20 +0000 | arandombit | (~arandombi@user/arandombit) arandombit |
| 2026-04-15 17:19:20 +0000 | arandombit | (~arandombi@2a02:2455:8656:7100:41ca:b44c:b589:e153) (Changing host) |
| 2026-04-15 17:19:20 +0000 | arandombit | (~arandombi@2a02:2455:8656:7100:41ca:b44c:b589:e153) |
| 2026-04-15 17:19:16 +0000 | Milan_Vanca | (~milan@user/Milan-Vanca:32634) (Quit: WeeChat 4.7.2) |
| 2026-04-15 17:18:53 +0000 | Googulator | (~Googulato@94-21-172-213.pool.digikabel.hu) (Quit: Client closed) |
| 2026-04-15 17:18:40 +0000 | tromp | (~textual@2001:1c00:340e:2700:60c1:e0e:2c45:a3f6) |
| 2026-04-15 17:14:47 +0000 | <dminuoso> | Fun side-note: You can have boxed unlifted types. |
| 2026-04-15 17:13:58 +0000 | <dminuoso> | https://hackage-content.haskell.org/package/base-4.22.0.0/docs/GHC-Exts.html#t:RuntimeRep |
| 2026-04-15 17:12:52 +0000 | <janus> | i know the syntax makes it look equi-recursive but i am wondering whether there is a transformation |
| 2026-04-15 17:12:32 +0000 | <janus> | is haskell compatible with iso-recursive typing? |
| 2026-04-15 17:11:52 +0000 | bggd | (~bgg@user/bggd) (Remote host closed the connection) |
| 2026-04-15 17:11:31 +0000 | jmcantrell_ | (~weechat@user/jmcantrell) jmcantrell |
| 2026-04-15 17:11:18 +0000 | califax | (~califax@user/califx) califx |
| 2026-04-15 17:11:06 +0000 | califax | (~califax@user/califx) (Quit: ZNC 1.10.1 - https://znc.in) |
| 2026-04-15 17:09:09 +0000 | uli-fem | (~uli-fem@203.87.114.209) (Ping timeout: 255 seconds) |
| 2026-04-15 17:09:05 +0000 | <c_wraith> | An attempt to create the latter becomes the former when evaluated, but before being evaluated it's all just an expression with a type. |
| 2026-04-15 17:04:38 +0000 | uli-fem | (~uli-fem@203.87.114.209) |
| 2026-04-15 16:57:38 +0000 | <EvanR> | yes ⊥ is in the domain for Point but Point ⊥ ⊥ wouldn't be |
| 2026-04-15 16:56:32 +0000 | <c_wraith> | if you really want to completely prevent bottom values, you need to use an unlifted type |
| 2026-04-15 16:56:03 +0000 | gmg | (~user@user/gehmehgeh) gehmehgeh |
| 2026-04-15 16:55:29 +0000 | <c_wraith> | Anyway, it's rather important to understand that lifted types can always be bottom |
| 2026-04-15 16:55:22 +0000 | <EvanR> | (it only makes sense here if you put on glasses to distinguish code from values) |
| 2026-04-15 16:55:22 +0000 | gmg | (~user@user/gehmehgeh) (Remote host closed the connection) |
| 2026-04-15 16:54:58 +0000 | <c_wraith> | err. I got the args to const backwards. go me. |
| 2026-04-15 16:54:39 +0000 | <EvanR> | that's correct. But it does look strange because Point undefined undefined ought to be semantically impossible xD |
| 2026-04-15 16:53:33 +0000 | <c_wraith> | Just like `const (Point undefined undefined) ()` wouldn't be a bottom. The argument is never evaluated, so the fact that the fields are strict is irrelevant. |
| 2026-04-15 16:53:07 +0000 | <Milan_Vanca> | anyway ty for answer :) |
| 2026-04-15 16:50:29 +0000 | <c_wraith> | If you choose not to evaluate the constructor by marking the match as irrefutable, then no evaluation takes place. Just like you asked for. |
| 2026-04-15 16:49:50 +0000 | <c_wraith> | Strict fields are evaluated *when the constructor is*. |
| 2026-04-15 16:49:30 +0000 | <c_wraith> | No. |
| 2026-04-15 16:49:27 +0000 | <dminuoso> | So lazyness trumps strictness? |
| 2026-04-15 16:49:09 +0000 | <c_wraith> | If you specified a lazy pattern match on the fields, it would do nothing |
| 2026-04-15 16:49:00 +0000 | <dminuoso> | I would expect the fields to not be forced, but that's just a gut feeling |
| 2026-04-15 16:48:58 +0000 | <c_wraith> | If you specified a lazy pattern match on Point, it would affect "when the constructor is evaluated" |
| 2026-04-15 16:48:33 +0000 | <dminuoso> | That said... Im not sure what would happen if you specified a lazy pattern match.. |
| 2026-04-15 16:48:09 +0000 | <c_wraith> | Specifically, strict fields are evaluated (to WHNF) when the constructor is evaluated. |
| 2026-04-15 16:47:47 +0000 | <dminuoso> | Milan_Vanca: But yes, if the fields are strict they are forced if the value is forced. That is the point of strict fields. |
| 2026-04-15 16:47:30 +0000 | <c_wraith> | you're thinking of force |
| 2026-04-15 16:47:24 +0000 | <EvanR> | oh |