Home freenode/#haskell: Logs Calendar

Logs: freenode/#haskell

←Prev  Next→
Page 1 .. 1396 1397 1398 1399 1400 1401 1402 1403 1404 1405 1406 .. 5022
— 502,152 events total
2020-11-20 04:22:47 ← iqubic parts (~user@2601:602:9500:4870:d13a:6a31:cf0a:f017) ("ERC (IRC client for Emacs 28.0.50)")
2020-11-20 04:22:55 <koz_> I guess I'm confused at the difference between the horizontal line and the turnstile.
2020-11-20 04:24:03 <monochrom> But the left of a turnstile is a very special kind of "assumptions".
2020-11-20 04:24:38 <monochrom> The left can only list the variables in scope, and their types.
2020-11-20 04:24:54 <koz_> Ah, so in a way, to the left of the turnstile we have a 'typing environment' basically?
2020-11-20 04:25:05 <monochrom> Yes, that's exactly it.
2020-11-20 04:25:13 <koz_> So what's with the big horizontal line?
2020-11-20 04:25:25 <monochrom> That one is really general implication.
2020-11-20 04:26:10 <koz_> Ah! I think I see it.
2020-11-20 04:26:32 <koz_> Since we have Gamma on the left of the top turnstile, with no mention of x, it means 'we can assume that every type has a kind'?
2020-11-20 04:26:46 <monochrom> or dividing a proof step into "before" and "after"
2020-11-20 04:27:56 × machinedgod quits (~machinedg@24.105.81.50) (Ping timeout: 260 seconds)
2020-11-20 04:27:56 <koz_> I guess I'm asking why this wasn't written as something like 'Gamma, x : A |- A : s, x : A'.
2020-11-20 04:28:30 <monochrom> Instead of "assume that a type has a kind", I think this rules is saying "in this system, a type has a kind".
2020-11-20 04:29:25 → sand_dull joins (~theuser@c-73-149-95-105.hsd1.ct.comcast.net)
2020-11-20 04:29:46 × hololeap quits (~hololeap@unaffiliated/hololeap) (Ping timeout: 256 seconds)
2020-11-20 04:30:15 <koz_> The rule is called 'var' if that helps any.
2020-11-20 04:30:32 → hololeap joins (~hololeap@unaffiliated/hololeap)
2020-11-20 04:35:30 hackage yi-keymap-cua 0.19.0 - Cua keymap for Yi editor https://hackage.haskell.org/package/yi-keymap-cua-0.19.0 (TomMurphy)
2020-11-20 04:36:37 <monochrom> A:s in a conclusion position is very different, in some sense opposite, of A:s in a prerequisite position.
2020-11-20 04:37:03 <koz_> Could you elaborate on that?
2020-11-20 04:38:43 <monochrom> I was hoping that you could use what you already know about the difference between "G implies P and Q" and "G and P implies Q"
2020-11-20 04:40:10 <monochrom> If you have a rule that says: "conclusion: x:monochrom |- monochrom is a legal type, and x:monochrom", then it defines that monochrom is a legal type.
2020-11-20 04:40:23 <monochrom> But if you don't have rule...
2020-11-20 04:40:46 → conal joins (~conal@ip-66-115-176-195.creativelink.net)
2020-11-20 04:40:48 × DirefulSalt quits (DirefulSal@gateway/vpn/privateinternetaccess/direfulsalt) (Remote host closed the connection)
2020-11-20 04:40:53 <monochrom> If you have, instead, "premise: monochrom is a type; conclusion: x:monochrom |- x:monochrom"
2020-11-20 04:41:17 <monochrom> now you still don't know whether monochrom is a type, and generally "expr : monochrom" has any chance of being legal at all.
2020-11-20 04:41:39 <monochrom> You will have to look for other rules to see if you can prove "monochrom is a type" or not.
2020-11-20 04:42:06 <koz_> Ah, I think I see what you're saying.
2020-11-20 04:42:15 <monochrom> If there is no, this means the system is trying to say "monochrom is not a legal type, you will never have anything of the form expr : monochrom"
2020-11-20 04:42:17 × howdoi quits (uid224@gateway/web/irccloud.com/x-dgisunxwmcstbixs) (Quit: Connection closed for inactivity)
2020-11-20 04:42:36 <koz_> Alright, thanks, that helps.
2020-11-20 04:42:49 <koz_> I keep forgetting that I need to become ten times stupider than I am as a human to properly read logic. :P
2020-11-20 04:42:55 → DirefulSalt joins (DirefulSal@gateway/vpn/privateinternetaccess/direfulsalt)
2020-11-20 04:43:05 <koz_> It's the optimist in me. 'Of course this is a type, what else could it possibly be?'.
2020-11-20 04:44:29 <monochrom> Some authors write a separate CFG to define legal types, and don't include this in the type checking rules.
2020-11-20 04:44:38 <koz_> These ones clearly didn't do that.
2020-11-20 04:44:58 <monochrom> Other authors use the type rules to define both legal types and type checking at the same time.
2020-11-20 04:44:58 <nshepperd> i think i would read that as saying that a typing environment containing x:A emits/proves that judgement (eg. so you can use it in other rules), but only if it also proves that A is a type
2020-11-20 04:45:01 hackage yi-dynamic-configuration 0.19.1 - Dynamic configuration support for Yi https://hackage.haskell.org/package/yi-dynamic-configuration-0.19.1 (TomMurphy)
2020-11-20 04:45:25 × quarters quits (~quarters@unaffiliated/quarters) (Ping timeout: 240 seconds)
2020-11-20 04:45:30 → rekahsoft joins (~rekahsoft@fitz10681.telemetry.esentire.com)
2020-11-20 04:47:31 <monochrom> Dependent typing is likely to mean legal types don't match any CFG, so it may be better to merge type forming rules with type checking rules, because the format allows you to add more restrictions.
2020-11-20 04:47:31 hackage yi-frontend-pango 0.19.1 - Pango frontend for Yi editor https://hackage.haskell.org/package/yi-frontend-pango-0.19.1 (TomMurphy)
2020-11-20 04:47:37 × falafel_ quits (~falafel@2601:547:1303:b30:7811:313f:d0f3:f9f4) (Remote host closed the connection)
2020-11-20 04:47:39 <nshepperd> if A is not a type, but instead instead a potato, then "Gamma, x:A" does not let you use x:A in further rules
2020-11-20 04:47:59 <nshepperd> (unless there's a separate rules that says so)
2020-11-20 04:48:12 → falafel_ joins (~falafel@2601:547:1303:b30:7811:313f:d0f3:f9f4)
2020-11-20 04:49:15 <koz_> Propositions as potatoes.
2020-11-20 04:49:23 <dolio> Proper variable scoping isn't context free, I believe.
2020-11-20 04:49:42 <dolio> So you're already screwed once you have variables.
2020-11-20 04:49:57 <monochrom> Oh heh yeah.
2020-11-20 04:51:06 <monochrom> http://www.vex.net/~trebla/weblog/declare-before-use.xhtml is my proof, at least of a related theorem.
2020-11-20 04:51:57 <monochrom> If it's just a few issues such as proper scoping standing in the way, we can make do with "fits this CFG plus has scoping requirements". Many authors do.
2020-11-20 04:52:11 <dolio> I worked on a project that tried to resolve variable scoping during parsing. I recommend not doing that.
2020-11-20 04:52:43 <monochrom> But dependent typing can have so many more unwiedly restrictions that you can't scale that style.
2020-11-20 04:53:07 <koz_> monochrom: That's a really cute proof using a technique I spent a lot of time with.
2020-11-20 04:53:18 × christo quits (~chris@81.96.113.213) (Remote host closed the connection)
2020-11-20 04:53:21 <koz_> (our whole ToC class consisted of assignments pumping damn near everything)
2020-11-20 04:57:16 <dolio> Yeah. Now I remember almost nothing about that part. :)
2020-11-20 04:58:10 <koz_> dolio: One particularly gory (non-pumping) question was about CE languages.
2020-11-20 04:58:22 <koz_> Like, all the questions around CE-ness were unpleasant, honestly.
2020-11-20 05:02:32 × avoandmayo quits (~textual@122-58-109-105-adsl.sparkbb.co.nz) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2020-11-20 05:04:32 × falafel_ quits (~falafel@2601:547:1303:b30:7811:313f:d0f3:f9f4) (Ping timeout: 260 seconds)
2020-11-20 05:04:56 × texasmynsted quits (~texasmyns@212.102.45.112) (Ping timeout: 240 seconds)
2020-11-20 05:07:35 → avoandmayo joins (~textual@122-58-109-105-adsl.sparkbb.co.nz)
2020-11-20 05:10:16 × avoandmayo quits (~textual@122-58-109-105-adsl.sparkbb.co.nz) (Client Quit)
2020-11-20 05:13:30 hackage yi 0.19.0 - Yi editor https://hackage.haskell.org/package/yi-0.19.0 (TomMurphy)
2020-11-20 05:23:27 → day_ joins (~Unknown@unaffiliated/day)
2020-11-20 05:23:45 × conal quits (~conal@ip-66-115-176-195.creativelink.net) (Quit: Computer has gone to sleep.)
2020-11-20 05:26:44 × day quits (~Unknown@unaffiliated/day) (Ping timeout: 260 seconds)
2020-11-20 05:26:44 day_ is now known as day
2020-11-20 05:28:04 → quarters joins (~quarters@38-73-246-124.starry-inc.net)
2020-11-20 05:31:07 → merijn joins (~merijn@83-160-49-249.ip.xs4all.nl)
2020-11-20 05:31:41 × Sarma quits (~Amras@unaffiliated/amras0000) (Remote host closed the connection)
2020-11-20 05:35:17 → Amras joins (~Amras@unaffiliated/amras0000)
2020-11-20 05:35:34 × merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 256 seconds)
2020-11-20 05:38:57 × borne quits (~fritjof@200116b8640a4d0024e67d79d03c01ac.dip.versatel-1u1.de) (Ping timeout: 260 seconds)
2020-11-20 05:40:53 → borne joins (~fritjof@200116b86455d000feb15fd2865dc87d.dip.versatel-1u1.de)
2020-11-20 05:40:58 × Codaraxis_ quits (~Codaraxis@ip68-5-90-227.oc.oc.cox.net) (Ping timeout: 260 seconds)
2020-11-20 05:42:14 × wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 272 seconds)
2020-11-20 05:42:52 × Rudd0 quits (~Rudd0@185.189.115.108) (Ping timeout: 272 seconds)
2020-11-20 05:46:05 × alx741 quits (~alx741@181.196.68.156) (Ping timeout: 240 seconds)
2020-11-20 05:47:07 × acidjnk_new2 quits (~acidjnk@p200300d0c719ff356dc4eeabe79b61ea.dip0.t-ipconnect.de) (Ping timeout: 260 seconds)
2020-11-20 05:47:12 → ggole joins (~ggole@2001:8003:8119:7200:3080:9a4e:22db:fd6d)
2020-11-20 05:47:22 → hooper joins (2fe3e53b@047-227-229-059.res.spectrum.com)
2020-11-20 05:50:01 <hooper> hi! i have a design question: so I want to have shapes like triangles and squares. they should both share some common attributes like having a number of sides and functions like computing the area, but would have different functions specific to each class as well
2020-11-20 05:50:05 × rekahsoft quits (~rekahsoft@fitz10681.telemetry.esentire.com) (Ping timeout: 260 seconds)
2020-11-20 05:50:08 <hooper> what is the best way to structure this?
2020-11-20 05:50:20 <hooper> I'm thinking a shape typeclass
2020-11-20 05:51:36 <hooper> but then not sure how to handle methods unique to one class
2020-11-20 05:51:39 <glguy> hooper, you can make a record like: data Polygon = Polygon { sides :: Int, Area :: Double, etc }
2020-11-20 05:52:22 <hooper> hm but i only want triangles and squares
2020-11-20 05:52:39 <glguy> OK, then: data Shape = Triangle | Square
2020-11-20 05:53:26 <hooper> so then lets say i declare like data Triangle = { a, b, c }
2020-11-20 05:53:35 <hooper> where a b c are Double type
2020-11-20 05:53:46 <hooper> how would I write an area function then
2020-11-20 05:54:40 <hooper> i need area to be polymorphic for square and triangle
2020-11-20 05:55:42 → wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net)
←Prev  Next→
Page 1 .. 1396 1397 1398 1399 1400 1401 1402 1403 1404 1405 1406 .. 5022

All times are in UTC.