IRCBrowse

2025/02/12

2025-02-12 00:01:30 +0100 <dminuoso> euouae: That looks good.
2025-02-12 00:01:41 +0100alfiee(~alfiee@user/alfiee) (Ping timeout: 248 seconds)
2025-02-12 00:01:48 +0100mniip(mniip@libera/staff/mniip) mniip
2025-02-12 00:01:49 +0100peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich
2025-02-12 00:01:51 +0100 <dminuoso> euouae: So what you have conjured, is a `Lens (Vec3 a) a`
2025-02-12 00:02:12 +0100 <dminuoso> That is, that thing that "traverses over a single component using some functor", that is the lens.
2025-02-12 00:03:16 +0100 <euouae> I see the setter, but not the getter
2025-02-12 00:03:17 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds)
2025-02-12 00:03:23 +0100 <dminuoso> How do you `set` with that?
2025-02-12 00:03:38 +0100 <dminuoso> Curious whether you can find out yourself
2025-02-12 00:03:42 +0100 <euouae> traverseVecX (const v) vec
2025-02-12 00:03:57 +0100 <dminuoso> Interesting. You are close, but that wont work.
2025-02-12 00:04:10 +0100machinedgod(~machinedg@d108-173-18-100.abhsia.telus.net) machinedgod
2025-02-12 00:04:28 +0100 <dminuoso> You need to find a choice of `f` here.
2025-02-12 00:04:59 +0100 <euouae> Identity
2025-02-12 00:05:30 +0100 <dminuoso> Give it a try.
2025-02-12 00:05:38 +0100 <dminuoso> Have you peeked into the lens implementation before?
2025-02-12 00:06:20 +0100 <euouae> Not really I'm just reading the lens book
2025-02-12 00:06:27 +0100 <euouae> So far it's "how to use this" type of thing
2025-02-12 00:06:33 +0100 <dminuoso> Fair enough.
2025-02-12 00:06:51 +0100 <dminuoso> So there are two newtypes that seem rather useless or silly in isolation:
2025-02-12 00:06:58 +0100 <dminuoso> newtype Const a b = Const { getConst :: a }
2025-02-12 00:07:12 +0100 <dminuoso> newtype Const a b = Const { getConst :: a }
2025-02-12 00:07:15 +0100 <dminuoso> newtype Identity a = Identity { runIdentity :: a }
2025-02-12 00:07:56 +0100 <dminuoso> And both happen to be Functor. And it turns out that if you traverseVecX using those functors, it gives you the exact behavior of either extracting the thing it traverses over, or setting the value in place.
2025-02-12 00:09:05 +0100 <euouae> I made this work `traverseVecX (const 30) x :: Identity (Vec3 Int)`
2025-02-12 00:09:27 +0100 <euouae> oh? let me re-read what you said
2025-02-12 00:09:59 +0100 <dminuoso> euouae: Yeah, that way to "set" with Identity is correct.
2025-02-12 00:10:10 +0100 <dminuoso> euouae: https://hackage.haskell.org/package/lens-5.3.3/docs/src/Control.Lens.Setter.html#set
2025-02-12 00:10:30 +0100__monty__(~toonn@user/toonn) (Quit: leaving)
2025-02-12 00:11:01 +0100 <dminuoso> Note that your lens is a simple: Lens' (Vec3 a) a
2025-02-12 00:11:08 +0100 <euouae> so you're using `traverseVecX getConst vec`?
2025-02-12 00:11:35 +0100weary-traveler(~user@user/user363627) user363627
2025-02-12 00:12:05 +0100 <euouae> no, hm...
2025-02-12 00:12:35 +0100 <dminuoso> You just `traverseVec3 Const`, that's it!
2025-02-12 00:12:46 +0100 <dminuoso> (Well and getConst to unwrap it)
2025-02-12 00:13:32 +0100 <dminuoso> https://hackage.haskell.org/package/microlens-0.4.13.1/docs/src/Lens.Micro.Extras.html#view (the lens implementation has a small layer of indirection with `asks`, so this one is a bit easier to look at
2025-02-12 00:13:46 +0100 <dminuoso> euouae: And here comes the next cool part:
2025-02-12 00:13:51 +0100 <dminuoso> % :t traverse . traverse
2025-02-12 00:13:51 +0100 <yahb2> traverse . traverse ; :: (Applicative f, Traversable t1, Traversable t2) => ; (a -> f b) -> t1 (t2 a) -> f (t1 (t2 b))
2025-02-12 00:13:54 +0100 <dminuoso> % :t traverse . traverse . traverse)
2025-02-12 00:13:55 +0100 <yahb2> <interactive>:1:31: error: [GHC-58481] parse error on input ‘)’
2025-02-12 00:13:56 +0100 <dminuoso> % :t traverse . traverse . traverse
2025-02-12 00:13:56 +0100 <yahb2> traverse . traverse . traverse ; :: (Applicative f, Traversable t1, Traversable t2, ; Traversable t3) => ; (a -> f b) -> t1 (t2 (t3 a)) -> f (t1 (t2 (t3 b)))
2025-02-12 00:14:10 +0100 <dminuoso> Note how you can just compose these traverse-like functions to traverse over nested structures.
2025-02-12 00:14:19 +0100 <euouae> I'm not able to get an answer with getConst (traverseVecX Const (Vec3 1 2 3))
2025-02-12 00:14:28 +0100 <euouae> Maybe because there's no Show?
2025-02-12 00:14:35 +0100 <dminuoso> What error do you get?
2025-02-12 00:14:45 +0100 <euouae> I just get `getConst (traverseVecX Const x) :: (Monoid a, Num a) => a` as a type
2025-02-12 00:14:50 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-02-12 00:14:58 +0100 <euouae> I think it evaluates, I just don't know what it is, it's the repl on haskell-mode in emasc
2025-02-12 00:15:02 +0100 <dminuoso> euouae: Check your type.
2025-02-12 00:15:10 +0100 <dminuoso> Did you relax the constraint to Functor?
2025-02-12 00:15:17 +0100 <euouae> No its still Applicative
2025-02-12 00:15:21 +0100 <dminuoso> Thats why.
2025-02-12 00:15:24 +0100 <euouae> Oh, heh
2025-02-12 00:15:30 +0100 <dminuoso> We can use this to figure out what just happened next.
2025-02-12 00:15:35 +0100 <dminuoso> So
2025-02-12 00:15:57 +0100 <dminuoso> Consider your original traverseVec3 that traversed over all components, but needed Applicative
2025-02-12 00:16:14 +0100 <dminuoso> Use your Const, but instead of using Numbers maybe put strings into your Vec.
2025-02-12 00:16:16 +0100 <dminuoso> Give it a try.
2025-02-12 00:17:31 +0100 <dminuoso> And similiarly, try using Identity with that too.
2025-02-12 00:17:43 +0100 <mauke> "stringsareanicemonoid"
2025-02-12 00:18:12 +0100 <dminuoso> yada-yada-free-monoid
2025-02-12 00:19:52 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds)
2025-02-12 00:21:56 +0100 <euouae> I'm going to definitely refactor with just Functor and investigate how Const works, thank you
2025-02-12 00:22:04 +0100 <euouae> I'll do this tomorrow because there's stuff now to do
2025-02-12 00:22:25 +0100 <euouae> One thing that trips me up in Haskell is that I don't know if I'm dealing with a class or data whenever I see "Foo"... is this normal?
2025-02-12 00:22:37 +0100 <dminuoso> You can know.
2025-02-12 00:22:58 +0100 <euouae> Well if it is in the left of => it's a class?
2025-02-12 00:23:09 +0100 <dminuoso> A typeclass constraint can only appear in special places, normally not even in type position but only special constraint places.
2025-02-12 00:23:31 +0100 <euouae> right... just talking about "Const a b" though, you wouldn't know, you'd have to look into it
2025-02-12 00:23:32 +0100 <dminuoso> In places where values can appear, any identifier starting with an uppercase letter is a constructor of sorts.
2025-02-12 00:24:02 +0100 <dminuoso> euouae: well I did not mention `Const a b` in isolation.
2025-02-12 00:24:06 +0100 <euouae> I guess I need to be more conscious about it
2025-02-12 00:24:11 +0100 <dminuoso> newtype Const a b = Const { getConst :: a }
2025-02-12 00:24:21 +0100 <dminuoso> Or, with GADTSyntax (which I prefer):
2025-02-12 00:24:50 +0100Crypt-Lab(NSA@gateway/vpn/protonvpn/commanderbond007) CommanderBond007
2025-02-12 00:25:05 +0100CryptLab(NSA@gateway/vpn/protonvpn/commanderbond007) (Remote host closed the connection)
2025-02-12 00:25:15 +0100 <dminuoso> % newtype Const a b where Const :: a -> Const a b
2025-02-12 00:25:15 +0100 <yahb2> <no output>
2025-02-12 00:25:36 +0100ski'd really prefer various data types to not reuse the exact same name for the data constructor
2025-02-12 00:25:50 +0100 <dminuoso> euouae: One of the larger sources of confusion for beginners of haskell is the compact dense notation of data, where value-level constructor and types appear to be sitting right next to each other
2025-02-12 00:26:23 +0100 <dminuoso> ski: Have you worked with languages that have a shared namespace for types and value level constructs?
2025-02-12 00:26:39 +0100 <ski> dependently typed
2025-02-12 00:26:42 +0100 <dminuoso> Oh well, I guess in dependent types this would be natural
2025-02-12 00:26:44 +0100 <dminuoso> Yeah.
2025-02-12 00:27:54 +0100 <ski> but yea. having seen BNF before, the way `data' declarations work becomes a bit less unfamiliar
2025-02-12 00:27:56 +0100 <mauke> euouae: right, and with things like constraint types, it's completely ambiguous
2025-02-12 00:28:27 +0100 <mauke> type Wtf a = (Show a, Num a) -- what even is that
2025-02-12 00:28:53 +0100 <dminuoso> Wait until I hand you a `Dict Show`
2025-02-12 00:29:02 +0100 <mauke> that's illegal
2025-02-12 00:29:07 +0100 <dminuoso> Oh its not.
2025-02-12 00:29:20 +0100 <ski> `Dict (Show T)'
2025-02-12 00:29:41 +0100 <dminuoso> Oh I was a bit too quick with that assessment indeed.
2025-02-12 00:30:11 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-02-12 00:30:33 +0100 <mauke> newtype Identity runIdentity where Identity::a -> Identity a
2025-02-12 00:30:55 +0100 <ski> heh
2025-02-12 00:30:58 +0100 <euouae> mauke: I guess it's a restriction on what a can be? is that an extension?
2025-02-12 00:31:02 +0100 <jackdk> I had some code a while back that went hard on the stuff from package `constraints` to wrangle various `KnownNat` constraints. And then I fixed my design error and it all went away. But it was fun while it lasted.
2025-02-12 00:31:23 +0100 <dminuoso> euouae: `type ..` introduces just a type alias.
2025-02-12 00:31:39 +0100 <dminuoso> However...
2025-02-12 00:32:15 +0100 <mauke> euouae: https://downloads.haskell.org/ghc/latest/docs/users_guide/exts/constraint_kind.html
2025-02-12 00:32:37 +0100 <dminuoso> I think they were referring to `type Wtf ...`
2025-02-12 00:32:43 +0100 <dminuoso> % type Wtf a = (Show a, Num a)b
2025-02-12 00:32:43 +0100 <yahb2> <interactive>:183:29: error: [GHC-76037] ; Not in scope: type variable ‘b’
2025-02-12 00:32:45 +0100 <dminuoso> % type Wtf a = (Show a, Num a)
2025-02-12 00:32:45 +0100 <yahb2> <no output>
2025-02-12 00:33:31 +0100 <dminuoso> % f :: Wtf a => a -> a; f = id
2025-02-12 00:33:31 +0100 <yahb2> <no output>
2025-02-12 00:34:09 +0100 <ski> % let foo :: Wtf a => a -> String; foo n = show (show (n + 1)) in foo 42
2025-02-12 00:34:10 +0100 <yahb2> "\"43\""
2025-02-12 00:34:23 +0100tabaqui1(~root@87.200.129.102) (Ping timeout: 252 seconds)
2025-02-12 00:34:27 +0100 <euouae> oh it's a type constraint synonym that page says
2025-02-12 00:34:44 +0100 <euouae> so an intersection of Show and Num
2025-02-12 00:34:46 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-02-12 00:35:08 +0100 <ski> it's a compound constraint, consisting of two part constraints
2025-02-12 00:35:12 +0100 <dminuoso> euouae: This can be useful for situations where you may have a bunch of constraints that you want to repeatedly mention in type signatures.
2025-02-12 00:35:19 +0100 <euouae> right
2025-02-12 00:35:25 +0100 <dminuoso> Especially in effect systems like effectful.
2025-02-12 00:35:42 +0100 <ski> basically, "constraints live at the same level as types"
2025-02-12 00:37:06 +0100mange(~user@user/mange) mange
2025-02-12 00:37:21 +0100 <mauke> newtype Identity runIdentity where Identity :: { runIdentity :: a } -> Identity a
2025-02-12 00:37:35 +0100 <mauke> had to look up GADT record syntax
2025-02-12 00:38:48 +0100Tuplanolla(~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) Tuplanolla
2025-02-12 00:38:48 +0100 <dminuoso> % data Dict :: Constraint -> Type where Dict :: a => Dict a
2025-02-12 00:38:48 +0100 <yahb2> <no output>
2025-02-12 00:38:55 +0100 <dminuoso> % d = Dict :: Dict (Show Int)
2025-02-12 00:38:55 +0100 <yahb2> <no output>
2025-02-12 00:39:12 +0100 <dminuoso> Some portion of these constraints can exist at the value level too!
2025-02-12 00:39:42 +0100 <dminuoso> Not quite the constraints, but dictionaries of them.
2025-02-12 00:40:08 +0100 <dminuoso> And we can use them to discharge constraints at will, no longer are we at the whim of the compiler.
2025-02-12 00:40:16 +0100 <dminuoso> Finally, liberated.
2025-02-12 00:41:17 +0100 <dminuoso> I tried really hard to find a reason to use `constraints` in one of our projects.. but no matter the mental gymnastics, I couldn't even justify it to myself.
2025-02-12 00:42:01 +0100 <mauke> % let { foo :: Dict (Show a) -> a -> String; foo Dict x = show x } in foo Dict '?'
2025-02-12 00:42:01 +0100 <yahb2> "'?'"
2025-02-12 00:42:18 +0100 <mauke> % let { foo :: Dict (Show a) -> a -> String; foo _ x = show x } in foo Dict '?'
2025-02-12 00:42:18 +0100 <yahb2> <interactive>:231:54: error: [GHC-39999] ; • No instance for ‘Show a’ arising from a use of ‘show’ ; Possible fix: ; add (Show a) to the context of ; the type signature ...
2025-02-12 00:43:31 +0100 <dminuoso> % withDict :: Dict a -> (a => r) -> r; withDict d r = case d of Dict -> r
2025-02-12 00:43:31 +0100 <yahb2> <no output>
2025-02-12 00:43:50 +0100 <dminuoso> mauke: ^- you must pattern match for the GADT packed dict to discharge the surrounding constraint.
2025-02-12 00:44:13 +0100 <ski> that's the point, yes
2025-02-12 00:44:47 +0100 <dminuoso> This machinery lives on not just ConstraintKinds but also GADTs.
2025-02-12 00:45:33 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-02-12 00:46:02 +0100 <mauke> % let { withDict' :: Dict a -> (a => r) -> r; withDict' Dict = id } in ()
2025-02-12 00:46:03 +0100 <yahb2> <interactive>:237:62: error: [GHC-91028] ; • Couldn't match type ‘r’ with ‘a => r’ ; Expected: (a => r) -> r ; Actual: r -> r ; Cannot equate type variable ‘r’ ; with ...
2025-02-12 00:46:08 +0100alfiee(~alfiee@user/alfiee) alfiee
2025-02-12 00:46:14 +0100 <mauke> % let { withDict' :: Dict a -> (a => r) -> r; withDict' Dict r = r } in ()
2025-02-12 00:46:14 +0100 <yahb2> ()
2025-02-12 00:47:03 +0100 <dminuoso> Okay I find the diagnostic a bit surprising here.
2025-02-12 00:47:05 +0100 <mauke> eta reduction: destroyed
2025-02-12 00:49:17 +0100 <geekosaur> % :set -XDeepSubsumption
2025-02-12 00:49:17 +0100 <yahb2> <no output>
2025-02-12 00:49:38 +0100 <geekosaur> % let { withDict'' :: Dict a -> (a => r) -> r; withDict'' Dict = id } in ()
2025-02-12 00:49:39 +0100 <yahb2> ()
2025-02-12 00:49:50 +0100 <ski> (s/eta reduction/function extensionality/)
2025-02-12 00:50:10 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-02-12 00:50:32 +0100alfiee(~alfiee@user/alfiee) (Ping timeout: 252 seconds)
2025-02-12 00:51:33 +0100 <ski> perhaps there should be an explicit syntax for dictionary application ?
2025-02-12 00:52:03 +0100 <dminuoso> Do we have a suitable syntax for type application, now?
2025-02-12 00:52:20 +0100 <ski> debatable
2025-02-12 00:52:35 +0100 <dminuoso> I recall there was a proposal a while ago, but I cant quite remember the name of the extension
2025-02-12 00:53:02 +0100skidoesn't think the selection of `@' is great
2025-02-12 00:54:02 +0100 <dminuoso> % :set -XTypeAbstractions
2025-02-12 00:54:02 +0100 <yahb2> <no output>
2025-02-12 00:54:13 +0100 <dminuoso> % id @a x = (x :: a)
2025-02-12 00:54:13 +0100 <yahb2> <interactive>:263:4: error: [GHC-14964] ; • Invisible type pattern a has no associated forall ; • In an equation for ‘id’: id @a x = (x :: a)
2025-02-12 00:54:13 +0100 <ski> withShowable (WrapShowable @a x) k = k @a x -- could one write something like this ?
2025-02-12 00:54:20 +0100 <dminuoso> Hold on.
2025-02-12 00:54:37 +0100 <dminuoso> Invisible type pattern?
2025-02-12 00:54:49 +0100sawilagar(~sawilagar@user/sawilagar) (Ping timeout: 244 seconds)
2025-02-12 00:54:51 +0100 <dminuoso> % id :: a -> a; id @a x = (x :: a)
2025-02-12 00:54:51 +0100 <yahb2> <no output>
2025-02-12 00:55:09 +0100 <dminuoso> But that has no associated forall either..
2025-02-12 00:55:20 +0100 <ski> (assuming `data Showable = forall a. Show a => WrapShowable a', and `withShowable :: Showable -> (forall a. Show a => a -> o) -> o')
2025-02-12 00:56:31 +0100 <dminuoso> Oh well, I think I understand what the diagnostic is really trying to say
2025-02-12 00:58:09 +0100 <dminuoso> ski: At times I do wish we had a mechanism to just swap out typeclass instances, or have some overlapping ones and then decide which ones I want.
2025-02-12 00:58:25 +0100 <ski> mm
2025-02-12 00:59:03 +0100 <dminuoso> The discussions Ive seen over the years consistently bring up coherence issues, but they feel contrived.
2025-02-12 00:59:36 +0100 <ski> occasionally, i'd like to be able to define types (possibly non-locally depending on tyvars in scope) in `where' and `let', as well as making instances for them there
2025-02-12 00:59:56 +0100 <dminuoso> Oh, locally scoped instances yes.
2025-02-12 01:00:06 +0100peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 246 seconds)
2025-02-12 01:00:37 +0100 <ski> as long as the instance is given in the same scope as the data type, i think there'd be no issue with coherence
2025-02-12 01:00:57 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-02-12 01:01:14 +0100peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich
2025-02-12 01:01:39 +0100ljdarj1(~Thunderbi@user/ljdarj) ljdarj
2025-02-12 01:01:55 +0100 <dminuoso> At least for `data` GHC would have to drag the type in interface files in case of inlining.
2025-02-12 01:01:57 +0100 <ski> perhaps it would be nice to have two variants, one requiring uniqueness, and the other not .. i dunno
2025-02-12 01:02:09 +0100 <dminuoso> At that point I'm not too sure what benefit you would gain.
2025-02-12 01:02:11 +0100 <ski> mm
2025-02-12 01:02:24 +0100 <ski> benefit over what ?
2025-02-12 01:02:35 +0100 <dminuoso> A module level type
2025-02-12 01:02:38 +0100 <ski> ah
2025-02-12 01:02:41 +0100 <EvanR> dminuoso, it's really nice not having to worry about incoherent instances
2025-02-12 01:03:05 +0100 <ski> well, avoiding needing to parameterize over nonlocal tyvars, at least
2025-02-12 01:03:18 +0100 <dminuoso> EvanR: I've been using orphan instances a plenty lot without having any occurence of that.
2025-02-12 01:03:19 +0100 <EvanR> code A sees instance B while code C sees instance D of the same typeclass on the same type
2025-02-12 01:03:49 +0100 <dminuoso> EvanR: Note, Im not talking about forcing automatic instance resolution.
2025-02-12 01:04:08 +0100 <dminuoso> If we had the freedom to just say "Dont resolve, Ill decide here locally", much of the incoherence problems disappear.
2025-02-12 01:04:34 +0100 <EvanR> other languages have mechanisms for using explicit instances and there comes with it the additional cognitive overhead
2025-02-12 01:04:38 +0100 <dminuoso> I mean writing newtypes with custom instances, and then selecting those instances is not a problem either.
2025-02-12 01:04:57 +0100 <EvanR> just like using imperative programming everywhere where it wouldn't help 99% of the time
2025-02-12 01:05:15 +0100 <dminuoso> If we had a mechanism of dict application that just skipped the instance resolution, the big benefit would be not having to wrap through newtype just for force instance selection
2025-02-12 01:05:21 +0100ljdarj(~Thunderbi@user/ljdarj) (Ping timeout: 246 seconds)
2025-02-12 01:05:21 +0100ljdarj1ljdarj
2025-02-12 01:05:37 +0100 <EvanR> code A sees instance B while code C sees instance D of the same typeclass on the same type
2025-02-12 01:05:45 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
2025-02-12 01:05:47 +0100 <dminuoso> EvanR: Yes, and this is not a problem with newtype either.
2025-02-12 01:05:52 +0100 <EvanR> (when someone didn't expect this)
2025-02-12 01:06:09 +0100 <EvanR> I know, newtypes are great
2025-02-12 01:06:31 +0100 <EvanR> just slapping the newtype constructor activates the special behavior
2025-02-12 01:06:51 +0100 <EvanR> and no one is surprised
2025-02-12 01:08:17 +0100 <dminuoso> The one thing is just, that if you have `f :: forall a. Show a => ...` you know that f cant possibly use any newtype wrappers to swap out the Show instance because of parametricity.
2025-02-12 01:08:26 +0100 <dminuoso> Or well, except for those versions that do silly things
2025-02-12 01:08:33 +0100 <dminuoso> Say `newtype UppercaseShow ...`
2025-02-12 01:08:43 +0100 <dminuoso> Or `newtype SortAfterShow ...`
2025-02-12 01:09:00 +0100 <dminuoso> So dunno, feels like incoherence is already upon us,.
2025-02-12 01:09:05 +0100 <EvanR> yeah I have dumb newtypes specifically to change the show instance
2025-02-12 01:09:38 +0100 <EvanR> but Show type issues are a separate ergonomic issue from type class mechanisms I think