Home freenode/#haskell: Logs Calendar

Logs: freenode/#haskell

←Prev  Next→
Page 1 .. 11 12 13 14 15 16 17 18 19 20 21 .. 5022
— 502,152 events total
2020-09-17 05:47:11 → mrte joins (~mrt@p4fcabee7.dip0.t-ipconnect.de)
2020-09-17 05:47:11 <edwardk> look at the environments
2020-09-17 05:47:26 <topos> Axman6 yeah
2020-09-17 05:47:27 <edwardk> you have Gamma, x : T
2020-09-17 05:47:31 <shafox> Anyone can share their ~/.cabal/config file. I want to know what I can do with all the options.
2020-09-17 05:47:49 <edwardk> add a member of some semiring with nice properties to the : annotating each typing judgment
2020-09-17 05:48:05 <edwardk> e.g. you might choose the semiring to have 0 for erased, 1 for present
2020-09-17 05:48:26 × elliott_ quits (~elliott@pool-71-114-77-65.washdc.fios.verizon.net) (Ping timeout: 272 seconds)
2020-09-17 05:48:42 <edwardk> and then you run through all the usual rules of type theory, treating environments as semimodules (like vector spaces) over this scalar semiring
2020-09-17 05:48:47 <edwardk> why?
2020-09-17 05:48:53 <topos> Axman6 when i benched, computing the modulus was faster than doing yet another index look up on a different table. but i have come a long way with it and i might need to revisit
2020-09-17 05:49:01 <edwardk> you get to use this to compute erasure for one.
2020-09-17 05:49:35 <edwardk> but if you replace the semiring with {0,1,many} with 1+1=many, you get something like linear haskell
2020-09-17 05:49:40 <edwardk> but you can pick all sorts of other semirings
2020-09-17 05:49:57 <edwardk> e.g. just using the natural numbers would get you something like granule where you get exact usage counts of all variables
2020-09-17 05:50:09 <siraben> Oh that's fascinating, so the resource usage is determined by the chosen semiring?
2020-09-17 05:50:16 <topos> Axman6 sorry - wires crossed. i can get rid of that shift, yeah
2020-09-17 05:50:30 <edwardk> or using {0,1,affine,relevant,unrestricted} you can get something like david walker's post in "Advanced Topics in Types and Programming Languages"
2020-09-17 05:50:32 <edwardk> yeah
2020-09-17 05:50:54 <edwardk> i've been using a semiring with 6 elements, rather than those 5. {0,1,affine,relevant,STRICT,unrestricted}
2020-09-17 05:51:02 <edwardk> where strict and relevance are closely related but not the same
2020-09-17 05:52:04 × mrte quits (~mrt@p4fcabee7.dip0.t-ipconnect.de) (Ping timeout: 260 seconds)
2020-09-17 05:52:16 <edwardk> in my toy type theory 1, strict, relevant all act as the dividing line at which i no longer have thunks in my data types. 0 doesn't exist at all in the result, and affine/unrestricted are lazy
2020-09-17 05:53:08 <edwardk> and 1 + 1 is relevant, but 1 + affine = strict rather than unrestricted like it'd be in the 5 point semiring above
2020-09-17 05:53:28 → ggole joins (~ggole@2001:8003:8119:7200:7c4d:5b32:3cf7:fd63)
2020-09-17 05:53:30 <edwardk> strictness then becomes the claim that you will definitely consume at least one of the copies of the thing you passed out to a bunch of sites
2020-09-17 05:53:40 <edwardk> where relevance is the claim you will consume ALL of them
2020-09-17 05:55:31 <edwardk> the dividing line is something like how relevance _could_ be managed by something that basically copied each A and made two of them and passed each out. Then relevance/linear in that universe would have you delete the structure when you're done. affine would still need the gc to help to know how to deal with something that was dropped, alternately you could maybe refine the notion of affine in that semiring to have versions that both
2020-09-17 05:55:32 <edwardk> supported unrestricted style dropping and ones that used an explicit finalizer to free like rust
2020-09-17 05:56:17 <edwardk> anything stuffed in a linear/relevant resource can get sort of freely added to some kind of gc root list, and you then don't even need to walk the relevant/linear stuff
2020-09-17 05:56:32 <edwardk> because you know it'll be consumed (and hence removed from the global gc root list) eventually
2020-09-17 05:56:51 <edwardk> this is a very resource-centric view, but one i've been playing with since i first found haskell
2020-09-17 05:57:02 <edwardk> qtt gave me the right framework, i was missing the + for the semiring
2020-09-17 05:58:10 <edwardk> now, this is still missing a last component, which is a notion of uniqueness, linearity says the consumer will definitely use up the thing, uniqueness says that you are being handed the only copy, and that the producer hasn't passed around any pointers to anybody else
2020-09-17 05:58:32 × lucid_0x80 quits (~lucid_0x8@188.253.232.35) (Quit: Leaving)
2020-09-17 05:58:41 <edwardk> but the quantitative type theory stuff basically doesn't prejudge too much what the semiring means
2020-09-17 05:58:45 <edwardk> it is more of a formal tool
2020-09-17 05:59:11 <edwardk> and your semantics then clears up what you mean, the choudhury et al paper at the end of the reading list i dumped is actually quite clear.
2020-09-17 05:59:23 <Axman6> topos: nibbleChar :: Word8 -> Word8; nibbleChar (W8# n) = W8# (int2Word# (word2Int# n +# (48# +# ((geWord# n 10##) *# 39#))))
2020-09-17 06:00:02 × jjj quits (~jjj@195.206.169.184) ()
2020-09-17 06:00:07 <siraben> edwardk: that is fascinating. do you have a repository for this?
2020-09-17 06:00:14 <edwardk> anyways my general problem is this for a _ in my toy type theory i usually drop in a meta variable.
2020-09-17 06:00:33 <edwardk> github.com/ekmett/haskell has been where i've been scribbling thoughts, but i don't have any of the qtt stuff committed yet, it breaks the whole toy
2020-09-17 06:00:56 × toorevitimirp quits (~tooreviti@117.182.182.33) (Ping timeout: 260 seconds)
2020-09-17 06:01:15 <Axman6> topos: using that makes converting it to work a word at a time "trivial"
2020-09-17 06:01:24 × merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 260 seconds)
2020-09-17 06:02:31 <edwardk> for a meta variable the way i handle it is i look around at all the locally bound variables where i created and placed the meta variable and i just build a meta variable that gets all those as arguments. \x y z. foo M -- where M could reference x y and z requires M to know about contexts, and is messy, so instead I make it \x y z. foo (M x y z). Now if M instantiates to a constant valued function that ignores its arguments, the
2020-09-17 06:02:31 <edwardk> normalization done by my unification engine gets me the answer i want.
2020-09-17 06:02:38 <edwardk> but here I don't know the usage data for M.
2020-09-17 06:02:42 <siraben> edwardk: this metavariable is not the same as a type variable?
2020-09-17 06:02:48 <edwardk> which mucks with my ability to do type inference
2020-09-17 06:02:52 → mmohammadi9812 joins (~mmohammad@5.116.223.123)
2020-09-17 06:03:12 <edwardk> meta variables here are like holes in the program. 'please put here the only thing that makes sense'
2020-09-17 06:03:36 <siraben> Oh, nice style for a repository. I might steal that, hehe. Maintaining separate repositories is annoying for small projects.
2020-09-17 06:03:53 <siraben> Right, I'm thinking of like Coq's metavariables then, ?A
2020-09-17 06:04:09 <edwardk> yeah. these are little existential holes
2020-09-17 06:04:13 <siraben> I use _ quite a lot when I want Coq to infer it
2020-09-17 06:04:32 <siraben> rewrite (mul_assoc _ b c)
2020-09-17 06:04:37 <edwardk> and they come up a bunch when you just write something like id :: {A} A -> A
2020-09-17 06:05:22 <siraben> Yes
2020-09-17 06:05:25 × hvr quits (~hvr@haskell/developer/hvr) (Ping timeout: 272 seconds)
2020-09-17 06:05:34 <edwardk> i have an implicit argument A there. great, but it really took id : {A : _} A -> A, and then when elaboration happened it expanded _ to a meta variable, and figured out that it should be 'type'
2020-09-17 06:05:35 × sfvm quits (~sfvm@37.228.215.148) (Quit: off to the basement, mixing up the medicine)
2020-09-17 06:06:19 <Axman6> topos: magic numbers in there are 48 = '0', 39 = 'a' - '0' - 10
2020-09-17 06:06:53 <edwardk> the general model is something like start out with a surface language with a bunch of extra nonsense and file locations and stuff in it, convert to some internal representation used for elaboration that has all these meta variables in it, then crush them out and you get the final 'core' equivalent.
2020-09-17 06:07:01 × heatsink quits (~heatsink@2600:1700:bef1:5e10:99ca:18ad:4e5f:ffdf) (Remote host closed the connection)
2020-09-17 06:07:34 → rihards joins (~rihards@balticom-142-78-50.balticom.lv)
2020-09-17 06:07:37 <edwardk> typechecking/inference produces terms in the elaboration form as witnesses that a given source term has a type
2020-09-17 06:07:46 <edwardk> but source terms have all sorts of extra bells and whistles.
2020-09-17 06:07:51 <edwardk> like in haskell we have where vs. let
2020-09-17 06:08:00 <edwardk> complex patterns, top level decls...
2020-09-17 06:08:37 → rapskalian joins (~user@2601:804:8400:5750:6d07:cb01:64a9:36bb)
2020-09-17 06:08:51 → knupfer joins (~Thunderbi@mue-88-130-61-060.dsl.tropolys.de)
2020-09-17 06:09:41 <edwardk> anyways, right now i'm currently wrestling with how to get resource usage constraints on each of my meta variables right, because _normally_ i can just sprinkle them around in my terms, but now i have a problem. their usage of resources affects how many resources i have to typecheck the _rest_ of the term.
2020-09-17 06:10:21 <edwardk> so i could try to carefully dance around and use up all the other resources and give them what is left, but i don't _really_ have a subtraction for resources (i'm in a semiring)
2020-09-17 06:10:43 <edwardk> i could also do something like first typecheck in the boring {0,1} presence/absence semiring, use that to flesh out my metas
2020-09-17 06:11:35 <edwardk> and then try to use backwards the fact that i have a semiring homomorphism from my final semiring to that semiring, and try to use that to 'redo' the job now that i actually have a sort of minimal bottom up chunk of resource usage data to go off
2020-09-17 06:11:49 → gnumonik joins (~gnumonik@c-73-170-91-210.hsd1.ca.comcast.net)
2020-09-17 06:12:04 <siraben> Hmm, seems tricky. I have no idea how semirings work when applied in a type theoretic context yet.
2020-09-17 06:12:19 → cole-h joins (~cole-h@c-73-48-197-220.hsd1.ca.comcast.net)
2020-09-17 06:13:11 <edwardk> if you look at https://richarde.dev/papers/2020/quantitative/quantitative.pdf in figure 1, the rule for ST-App is my bane
2020-09-17 06:13:21 × rapskalian quits (~user@2601:804:8400:5750:6d07:cb01:64a9:36bb) (Ping timeout: 244 seconds)
2020-09-17 06:13:52 → heatsink joins (~heatsink@2600:1700:bef1:5e10:b0dc:6c54:247b:ece)
2020-09-17 06:14:13 × shafox quits (~shafox@106.51.234.111) (Remote host closed the connection)
2020-09-17 06:14:34 → shafox joins (~shafox@106.51.234.111)
2020-09-17 06:14:59 <edwardk> because you have to infer the type of (f) in (f x), then use that to get the usage information for the application rule. but if f is a meta variable then we have no usage to use to fill in
2020-09-17 06:15:52 <edwardk> the fact that these judgments tend to be written in a style where it isn't clear how to infer rather than just check doesn't help the story
2020-09-17 06:15:58 <siraben> These typing rules don't seem to have meta variables, you added them?
2020-09-17 06:16:02 → dhouthoo joins (~dhouthoo@ptr-eiv6509pb4ifhdr9lsd.18120a2.ip6.access.telenet.be)
2020-09-17 06:16:09 <Axman6> anyone know of a tool which accepts assembly and can give you how much instruction level parallelism it might have?
2020-09-17 06:16:55 <siraben> I meant like, meta variables being part of the source language, not in the meta language used to describe the language (which does have meta variables)
2020-09-17 06:16:57 <edwardk> correct. because i need inference and inference wants to put little holes in various places. (also that type theory in that figure is non-dependent, and mine is dependently typed)
2020-09-17 06:17:12 × ChaiTRex quits (~ChaiTRex@gateway/tor-sasl/chaitrex) (Remote host closed the connection)
2020-09-17 06:17:18 <siraben> Have you thought about using bidirectional type inference?
2020-09-17 06:17:26 × ddere quits (uid110888@gateway/web/irccloud.com/x-hxjfplopujbdeyav) (Quit: Connection closed for inactivity)
2020-09-17 06:17:26 <siraben> That's a technique I learned recently, very useful.
2020-09-17 06:17:27 <edwardk> this is in a bidirectional type checker =)
2020-09-17 06:17:44 × mmohammadi9812 quits (~mmohammad@5.116.223.123) (Quit: I quit (╯°□°）╯︵ ┻━┻)
2020-09-17 06:17:48 <siraben> Where are the inferred vs. checked types then?
2020-09-17 06:17:50 × incognito9999 quits (~incognito@hwsrv-648981.hostwindsdns.com) (Ping timeout: 256 seconds)
←Prev  Next→
Page 1 .. 11 12 13 14 15 16 17 18 19 20 21 .. 5022

All times are in UTC.