Logs: freenode/#haskell
| 2021-05-06 14:26:43 | <superstar64> | or is there a more general form of this? |
| 2021-05-06 14:26:45 | × | ddellacosta quits (~ddellacos@ool-44c73afa.dyn.optonline.net) (Remote host closed the connection) |
| 2021-05-06 14:26:57 | → | hyperisco joins (~hyperisco@d192-186-117-226.static.comm.cgocable.net) |
| 2021-05-06 14:26:57 | <kuribas> | superstar64: are you new to haskell? |
| 2021-05-06 14:27:23 | <superstar64> | no, i'm trying to make my own language and i'm asking if something like this exists yet |
| 2021-05-06 14:27:46 | <kuribas> | superstar64: oh, I thought you meant linear types in haskell :) |
| 2021-05-06 14:27:51 | → | cr3 joins (~cr3@192-222-143-195.qc.cable.ebox.net) |
| 2021-05-06 14:28:09 | <tomsmeding> | are the s1 and s2 essential? |
| 2021-05-06 14:28:32 | <tomsmeding> | hm I guess if you want to preserve the information that the given function is linear in it |
| 2021-05-06 14:28:32 | × | benjamingr__ quits (uid23465@gateway/web/irccloud.com/x-vybrriwslamksbzv) (Quit: Connection closed for inactivity) |
| 2021-05-06 14:28:48 | → | ddellaco_ joins (~ddellacos@ool-44c73afa.dyn.optonline.net) |
| 2021-05-06 14:29:03 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 2021-05-06 14:29:42 | <superstar64> | i already know i want new and delete, where `new :: a ⊸ p a` and `delete : p a ⊸ a`, i just need to think of some other primitives |
| 2021-05-06 14:29:59 | <superstar64> | tomsmeding, they are bounded to `modify` like most other type variables |
| 2021-05-06 14:30:24 | <boxscape> | hmm it looks pretty similar to linear fmap |
| 2021-05-06 14:30:46 | × | frozenErebus quits (~frozenEre@37.231.244.249) (Ping timeout: 240 seconds) |
| 2021-05-06 14:30:55 | <superstar64> | it's not an fmap though, a pointer can't change it's type |
| 2021-05-06 14:31:12 | <superstar64> | or wait actually it could, it just can't change it's representation |
| 2021-05-06 14:31:39 | <tomsmeding> | superstar64: my point about s1/s2 was, is there an application of your modify that cannot be implemented using just modify' :: Pointer p => (a -o a) -o p a -o p a |
| 2021-05-06 14:32:53 | <boxscape> | if you had `newtype Pointer' p a b = Pointer' (p a, b)` it seems like `instance Pointer p => Functor (Pointer' p a)` would give you that |
| 2021-05-06 14:33:13 | <boxscape> | unless I messed up a type somewhere which is quite possible |
| 2021-05-06 14:33:17 | <tomsmeding> | but of course the point is that want to be able to have multiple pointers that you just pass through the computation, preserving the information that you're linear in them |
| 2021-05-06 14:33:34 | <superstar64> | tomsmeding, yes, `(a, world) = let !a = a; world' = print(a); (a, world')` or in general anything that modifies the world |
| 2021-05-06 14:34:12 | <superstar64> | `s` is usually going the world type i imagine |
| 2021-05-06 14:34:20 | <boxscape> | ah, I'm wrong |
| 2021-05-06 14:34:33 | <boxscape> | that would be `( s1 ⊸ s2) ⊸ (p a, s1) ⊸ (p a, s2)` |
| 2021-05-06 14:35:11 | → | cortexauth joins (~cortexaut@2409:4053:2d01:fc8a:2bda:f737:6878:919f) |
| 2021-05-06 14:35:12 | → | swater joins (bouhier200@perso.iiens.net) |
| 2021-05-06 14:35:38 | <superstar64> | boxscape, that's not too useful if `s1` has to be used linearily |
| 2021-05-06 14:35:51 | <boxscape> | mhm |
| 2021-05-06 14:36:10 | <superstar64> | or wait, nvm, that can't modify `a` at all |
| 2021-05-06 14:36:14 | <boxscape> | rigt |
| 2021-05-06 14:37:26 | <tomsmeding> | perhaps this is in general a useful operation to have on linear functors in the presence of linear types |
| 2021-05-06 14:37:33 | → | Pickchea joins (~private@unaffiliated/pickchea) |
| 2021-05-06 14:38:04 | <tomsmeding> | like, `fmap :: Functor f => (a -> b) -> f a -> f b` works fine, but `fmapL :: LinearFunctor f => (a -o b) -o f a -o f b` is kind of crippled |
| 2021-05-06 14:38:09 | <tomsmeding> | (making up LinearFunctor here) |
| 2021-05-06 14:38:22 | <boxscape> | tomsmeding you've made it up pretty well https://hackage.haskell.org/package/linear-base-0.1.0/docs/Control-Functor-Linear.html |
| 2021-05-06 14:38:33 | <tomsmeding> | because what you sometimes need is `fmapL' :: LinearFunctor f => ((a, s) -o (b, s')) -o (f a, s) -o (f b, s')` |
| 2021-05-06 14:38:44 | <[exa]> | why's the middle lollipop not a normal arrow? |
| 2021-05-06 14:38:57 | <boxscape> | [exa] it's a linear arrow, the argument must be used exactly once |
| 2021-05-06 14:39:06 | <boxscape> | or wait |
| 2021-05-06 14:39:08 | <boxscape> | you mean |
| 2021-05-06 14:39:10 | <boxscape> | why is it a linear aroow |
| 2021-05-06 14:39:24 | <tomsmeding> | [exa]: I guess that depends on the particular functor? |
| 2021-05-06 14:39:34 | <tomsmeding> | if the functor allows it being a -o, then a -o is strictly better |
| 2021-05-06 14:39:52 | <[exa]> | yeah, I don't see much reason in having it linear, not sure if that restriction isn't a bit too brutal if you still want to have some nice properties preserved |
| 2021-05-06 14:39:55 | → | proteusguy joins (~proteusgu@cm-58-10-209-239.revip7.asianet.co.th) |
| 2021-05-06 14:39:58 | <boxscape> | https://hackage.haskell.org/package/linear-base-0.1.0/docs/Data-Functor-Linear.html |
| 2021-05-06 14:40:00 | <boxscape> | this is the other kind |
| 2021-05-06 14:40:12 | <superstar64> | i mean, i can define a functor over pointers with `modify :: Pointer p => ((a, s1) ⊸ (b, s2)) ⊸ (p a, s1) ⊸ (p b, s2)`, but i don't think you can define `modify` in terms of functor maps |
| 2021-05-06 14:40:12 | <boxscape> | "All control functors are data functors, but not all data functors are control functors." |
| 2021-05-06 14:40:13 | → | nineonine joins (~nineonine@2604:3d08:7783:f200:98ea:cd24:b2e0:9b6f) |
| 2021-05-06 14:40:41 | <boxscape> | [exa] I haven't read it yet but here you go https://www.tweag.io/blog/2020-01-16-data-vs-control/ |
| 2021-05-06 14:41:03 | <tomsmeding> | oooo nice |
| 2021-05-06 14:41:12 | → | rekahsoft joins (~rekahsoft@38.29.28.2) |
| 2021-05-06 14:41:13 | <tomsmeding> | that's indeed precisely [exa]'s distinction |
| 2021-05-06 14:41:51 | <tomsmeding> | superstar64: no indeed you can't define your modify in terms of my fmapL |
| 2021-05-06 14:42:43 | <[exa]> | they don't use the -o for functors there, unless there's the need for it (e.g. when it becomes applicative and nees to consume the original wrap) |
| 2021-05-06 14:42:57 | <[exa]> | interesting, thanks for the pointer |
| 2021-05-06 14:44:55 | → | eacameron joins (uid256985@gateway/web/irccloud.com/x-ddrdfsfxoylsjvjk) |
| 2021-05-06 14:45:25 | × | nineonine quits (~nineonine@2604:3d08:7783:f200:98ea:cd24:b2e0:9b6f) (Ping timeout: 276 seconds) |
| 2021-05-06 14:45:33 | <[exa]> | superstar64: one note, I was actually trying to play with this stuff some time ago as well (and didn't have much time for it), `modify` composes brutally bad. If you don't need the whole program to be totally linear, it's much more useful to view the pointers in a lensish way, as isos |
| 2021-05-06 14:46:39 | <superstar64> | i'm trying to define primitives for pointers in my language, what would these lensish ones look like? |
| 2021-05-06 14:46:43 | <tomsmeding> | superstar64: heh there's your modify, kind of, in 'on2' |
| 2021-05-06 14:46:48 | <tomsmeding> | in the linked blog post |
| 2021-05-06 14:46:56 | <tomsmeding> | at least part of the way there |
| 2021-05-06 14:47:00 | <[exa]> | at the bare minimum, it gives straightforward combinators to access various deeply nested pointy stuff without feeling like writing assembly all over again |
| 2021-05-06 14:47:35 | <[exa]> | ah if that's for some base primitives then that's good I guess |
| 2021-05-06 14:47:41 | <superstar64> | can these more complicated one be built on top of `modify` [exa]? |
| 2021-05-06 14:47:48 | <[exa]> | I guess so |
| 2021-05-06 14:48:01 | × | cortexauth quits (~cortexaut@2409:4053:2d01:fc8a:2bda:f737:6878:919f) (Ping timeout: 276 seconds) |
| 2021-05-06 14:48:24 | → | cortexauth joins (~cortexaut@2409:4053:2291:557d:1149:3540:fa21:7f76) |
| 2021-05-06 14:48:26 | → | wonko7 joins (~wonko7@62.115.229.50) |
| 2021-05-06 14:48:35 | <superstar64> | i think `modify` can be built in terms of `new` and `delete` but that's not very practical |
| 2021-05-06 14:48:39 | × | Gurkenglas quits (~Gurkengla@unaffiliated/gurkenglas) (Read error: Connection reset by peer) |
| 2021-05-06 14:48:57 | <superstar64> | i also need to come up with a version for shared pointers too, somehow |
| 2021-05-06 14:49:06 | → | Gurkenglas joins (~Gurkengla@unaffiliated/gurkenglas) |
| 2021-05-06 14:49:09 | <[exa]> | we had a toy implementation over a mutable vector in ST but that was a single-seminar thing and I guess the code is lost |
| 2021-05-06 14:49:47 | → | dorkside joins (~tdbgamer@208.190.197.222) |
| 2021-05-06 14:49:53 | → | Deide joins (~Deide@217.155.19.23) |
| 2021-05-06 14:51:12 | × | royal_screwup213 quits (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) (Quit: Connection closed) |
| 2021-05-06 14:51:31 | → | royal_screwup213 joins (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) |
| 2021-05-06 14:51:39 | × | justanotheruser quits (~justanoth@unaffiliated/justanotheruser) (Ping timeout: 245 seconds) |
| 2021-05-06 14:51:59 | <tomsmeding> | there is a nice proof-of-concept of mutable arrays in the linear constraints paper, though that uses linear _constraints_, which is either in ghc 9.2 or not in any release at all yet |
| 2021-05-06 14:52:10 | <tomsmeding> | https://arxiv.org/abs/2103.06127 |
| 2021-05-06 14:52:17 | → | frozenErebus joins (~frozenEre@37.231.244.249) |
| 2021-05-06 14:52:34 | <tomsmeding> | (section 3.1-3.2) |
| 2021-05-06 14:53:28 | <tomsmeding> | but of course linear constraints are desugarable to normal linear types code, so it's not like it's impossible to do with normal linear haskell |
| 2021-05-06 14:54:27 | <boxscape> | would the syntax be %1=> ? If so, it doesn't seem to be in HEAD. |
| 2021-05-06 14:54:39 | <superstar64> | thanks, tomsmeding, i'll have to look though that paper later |
| 2021-05-06 14:54:39 | <tomsmeding> | ¯\_(ツ)_/¯ |
| 2021-05-06 14:54:47 | <boxscape> | fair enough |
| 2021-05-06 14:54:50 | <tomsmeding> | :p |
| 2021-05-06 14:54:59 | <tomsmeding> | just read the paper for a reading group :p |
| 2021-05-06 14:55:27 | <tomsmeding> | if they made the syntax something else than %1=> that would be really weird though |
| 2021-05-06 14:55:49 | × | cortexauth quits (~cortexaut@2409:4053:2291:557d:1149:3540:fa21:7f76) (Ping timeout: 276 seconds) |
| 2021-05-06 14:56:48 | → | cortexauth joins (~cortexaut@2409:4053:2291:557d:9c7c:7508:1d26:929d) |
| 2021-05-06 14:56:53 | <boxscape> | yeah |
| 2021-05-06 14:57:29 | × | toppler quits (~user@mtop.default.momentoftop.uk0.bigv.io) (Read error: Connection reset by peer) |
| 2021-05-06 14:57:46 | → | toppler joins (~user@mtop.default.momentoftop.uk0.bigv.io) |
All times are in UTC.