Logs: liberachat/#haskell
| 2025-12-18 14:31:38 | → | shaeto__ joins (~Shaeto@94.25.234.244) |
| 2025-12-18 14:32:52 | → | shaeto joins (~Shaeto@78.37.15.179) |
| 2025-12-18 14:33:28 | × | shaeto_ quits (~Shaeto@94.25.234.244) (Ping timeout: 260 seconds) |
| 2025-12-18 14:35:43 | × | shaeto__ quits (~Shaeto@94.25.234.244) (Ping timeout: 240 seconds) |
| 2025-12-18 14:36:31 | × | itaipu quits (~itaipu@168.121.97.28) (Ping timeout: 240 seconds) |
| 2025-12-18 14:36:41 | → | shaeto_ joins (~Shaeto@78.37.15.179) |
| 2025-12-18 14:37:25 | × | shaeto quits (~Shaeto@78.37.15.179) (Ping timeout: 255 seconds) |
| 2025-12-18 14:37:25 | <shaeto_> | hi, question, how to see code produced by "deriving (Eq, Ord)" for Peano numbers ? is it pure recursive or some hack for performance ? |
| 2025-12-18 14:37:46 | <tomsmeding> | the deriving-generated code is generally not very clever |
| 2025-12-18 14:38:31 | <tomsmeding> | shaeto_: you can pass -ddump-deriv to GHC to have deriving-generated code printed to stderr; an easy way to do this for a single module is to put {-# OPTIONS -ddump-deriv #-} at the top of the file |
| 2025-12-18 14:38:54 | <tomsmeding> | https://downloads.haskell.org/ghc/latest/docs/users_guide/flags.html#compiler-debugging-options |
| 2025-12-18 14:40:00 | <shaeto_> | @tomsmeding thank you, will try, i just want to understand it for learning purposes |
| 2025-12-18 14:40:00 | <lambdabot> | Unknown command, try @list |
| 2025-12-18 14:40:14 | <tomsmeding> | (we generally don't use @ on irc) |
| 2025-12-18 14:40:52 | → | itaipu joins (~itaipu@168.121.97.28) |
| 2025-12-18 14:41:16 | → | __monty__ joins (~toonn@user/toonn) |
| 2025-12-18 14:41:27 | <shaeto_> | tomsmeding: thank you |
| 2025-12-18 14:49:42 | × | carbolymer_ quits (~carbolyme@delirium.systems) () |
| 2025-12-18 14:49:54 | → | carbolymer joins (carbolymer@delirium.systems) |
| 2025-12-18 14:50:20 | × | itaipu quits (~itaipu@168.121.97.28) (Ping timeout: 245 seconds) |
| 2025-12-18 14:58:53 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 2025-12-18 15:01:07 | → | itaipu joins (~itaipu@168.121.97.28) |
| 2025-12-18 15:08:08 | → | shaeto joins (~Shaeto@94.25.234.244) |
| 2025-12-18 15:11:03 | × | shaeto_ quits (~Shaeto@78.37.15.179) (Ping timeout: 244 seconds) |
| 2025-12-18 15:17:11 | × | fp quits (~Thunderbi@2001:708:20:1406::10c5) (Quit: fp) |
| 2025-12-18 15:20:00 | ← | L29Ah parts (~L29Ah@wikipedia/L29Ah) () |
| 2025-12-18 15:20:42 | → | tromp joins (~textual@2001:1c00:3487:1b00:388e:400a:f906:df4a) |
| 2025-12-18 15:40:31 | × | somemathguy quits (~somemathg@user/somemathguy) (Ping timeout: 264 seconds) |
| 2025-12-18 15:44:22 | → | lambda_gibbon joins (~lambda_gi@208.83.175.39) |
| 2025-12-18 15:53:28 | × | wootehfoot quits (~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer) |
| 2025-12-18 15:53:47 | × | comerijn quits (~merijn@77.242.116.146) (Ping timeout: 250 seconds) |
| 2025-12-18 15:56:54 | → | merijn joins (~merijn@77.242.116.146) |
| 2025-12-18 16:00:08 | → | somemathguy joins (~somemathg@user/somemathguy) |
| 2025-12-18 16:00:10 | × | qqe quits (~qqq@185.54.20.98) (Quit: Lost terminal) |
| 2025-12-18 16:02:12 | × | somemathguy quits (~somemathg@user/somemathguy) (Client Quit) |
| 2025-12-18 16:07:38 | × | merijn quits (~merijn@77.242.116.146) (Quit: leaving) |
| 2025-12-18 16:22:53 | × | polux quits (~polux@51-15-169-172.rev.poneytelecom.eu) (Remote host closed the connection) |
| 2025-12-18 16:23:37 | → | hiredman joins (~hiredman@frontier1.downey.family) |
| 2025-12-18 16:29:32 | → | polux joins (~polux@51-15-169-172.rev.poneytelecom.eu) |
| 2025-12-18 16:29:40 | × | lucabtz quits (~lucabtz@user/lucabtz) (Quit: Lost terminal) |
| 2025-12-18 16:30:30 | × | tromp quits (~textual@2001:1c00:3487:1b00:388e:400a:f906:df4a) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-12-18 16:31:32 | → | Square2 joins (~Square@user/square) |
| 2025-12-18 16:32:52 | → | tromp joins (~textual@2001:1c00:3487:1b00:388e:400a:f906:df4a) |
| 2025-12-18 16:40:27 | → | merijn joins (~merijn@77.242.116.146) |
| 2025-12-18 16:44:48 | → | wootehfoot joins (~wootehfoo@user/wootehfoot) |
| 2025-12-18 17:00:08 | → | L29Ah joins (~L29Ah@wikipedia/L29Ah) |
| 2025-12-18 17:02:30 | <machinedgod> | Hi everyone. Does anyone here have a bit of experience with linear-base and LinearTypes? I can't seem to figure out how to get projection functions on my datatypes to be linear. |
| 2025-12-18 17:03:10 | <machinedgod> | Second issue: when I hide prelude and import Prelude.Linear - it seems like I lose ability to derive stock classes easily. Is this correct or I'm doing it wrong? |
| 2025-12-18 17:05:24 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 256 seconds) |
| 2025-12-18 17:14:44 | <tomsmeding> | machinedgod: I've never used Prelude.Linear, but I've used linear-base a bit; can you give a small code snippet showing precisely what projection functions you want? |
| 2025-12-18 17:15:24 | → | jbob joins (~jbob@172.59.173.118) |
| 2025-12-18 17:16:09 | × | jbob quits (~jbob@172.59.173.118) (Client Quit) |
| 2025-12-18 17:18:35 | × | sord937 quits (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
| 2025-12-18 17:20:14 | <machinedgod> | tomsmeding: Hey, thank you for replying! What I meant was, sorry for misusing a wrong term - a record selector function. Basically, a datatype with a named field - I would presume those auto-genned functions would be linear, when LinearTypes are enabled? |
| 2025-12-18 17:27:49 | <tomsmeding> | aparently not! |
| 2025-12-18 17:28:20 | <tomsmeding> | machinedgod: ah, see point 6 here https://downloads.haskell.org/ghc/latest/docs/users_guide/exts/linear_types.html#limitations |
| 2025-12-18 17:28:40 | <tomsmeding> | ah no that's not quite your question |
| 2025-12-18 17:31:46 | <tomsmeding> | machinedgod: the constructor of a data type _is_ linear by default, unless you explicitly make it not so using GADTSyntax |
| 2025-12-18 17:31:58 | → | marinelli joins (~weechat@gateway/tor-sasl/marinelli) |
| 2025-12-18 17:33:41 | <tomsmeding> | on reflection, yes, that bullet in the limitations _is_ your questoin |
| 2025-12-18 17:33:47 | <tomsmeding> | *question |
| 2025-12-18 17:40:12 | → | spew joins (~spew@user/spew) |
| 2025-12-18 17:41:14 | <machinedgod> | tomsmeding: Aye, that's a good answer! Thank you, I did check the user manual and I did look into limitations - but I misread the part about records. |
| 2025-12-18 17:42:20 | <machinedgod> | I am attempting to find a correct, uh... 'meta pattern' to use linear types. Its mainly to get some experience in usage. Do you maybe know what could I look at? |
| 2025-12-18 17:43:15 | <tomsmeding> | I'm not sure. I used it once for a very specific purpose, and it worked fine for that, but there are still a lot of rough edges, I think |
| 2025-12-18 17:43:40 | <tomsmeding> | decide what exactly you want to do with linearity, and find ways to accomplish that, is what I would say |
| 2025-12-18 17:43:52 | <tomsmeding> | making your whole program "linear" is not really a thing |
| 2025-12-18 17:48:38 | × | lambda_gibbon quits (~lambda_gi@208.83.175.39) (Ping timeout: 244 seconds) |
| 2025-12-18 17:49:04 | <machinedgod> | You're reading my mind :) One good advice I've gotten was to separate observation from mutation, and to add 'authority' tokens which have linear access. That's what I'm going to attempt to do, and see how far I get. |
| 2025-12-18 17:49:51 | <machinedgod> | But yeah, I honestly don't really have a clear goal on what do I want to accomplish - I have a toy project specifically crafted just so that I could toy around with lineary and 'real' problems and see what is doable, what isn't and what are the pros/cons. I've done the same thing when datakinds became a thing :) |
| 2025-12-18 17:51:14 | <tomsmeding> | "authority tokens" sound like a design pattern to simplify writing APIs that use linearity to enforce certain invariants. That still requires you to have an idea beforehand what invariants you want to enforce, exactly :) |
| 2025-12-18 17:51:30 | <tomsmeding> | I think that if you know that, it'll become clearer how to use linearity to accomplish that |
| 2025-12-18 17:51:34 | <tomsmeding> | (and if it doesn't, come back) |
| 2025-12-18 17:52:14 | <tomsmeding> | this is not to discourage you from experimenting, by the way! :) |
| 2025-12-18 17:55:43 | <machinedgod> | tomsmeding: Oh, I didn't feel like you're being discouraging, quite the oppoosite! You're here, spending time of your life to consult me for free - if that isn't practical encouraging, I don't know what is :) and, I am taking your advice to heart, I've just poured myself another cup of coffee, and rather than typing more code, I'm gonna sit, look at it and think for a bit |
| 2025-12-18 17:55:57 | <machinedgod> | Thank you, both for time and knowledge! |
| 2025-12-18 17:56:07 | <tomsmeding> | nice, have fun :) |
| 2025-12-18 17:56:27 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "") |
| 2025-12-18 18:00:47 | → | lambda_gibbon joins (~lambda_gi@208.83.175.39) |
| 2025-12-18 18:01:19 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2025-12-18 18:06:21 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 2025-12-18 18:15:32 | × | trickard quits (~trickard@cpe-81-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2025-12-18 18:15:44 | → | trickard joins (~trickard@cpe-81-98-47-163.wireline.com.au) |
| 2025-12-18 18:17:13 | → | merijn joins (~merijn@62.45.136.136) |
| 2025-12-18 18:17:21 | ← | L29Ah parts (~L29Ah@wikipedia/L29Ah) () |
| 2025-12-18 18:17:25 | × | lambda_gibbon quits (~lambda_gi@208.83.175.39) (Ping timeout: 264 seconds) |
| 2025-12-18 18:17:29 | → | jmcantrell_ joins (~weechat@user/jmcantrell) |
| 2025-12-18 18:17:48 | jmcantrell_ | is now known as jmcantrell |
| 2025-12-18 18:19:38 | × | Pozyomka quits (~pyon@user/pyon) (Quit: bbl) |
| 2025-12-18 18:21:54 | × | merijn quits (~merijn@62.45.136.136) (Ping timeout: 256 seconds) |
| 2025-12-18 18:29:50 | → | ljdarj joins (~Thunderbi@user/ljdarj) |
| 2025-12-18 18:30:38 | × | chele quits (~chele@user/chele) (Remote host closed the connection) |
| 2025-12-18 18:32:32 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2025-12-18 18:39:06 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-12-18 18:42:18 | → | tzh joins (~tzh@c-76-115-131-146.hsd1.or.comcast.net) |
| 2025-12-18 18:44:36 | × | acidjnk quits (~acidjnk@p200300d6e7171981f0c6dc9689540cc0.dip0.t-ipconnect.de) (Ping timeout: 252 seconds) |
| 2025-12-18 18:50:35 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2025-12-18 18:54:24 | → | L29Ah joins (~L29Ah@wikipedia/L29Ah) |
| 2025-12-18 18:55:20 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2025-12-18 18:55:37 | → | ljdarj1 joins (~Thunderbi@user/ljdarj) |
All times are in UTC.