Home freenode/#haskell: Logs Calendar

Logs: freenode/#haskell

←Prev  Next→
Page 1 .. 91 92 93 94 95 96 97 98 99 100 101 .. 5022
— 502,152 events total
2020-09-20 12:32:35 → heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net)
2020-09-20 12:32:41 <ski> gpvs : that's a pretty vague, non-committal description
2020-09-20 12:33:01 <gpvs> lamdabot: thanks for the link
2020-09-20 12:34:05 <ski> gpvs : (a) often you don't want/need OO-style things; (b) if you do, ordinary lexical scoping with records commonly suffice; (c) sometimes existentials may be required
2020-09-20 12:34:30 <bicho_rastrero> I'm learning haskell and I saw this syntax in a function "merge list1@(x: xs) list2@(y : ys)", what is the name of the @ operator there? How is that structure named?
2020-09-20 12:34:36 <ski> gpvs : you should probably not reach for existentials, unless you really need them
2020-09-20 12:35:25 <ski> bicho_rastrero : "as-patterns"
2020-09-20 12:35:30 <gpvs> ski: part I stumbled on is the last part of description. Any type of class node should be able to return a list of nodes it's connected to, these nodes might be of different types, but of the same base class.
2020-09-20 12:35:48 <bicho_rastrero> Thank you, ski
2020-09-20 12:36:12 → ericsagnes joins (~ericsagne@2405:6580:0:5100:59cb:4e8f:c201:4e04)
2020-09-20 12:36:16 <ski> bicho_rastrero : it's both giving a name to the whole input, and simultaneously matching it with a pattern, so that you can check its shape, and name parts
2020-09-20 12:36:26 × carif quits (~mcarifio@cpe-67-246-228-200.rochester.res.rr.com) (Quit: Leaving)
2020-09-20 12:37:00 <bicho_rastrero> Yeah, that was my understanding, but I wanted to read an proper explanation with more examples. Thanks.
2020-09-20 12:37:04 <ski> gpvs : yea, it sounds like you could possibly do that with just (b)
2020-09-20 12:37:17 <ski> (depending on the specifics of what you want to do with them)
2020-09-20 12:37:23 × heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 260 seconds)
2020-09-20 12:37:31 <ski> gpvs : iow the record-of-operations that Cale mentioned
2020-09-20 12:39:01 × utopic_int0x80 quits (~lucid_0x8@188.253.237.87) (Ping timeout: 260 seconds)
2020-09-20 12:39:08 → drbean joins (~drbean@TC210-63-209-85.static.apol.com.tw)
2020-09-20 12:40:02 → ukari joins (~ukari@unaffiliated/ukari)
2020-09-20 12:42:28 → pfurla joins (~pfurla@ool-182ed2e2.dyn.optonline.net)
2020-09-20 12:42:54 → henninb joins (~henninb@63-226-191-96.mpls.qwest.net)
2020-09-20 12:44:15 × henninb quits (~henninb@63-226-191-96.mpls.qwest.net) (Client Quit)
2020-09-20 12:44:27 <Cale> edwardk: Ah, so annoying to try to get these n1 and n2 in scope...
2020-09-20 12:44:35 <edwardk> exactly!
2020-09-20 12:44:35 → henninb joins (~henninb@63-226-191-96.mpls.qwest.net)
2020-09-20 12:44:40 × henninb quits (~henninb@63-226-191-96.mpls.qwest.net) (Client Quit)
2020-09-20 12:45:06 <Cale> It's not even syntactically permitted to write something like pattern SVCons y (ys :: ...)
2020-09-20 12:45:13 → henninb joins (~henninb@63-226-191-96.mpls.qwest.net)
2020-09-20 12:45:19 → bitmagie joins (~Thunderbi@200116b8062b2e00fc59d02ac7bcf06a.dip.versatel-1u1.de)
2020-09-20 12:46:44 <edwardk> i fought with writing (\x -> case upSNat x of ... -> (sometypeequality,y,ys) ) -> (Refl,y,ys))
2020-09-20 12:46:52 <edwardk> for the viewpattern
2020-09-20 12:47:00 <edwardk> but that didn't move the needle much
2020-09-20 12:47:26 <edwardk> if S is replaced with data family S :: Nat -> k -- this just works
2020-09-20 12:47:44 <edwardk> but then i'm adding exotic types to kind Nat
2020-09-20 12:47:47 <Cale> I wrote this thing: onePlusInj :: forall n m r. ((1+n) ~ (1+m)) => (n ~ m => r) -> r but of course, I need to disambiguate which types I want to use it with
2020-09-20 12:47:55 <edwardk> yeah
2020-09-20 12:47:58 <edwardk> did the same
2020-09-20 12:48:02 <Cale> The idea being that maybe we can stick it in using a view pattern
2020-09-20 12:48:17 <edwardk> thats the sort of thing the scenario above tried to use
2020-09-20 12:48:18 × coot quits (~coot@37.30.55.202.nat.umts.dynamic.t-mobile.pl) (Ping timeout: 272 seconds)
2020-09-20 12:48:25 <Cale> yeah, I see
2020-09-20 12:48:26 <Cale> hmm
2020-09-20 12:48:27 <edwardk> the someTypeEquality thing there can be a refl built
2020-09-20 12:48:41 <edwardk> and in there i can see x and the types of y and ys
2020-09-20 12:48:54 <edwardk> before i return them out to the surrounding context
2020-09-20 12:50:18 → kicov joins (959c7c03@nat.ds3.agh.edu.pl)
2020-09-20 12:51:41 <kicov> Hi, one more question about liquid haskell : are annotation such as `function :: f:(Int -> Int) -> {ret : Int | f ret == 0}` possible, or is something similiar also possible ?
2020-09-20 12:51:55 <Cale> btw, I love the super janky required () => in the type of the pattern synonym
2020-09-20 12:52:09 <Cale> It inspires so much confidence in GHC
2020-09-20 12:52:48 <edwardk> i also run into problems when i go to write the SingI instance. morally its instance (SingI a, SingI b) => SingI ('VCons a b) -- but the argumentthere has a type synonym in it!
2020-09-20 12:53:18 <edwardk> which prevents me from hanging the instance
2020-09-20 12:53:19 <Cale> I wonder... can we bind (kind/type) variables in the pattern's type signature? Does that work?
2020-09-20 12:53:26 → heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net)
2020-09-20 12:53:32 <edwardk> oh let me give you a longer worked version
2020-09-20 12:53:46 <edwardk> yes
2020-09-20 12:54:19 <edwardk> forall variables. (context needed to call the pattern) => forall more variables (stuff you learn by binding the pattern) => pattern args -> pattern result
2020-09-20 12:54:30 <edwardk> the two context thing is deliberate
2020-09-20 12:54:33 <edwardk> it was the chosen syntax
2020-09-20 12:54:39 <edwardk> by ghc ghc
2020-09-20 12:54:41 <edwardk> er ghc hq
2020-09-20 12:54:57 hackage inline-c 0.9.1.1 - Write Haskell source files including C code inline. No FFI required. https://hackage.haskell.org/package/inline-c-0.9.1.1 (FrancescoMazzoli)
2020-09-20 12:55:17 <edwardk> to disambiguate between what you need to call the pattern (like fromjson, tojson, etc.) and what you learn by matching. (like GADT existential args)
2020-09-20 12:55:33 → kenran joins (~maier@b2b-37-24-119-190.unitymedia.biz)
2020-09-20 12:56:19 → nbloomf joins (~nbloomf@2600:1700:83e0:1f40:118d:2a8:7881:1f11)
2020-09-20 12:56:40 → utopic_int0x80 joins (~lucid_0x8@188.253.237.87)
2020-09-20 12:57:56 × heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 256 seconds)
2020-09-20 12:58:25 <gpvs> lambdabot: <https://lukepalmer.wordpress.com/2010/01/24/haskell-antipattern-existential-typeclass/> yeah, this actually made sense for me once I recalled there is currying
2020-09-20 12:58:34 → merijn joins (~merijn@83-160-49-249.ip.xs4all.nl)
2020-09-20 12:58:39 <gpvs> ski, Cale, lamdabot: thank you for your help!
2020-09-20 12:58:40 → ystael joins (~ystael@209.6.50.55)
2020-09-20 12:58:59 × gpvs quits (~gp@37.57.178.79) (Quit: Leaving.)
2020-09-20 13:00:58 × kenran quits (~maier@b2b-37-24-119-190.unitymedia.biz) (Ping timeout: 272 seconds)
2020-09-20 13:01:47 × ph88^ quits (~ph88@ip5f5af726.dynamic.kabel-deutschland.de) (Ping timeout: 240 seconds)
2020-09-20 13:03:19 × fiQ2 quits (~fiQ@mirkk.ninja) (Ping timeout: 246 seconds)
2020-09-20 13:04:02 × laxask quits (~lax@unaffiliated/laxask) (Ping timeout: 246 seconds)
2020-09-20 13:04:35 ski suspects gpvs meant "partial application"
2020-09-20 13:08:28 <Cale> edwardk: I got... something... to compile
2020-09-20 13:08:43 <Cale> I'm not sure if it's not just completely fucked, one sec :D
2020-09-20 13:08:43 <edwardk> i have a few versions that compile, but none that learn when they match
2020-09-20 13:08:54 × henninb quits (~henninb@63-226-191-96.mpls.qwest.net) (Quit: leaving)
2020-09-20 13:09:42 × bicho_rastrero quits (~cerdito@169.85-87-37.dynamic.clientes.euskaltel.es) (Remote host closed the connection)
2020-09-20 13:09:53 <edwardk> pattern SVCons :: forall (k::Type) (x::k) (n::Nat) (xs :: Vec k n). () => () => Sing x -> Sing xs -> Sing ('VCons x xs :: Vec k (S n)); pattern SVCons a b <- (upSVec -> (SVCons' a b :: SVec' ('VCons a b))) where SVCons (Sing y) (Sing ys) = UnsafeSing (VCons y ys)
2020-09-20 13:10:27 → polyrain joins (~polyrain@2001:8003:e501:6901:3846:7fa4:c749:eb08)
2020-09-20 13:10:35 <Cale> Yeah, that looks pretty similar
2020-09-20 13:11:08 → laxask joins (~lax@unaffiliated/laxask)
2020-09-20 13:11:35 <edwardk> all of this is to hack around the injectivity of succ, if it was there i could just use literally the same code i generate via template haskell for everything else
2020-09-20 13:11:56 <Cale> oh wait, what if we just need r ~ 'VCons x xs twice?
2020-09-20 13:12:05 <edwardk> but if i get gimped by any attempt to use kind nat, which perforce infects Int and other numeric types i lift i get screwed up
2020-09-20 13:12:08 <edwardk> ?
2020-09-20 13:12:45 × utopic_int0x80 quits (~lucid_0x8@188.253.237.87) (Ping timeout: 240 seconds)
2020-09-20 13:12:45 <edwardk> oh, the ~ there is probably going to be a ~~
2020-09-20 13:13:04 <edwardk> the starting Vec k n needs to learn it is Vec k n' but that is the kind for the argument type
2020-09-20 13:13:15 <edwardk> so you need to learn both the kind and the type
2020-09-20 13:13:20 <edwardk> which is ~~'s job
2020-09-20 13:13:32 × suppi quits (~suppi@2605:f700:40:c00::e6fc:6842) (Ping timeout: 260 seconds)
2020-09-20 13:13:33 <Cale> Do you have an example usage handy?
2020-09-20 13:13:47 <Cale> (of using the pattern synonym to learn the equality)
2020-09-20 13:14:11 → heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net)
2020-09-20 13:14:28 × acidjnk_new2 quits (~acidjnk@p200300d0c736584378afc0f7e05aaafd.dip0.t-ipconnect.de) (Remote host closed the connection)
←Prev  Next→
Page 1 .. 91 92 93 94 95 96 97 98 99 100 101 .. 5022

All times are in UTC.