Logs: liberachat/#haskell
| 2026-04-15 16:43:35 | <Milan_Vanca> | Hello guyz, does pattern match on on constructor with strict fields when wildcard is used? rnf (Point x y) = () vs rnf (Point _ _) = () |
| 2026-04-15 16:44:38 | <Milan_Vanca> | does it fully evaluate all fields? I guess they are evaluated the moment constructor is called not when pattern matched |
| 2026-04-15 16:44:40 | <c_wraith> | Just in general, naming the fields or not does not affect whether they're evaluated by the match. |
| 2026-04-15 16:44:51 | <Milan_Vanca> | c_wraith: got it thanks |
| 2026-04-15 16:45:05 | <EvanR> | hmm. wasn't the question about strict fields not named fields |
| 2026-04-15 16:45:45 | <c_wraith> | not given the example |
| 2026-04-15 16:46:12 | <dminuoso> | c_wraith: Unclear, the fields could still be strict. |
| 2026-04-15 16:46:26 | <Milan_Vanca> | EvanR: Maybe both? example: data Point = Point !Int !Int and for that it is enough to rnf (Point _ _) = () right? |
| 2026-04-15 16:46:27 | <EvanR> | was assuming data Point = Point !Int !Int or something |
| 2026-04-15 16:46:57 | <EvanR> | :t rnf |
| 2026-04-15 16:46:58 | <lambdabot> | error: [GHC-88464] Variable not in scope: rnf |
| 2026-04-15 16:47:14 | <EvanR> | I thought rnf was supposed to return the value itself |
| 2026-04-15 16:47:17 | <Milan_Vanca> | :i NFData |
| 2026-04-15 16:47:21 | <c_wraith> | no, rnf returns () |
| 2026-04-15 16:47:24 | <EvanR> | oh |
| 2026-04-15 16:47:30 | <c_wraith> | you're thinking of force |
| 2026-04-15 16:47:47 | <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:48:09 | <c_wraith> | Specifically, strict fields are evaluated (to WHNF) when the constructor is evaluated. |
| 2026-04-15 16:48:33 | <dminuoso> | That said... Im not sure what would happen if you specified a lazy pattern match.. |
| 2026-04-15 16:48:58 | <c_wraith> | If you specified a lazy pattern match on Point, it would affect "when the constructor is evaluated" |
| 2026-04-15 16:49:00 | <dminuoso> | I would expect the fields to not be forced, but that's just a gut feeling |
| 2026-04-15 16:49:09 | <c_wraith> | If you specified a lazy pattern match on the fields, it would do nothing |
| 2026-04-15 16:49:27 | <dminuoso> | So lazyness trumps strictness? |
| 2026-04-15 16:49:30 | <c_wraith> | No. |
| 2026-04-15 16:49:50 | <c_wraith> | Strict fields are evaluated *when the constructor is*. |
| 2026-04-15 16:50:29 | <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:53:07 | <Milan_Vanca> | anyway ty for answer :) |
| 2026-04-15 16:53:33 | <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:54:39 | <EvanR> | that's correct. But it does look strange because Point undefined undefined ought to be semantically impossible xD |
| 2026-04-15 16:54:58 | <c_wraith> | err. I got the args to const backwards. go me. |
| 2026-04-15 16:55:22 | × | gmg quits (~user@user/gehmehgeh) (Remote host closed the connection) |
| 2026-04-15 16:55:22 | <EvanR> | (it only makes sense here if you put on glasses to distinguish code from values) |
| 2026-04-15 16:55:29 | <c_wraith> | Anyway, it's rather important to understand that lifted types can always be bottom |
| 2026-04-15 16:56:03 | → | gmg joins (~user@user/gehmehgeh) |
| 2026-04-15 16:56:32 | <c_wraith> | if you really want to completely prevent bottom values, you need to use an unlifted type |
| 2026-04-15 16:57:38 | <EvanR> | yes ⊥ is in the domain for Point but Point ⊥ ⊥ wouldn't be |
| 2026-04-15 17:04:38 | → | uli-fem joins (~uli-fem@203.87.114.209) |
| 2026-04-15 17:09:05 | <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:09:09 | × | uli-fem quits (~uli-fem@203.87.114.209) (Ping timeout: 255 seconds) |
| 2026-04-15 17:11:06 | × | califax quits (~califax@user/califx) (Quit: ZNC 1.10.1 - https://znc.in) |
| 2026-04-15 17:11:18 | → | califax joins (~califax@user/califx) |
| 2026-04-15 17:11:31 | → | jmcantrell_ joins (~weechat@user/jmcantrell) |
| 2026-04-15 17:11:52 | × | bggd quits (~bgg@user/bggd) (Remote host closed the connection) |
| 2026-04-15 17:12:32 | <janus> | is haskell compatible with iso-recursive typing? |
| 2026-04-15 17:12:52 | <janus> | i know the syntax makes it look equi-recursive but i am wondering whether there is a transformation |
| 2026-04-15 17:13:58 | <dminuoso> | https://hackage-content.haskell.org/package/base-4.22.0.0/docs/GHC-Exts.html#t:RuntimeRep |
| 2026-04-15 17:14:47 | <dminuoso> | Fun side-note: You can have boxed unlifted types. |
| 2026-04-15 17:18:40 | → | tromp joins (~textual@2001:1c00:340e:2700:60c1:e0e:2c45:a3f6) |
| 2026-04-15 17:18:53 | × | Googulator quits (~Googulato@94-21-172-213.pool.digikabel.hu) (Quit: Client closed) |
| 2026-04-15 17:19:16 | × | Milan_Vanca quits (~milan@user/Milan-Vanca:32634) (Quit: WeeChat 4.7.2) |
| 2026-04-15 17:19:20 | → | arandombit joins (~arandombi@2a02:2455:8656:7100:41ca:b44c:b589:e153) |
| 2026-04-15 17:19:20 | × | arandombit quits (~arandombi@2a02:2455:8656:7100:41ca:b44c:b589:e153) (Changing host) |
| 2026-04-15 17:19:20 | → | arandombit joins (~arandombi@user/arandombit) |
| 2026-04-15 17:19:24 | → | Googulator joins (~Googulato@94-21-172-213.pool.digikabel.hu) |
| 2026-04-15 17:24:08 | → | Square3 joins (~Square4@user/square) |
| 2026-04-15 17:26:35 | × | jle` quits (~jle`@2603:8001:3b00:11:2d70:9f38:ba84:72d9) (Ping timeout: 252 seconds) |
| 2026-04-15 17:27:33 | → | jle` joins (~jle`@2603:8001:3b00:11:4360:f9b:cc52:4598) |
| 2026-04-15 17:39:40 | → | uli-fem joins (~uli-fem@203.87.114.209) |
| 2026-04-15 17:41:53 | <ncf> | janus: wdym? haskell's recursive types are isorecursive |
| 2026-04-15 17:42:45 | <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:44:11 | × | uli-fem quits (~uli-fem@203.87.114.209) (Ping timeout: 252 seconds) |
| 2026-04-15 17:45:07 | <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:45:45 | <janus> | i am confused by variants being anonymous in TAPL, i guess.. |
| 2026-04-15 17:46:27 | <janus> | while in haskell, they're not. so now i have to juggle variants and recursiveness at the same time |
| 2026-04-15 17:51:49 | × | Enrico63 quits (~Enrico63@host-79-42-237-9.retail.telecomitalia.it) (Quit: Client closed) |
| 2026-04-15 17:56:28 | × | alter2000 quits (~alter2000@user/alter2000) (Ping timeout: 244 seconds) |
| 2026-04-15 17:56:34 | × | ouilemur quits (~jgmerritt@user/ouilemur) (Quit: WeeChat 4.9.0) |
| 2026-04-15 17:57:59 | <janus> | ncf: in 'data IntList = Nil | Cons Int IntList', what would be the witnesses of the isomorphism? |
| 2026-04-15 17:59:10 | → | uli-fem joins (~uli-fem@203.87.114.209) |
| 2026-04-15 17:59:30 | <monochrom> | Yes Haskell does iso-recursive, doesn't do equi-recursive. |
| 2026-04-15 17:59:47 | <EvanR> | isomorphism between what and what |
| 2026-04-15 18:00:09 | <EvanR> | Mu f `iso` f (Mu f) makes sense because it's a newtype |
| 2026-04-15 18:00:25 | <EvanR> | morally |
| 2026-04-15 18:00:40 | <monochrom> | Yeah with newtype you have that isomorphism. |
| 2026-04-15 18:01:10 | <monochrom> | With "data" you don't in Haskell, but you still do back in SML (generally strict languages). |
| 2026-04-15 18:01:31 | <janus> | the TAPL book talks about a an isomorphism between the type without it's own definition pasted in, and the one that has that replacement done |
| 2026-04-15 18:01:36 | <janus> | that is what they call fold/unfold |
| 2026-04-15 18:02:22 | × | craunts795335385 quits (~craunts@152.32.99.2) (Quit: The Lounge - https://thelounge.chat) |
| 2026-04-15 18:02:42 | <EvanR> | so IntList and 1 + Int x IntList |
| 2026-04-15 18:02:47 | <monochrom> | Yeah. |
| 2026-04-15 18:03:29 | → | craunts795335385 joins (~craunts@152.32.99.2) |
| 2026-04-15 18:03:31 | <janus> | monochrom: but 'data' still allows for recursion right? so how is that recursion described formally? is it neither iso nor equi? |
| 2026-04-15 18:03:34 | × | uli-fem quits (~uli-fem@203.87.114.209) (Ping timeout: 256 seconds) |
| 2026-04-15 18:05:51 | <EvanR> | \case {Nil -> Left (); Cons x xs -> Right (x,xs)} |
| 2026-04-15 18:06:14 | <EvanR> | \case {Left () -> Nil; Right (x,xs) -> Cons x xs} |
| 2026-04-15 18:06:20 | <monochrom> | Do you already know the denotational difference between "data D = D Int" and "newtype N = N Int"? |
| 2026-04-15 18:06:59 | <monochrom> | because that difference then carries over to "data X = X [X]" and "newtype Y = Y [Y]". Then X is not quite isomorphic to [X]. |
| 2026-04-15 18:07:51 | <monochrom> | This is something TaPL won't bring up because the author is from SML not Haskell. |
| 2026-04-15 18:07:54 | × | craunts795335385 quits (~craunts@152.32.99.2) (Client Quit) |
| 2026-04-15 18:08:16 | <monochrom> | or at least writing the book with that assumption. |
| 2026-04-15 18:10:09 | <monochrom> | Whereas for less mind-boggling examples like "data Z = Z | S Z" you have the expected isomorphism again! So all is not lost. |
| 2026-04-15 18:11:09 | → | alter2000 joins (~alter2000@user/alter2000) |
| 2026-04-15 18:11:14 | <monochrom> | Err no, I have to re-think it. |
| 2026-04-15 18:16:02 | → | Square2 joins (~Square@user/square) |
| 2026-04-15 18:16:04 | <monochrom> | Unfortunately Z has fewer bottoms than Either () Z too. Either Void Z should work, but it's a hack. |
| 2026-04-15 18:17:38 | × | Square2 quits (~Square@user/square) (Remote host closed the connection) |
| 2026-04-15 18:18:25 | → | Square2 joins (~Square@user/square) |
| 2026-04-15 18:21:40 | <monochrom> | I can imagine Bob Harper looking at all these annoyances and conclude "forget Haskell". :) |
| 2026-04-15 18:21:51 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-04-15 18:23:50 | <EvanR> | all the proofs can go through formally and haskell is just an exotic model |
All times are in UTC.