Home freenode/#haskell: Logs Calendar

Logs: freenode/#haskell

←Prev  Next→
Page 1 .. 89 90 91 92 93 94 95 96 97 98 99 .. 5022
— 502,152 events total
2020-09-20 11:45:42 <ski> gpvs : so you definitely don't want the `class Show type_self => Animal type_self where say :: AWord type_word => type_self -> [type_word]' version, since it means that if you pass a `AnimalSpecific' to `say', then `say' will have to be able to compute a list of `type_word's for any instance of `AWord' `type_word', that the caller wants, not just for the `AWordDog' instance
2020-09-20 11:45:47 <edwardk> phadej: https://github.com/ekmett/haskell/tree/master/types is the project in question
2020-09-20 11:45:47 × lucid_0x80 quits (~lucid_0x8@188.253.232.248) (Ping timeout: 258 seconds)
2020-09-20 11:46:10 <edwardk> if i compile with -f-injectiveSucc then examples/Vec.hs goes to hell
2020-09-20 11:46:53 <ski> gpvs : so, it seems you either want an existential (but i suspect you don't actually want that here), or else you want to make `type_word' an additional parameter of `Animal' (possibly with a Functional Dependency)
2020-09-20 11:47:04 <gpvs> ski: oh, now I got it. Any reason first approach should not work?
2020-09-20 11:47:05 <edwardk> you may need to disable the construction of the SingI instances in Data.Type.Internal.TH as well here https://github.com/ekmett/haskell/blob/master/types/src/Data/Type/Internal/TH.hs#L122
2020-09-20 11:47:14 <ski> gpvs : hmm
2020-09-20 11:47:46 <edwardk> but if i write a manual data type that does it rather than emulate a GADT with my pattern synonym i can make it work *headdesk*
2020-09-20 11:48:05 × merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds)
2020-09-20 11:48:19 <ski> gpvs : "AWord is good enough abstraction for Animal-s to work with, there is no need to bind particular animals to particular words" -- but you just tried to associate `AnimalSpecific', not to arbitrary instances of `AWord', but specifically to `AWordDog'
2020-09-20 11:48:24 <edwardk> but i can't have the actual data type because i need a homogeneous representation for my singletons or i lose a huge performance tax.
2020-09-20 11:48:51 <ski> gpvs : that is, your implementation of `say' tried to do that
2020-09-20 11:49:00 <phadej> edwardk: I only understood "right and slow vs. doesn't work fast"
2020-09-20 11:49:09 <gpvs> ski: what's existential? could you provide a link or googling term please? I'm truing two avoid making type_word a parameter to Animal not to bind them
2020-09-20 11:49:21 <edwardk> the cost is linear vs O(1)
2020-09-20 11:49:30 <edwardk> i have hacked around every other obstacle in the way
2020-09-20 11:49:38 <edwardk> this is the last farking leg
2020-09-20 11:49:55 → Cale joins (~cale@99.253.130.57)
2020-09-20 11:50:12 <ski> gpvs : do you want to require `say' to return a list of `type_word's, for some `type_word' that's an instance of `AWord' (but each `say' implementation should be allowed to pick which such `type_word' it wants) ?
2020-09-20 11:50:42 × shad0w_ quits (~shad0w_@160.202.36.27) (Remote host closed the connection)
2020-09-20 11:50:44 <edwardk> in the process i dragged the Nat kind and hacked it to work like Natural as a type (which will just work when ghc does it for real), hacked Type to look like TypeRep, hacked Symbol to look like String, used stuck data families to get me ways to use Int and Char meaningfully as kinds.
2020-09-20 11:50:57 → heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net)
2020-09-20 11:51:00 <edwardk> and came up with a way to get constant time singletons
2020-09-20 11:51:13 <edwardk> which works for everything except when my singleton gets fancy enough
2020-09-20 11:51:17 <edwardk> and Nat is involved
2020-09-20 11:51:20 <edwardk> because Nat is awful
2020-09-20 11:51:30 <gpvs> ski: exactly. Any Animal's 'say' may return *any* value which is instance of AWord
2020-09-20 11:51:40 <gpvs> ski: * a list
2020-09-20 11:51:45 × __Joker quits (~Joker@180.151.105.65) (Ping timeout: 240 seconds)
2020-09-20 11:52:20 <ski> gpvs : could different elements of the list be of different types `type_word', provided all are instances of `AWord' ? or should all elements in the list be of the same type `type_word' ?
2020-09-20 11:53:10 <gpvs> ski: I don't have requirement for/against it at the moment. could you please provide both verions?
2020-09-20 11:53:19 <edwardk> phadej: that said, i really like using Type as Typeable.TypeRep. and then Type.Reflection.TypeRep becomes its singleton
2020-09-20 11:53:40 <edwardk> very pretty code results
2020-09-20 11:54:41 dddddd_ is now known as dddddd
2020-09-20 11:54:48 × Raito_Bezarius quits (~Raito_Bez@unaffiliated/raito-bezarius/x-8764578) (Remote host closed the connection)
2020-09-20 11:54:59 → Raito_Bezarius joins (~Raito_Bez@2001:bc8:38ee::1)
2020-09-20 11:55:02 <ski> gpvs : hm, let's consider alternatives, and what they would mean
2020-09-20 11:55:25 × heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 246 seconds)
2020-09-20 11:55:31 → josh joins (~josh@c-67-164-104-206.hsd1.ca.comcast.net)
2020-09-20 11:55:35 <Cale> I'm pretty sure from the looks of the code that made it into the channel that gpvs wants a fundep
2020-09-20 11:55:46 <Cale> But maybe I missed something
2020-09-20 11:55:49 × sfvm quits (~sfvm@37.228.215.148) (Quit: off to the basement, mixing up the medicine)
2020-09-20 11:55:54 × Raito_Bezarius quits (~Raito_Bez@2001:bc8:38ee::1) (Changing host)
2020-09-20 11:55:54 → Raito_Bezarius joins (~Raito_Bez@unaffiliated/raito-bezarius/x-8764578)
2020-09-20 11:56:04 <ski> gpvs : `class Show type_self => Animal type_self where say :: AWord type_word => type_self -> [type_word]' means that the caller of `say' will decide which `type_word' to pick, can pick any, as long as its an instance of `AWord'. and you said you don't want that
2020-09-20 11:56:15 → roconnor joins (~roconnor@host-45-78-255-115.dyn.295.ca)
2020-09-20 11:56:26 → Unhammer joins (~Unhammer@gateway/tor-sasl/unhammer)
2020-09-20 11:56:42 <Cale> gpvs: The type of the result should depend on the type of the input, right?
2020-09-20 11:57:04 → alx741 joins (~alx741@186.178.110.130)
2020-09-20 11:57:20 × Raito_Bezarius quits (~Raito_Bez@unaffiliated/raito-bezarius/x-8764578) (Read error: Connection reset by peer)
2020-09-20 11:57:27 × priyesh quits (~priyesh@84.39.117.57) (Remote host closed the connection)
2020-09-20 11:57:33 → Raito_Bezarius joins (~Raito_Bez@2001:bc8:38ee::1)
2020-09-20 11:57:37 <edwardk> looks like ghc-typelits-natnormalise isn't able to help solve the 1 + n ~ 1 + m ==> n ~ m problem
2020-09-20 11:57:56 <edwardk> i get the same issue with the plugin enabled
2020-09-20 11:58:28 <gpvs> ski: I don't want the rigid return type to be defined at type instantiation moment. I'm interesting in both version where return type is define on call or by implementation itself
2020-09-20 11:58:39 <Cale> edwardk: Can you use unsafeCoerce to get yourself out of that?
2020-09-20 11:58:41 <edwardk> the problem is that i'm neck deep in a pattern synonym at the time it happens and can't. really get both n and m in type in scope to unsafeCoerce my way to glory
2020-09-20 11:58:43 <ski> gpvs : `class (Show type_self, AWord type_word) => Animal type_self where say :: type_self -> [type_word]' means that you have associations between particular `type_self's and particular `type_word'. so, for a particular `type_self', you don't need to have all possible instances `type_word' of `AWord' to consider. you could just have some of them, if you'd like to. also, you could enforce it to be at most one `type_word', if you'd want to
2020-09-20 11:58:55 <Cale> ahh
2020-09-20 11:58:56 × Raito_Bezarius quits (~Raito_Bez@2001:bc8:38ee::1) (Client Quit)
2020-09-20 11:58:58 <edwardk> i've been trying ever more esoteric dances to make that work
2020-09-20 11:59:07 → Raito_Bezarius joins (~Raito_Bez@unaffiliated/raito-bezarius/x-8764578)
2020-09-20 11:59:25 <Cale> Pattern synonyms are jankier than I ever imagined they might be
2020-09-20 11:59:31 <gpvs> Cale: optionaly, but I don't want to bind Animal instances to particular AWord-s instances
2020-09-20 11:59:45 × josh quits (~josh@c-67-164-104-206.hsd1.ca.comcast.net) (Ping timeout: 240 seconds)
2020-09-20 11:59:59 <edwardk> https://github.com/ekmett/haskell/blob/master/types/example/Vec.hs#L49 the issue is it can't figure out ys is well typed there.
2020-09-20 12:00:14 × Raito_Bezarius quits (~Raito_Bez@unaffiliated/raito-bezarius/x-8764578) (Read error: Connection reset by peer)
2020-09-20 12:00:23 <Cale> gpvs: Maybe the solution is just a simple two parameter type class then
2020-09-20 12:00:32 → Raito_Bezarius joins (~Raito_Bez@unaffiliated/raito-bezarius/x-8764578)
2020-09-20 12:00:38 <edwardk> there is another issue involving the SingI instance but i can hack around that by moving the type synonym around
2020-09-20 12:00:49 <Cale> gpvs: Though, that won't be terribly *convenient* since you'll probably have to annotate the type of the result a lot, given that it can't be determined by the type of the input
2020-09-20 12:00:58 <edwardk> Cale: i'm doing evil things in there
2020-09-20 12:01:27 <ski> gpvs : the last option is existentials, which here would be either `class Show type_self => Animal type_self where say :: type_self -> exists type_word. AWord type_word *> [type_word]' or `class Show type_self => Animal type_self where say :: type_self -> [exists type_word. AWord type_word *> type_word]'. both of these will allow the choice of `type_word' to depend on the run-time input to `say' (if you don't want that, that could be corrected)
2020-09-20 12:01:27 <edwardk> Cale: in particular i'm emulating GADTs on a non GADT using pattern synonyms and another GADT as a helper to sort of scaffold all the equalities i need
2020-09-20 12:01:40 <gpvs> Cale: resulting types will bind particula Animals to particular Words then, wouldn't they?
2020-09-20 12:01:43 <ski> (er, possibly cut off part was "(if you don't want that, that could be corrected)")
2020-09-20 12:01:44 <edwardk> the scaffolding GADT is just unsafeCoerced to offer what i need
2020-09-20 12:02:15 × kicov quits (959c7c03@nat.ds3.agh.edu.pl) (Remote host closed the connection)
2020-09-20 12:02:28 <gpvs> Cale: I've just read what fundeps are and I believe it's not what I want
2020-09-20 12:02:35 × wei2912 quits (~wei2912@unaffiliated/wei2912) (Quit: Lost terminal)
2020-09-20 12:02:41 → mirrorbird joins (~psutcliff@2a00:801:44a:a00b:20c3:c64:eb15:73a2)
2020-09-20 12:03:39 <edwardk> pattern SVCons :: forall k (n :: Nat) (r :: Vec k (1 + n)). () => forall (x :: k) (xs :: Vec k n). r ~ 'VCons x xs => Sing x -> Sing xs -> Sing r; pattern SVCons y ys <- ( upSVec -> SVCons' y ys) where SVCons (Sing y) (Sing ys) = UnsafeSing (VCons y ys); should basically faithfully emulate the GADT constructor that it delegates down to for proof
2020-09-20 12:03:47 <Cale> gpvs: It would mean that, say, given that you have a list of Cats as input, then the type of words that Cats produce would be determined by the fact that they are Cats
2020-09-20 12:04:00 <Cale> For example, maybe Cats produce Text
2020-09-20 12:04:03 <edwardk> upSVec casts from Sing x -> SVec' x
2020-09-20 12:04:07 <gpvs> ski: "means that the caller of `say' will decide which `type_word' to pick, can pick any" how do I express it in Haskell from the callers perspective?
2020-09-20 12:04:14 <edwardk> but the constructor for SVec' is well typed and happy
2020-09-20 12:04:29 <edwardk> i just can't figure out the right way to pass through the lesson from SVec' to Sing
2020-09-20 12:04:36 <Cale> gpvs: That's just the two-parameter class with no functional dependencies
2020-09-20 12:04:37 → mpereira joins (~mpereira@2a02:810d:f40:d96:b46b:1e98:8653:4550)
2020-09-20 12:04:43 <edwardk> when it matches it learns a heterogeneous type equality
2020-09-20 12:04:52 × DavidEichmann quits (~david@43.240.198.146.dyn.plus.net) (Ping timeout: 246 seconds)
2020-09-20 12:05:07 <Cale> gpvs: and you can write type annotations like (say cats :: [Text]) to determine the type of result then
2020-09-20 12:05:24 <Cale> (or if it's determined by how the result is used, that's also fine
2020-09-20 12:05:26 <Cale> )
2020-09-20 12:05:27 <ski> gpvs : that option was already expressed in Haskell. i dunno what you mean by "from the callers perspective" (i was already talking there about it being the caller who got to pick `type_word' there)
2020-09-20 12:05:27 <edwardk> that the output type is carrying an argument of kind Vec k (S n) relative to Vec k n for the inside argument to the vector.
2020-09-20 12:07:47 <edwardk> -- just works (S n = 1 + n as a type synonym, Z = 0) -- so now what i want is a pattern synonym as a next step that just basically wraps SVCons0 https://www.irccloud.com/pastebin/j3dAUDko/svec0
2020-09-20 12:07:58 hackage binaryen 0.0.4.0 - Haskell bindings to binaryen https://hackage.haskell.org/package/binaryen-0.0.4.0 (terrorjack)
←Prev  Next→
Page 1 .. 89 90 91 92 93 94 95 96 97 98 99 .. 5022

All times are in UTC.