Logs: liberachat/#haskell
| 2021-05-27 21:54:10 | × | ddellac__ quits (~ddellacos@89.46.62.31) (Ping timeout: 264 seconds) |
| 2021-05-27 21:55:22 | × | pe200012 quits (~pe200012@119.131.208.84) (Ping timeout: 264 seconds) |
| 2021-05-27 21:55:41 | → | pe200012 joins (~pe200012@119.131.208.84) |
| 2021-05-27 21:55:55 | × | rahguzar quits (~rahguzar@dynamic-adsl-84-220-228-254.clienti.tiscali.it) (Quit: Client closed) |
| 2021-05-27 21:56:39 | <monochrom> | You may like to know that the word "schema" can carry connotation about how instantiation is achieved, not just that it is allowed. |
| 2021-05-27 21:57:37 | <monochrom> | So for example suppose you try to state induction in first-order logic. It's first-order so you can't start with "for all predicate p". |
| 2021-05-27 21:57:48 | → | wagle joins (~wagle@quassel.wagle.io) |
| 2021-05-27 21:58:49 | <monochrom> | The workaround is you move that forall to the meta level. You say: for every predicate p, this sentence is an axiom: "p(0) and (forall n. p(n) implies p(n+1)) implies (forall n. p(n))" |
| 2021-05-27 21:59:34 | × | tanner_ quits (~tanner@74.221.100.239) (Ping timeout: 264 seconds) |
| 2021-05-27 21:59:36 | <monochrom> | In addition you actually don't want to commit to the stance "I have infinitely many axioms". Every proof should use only finitely many axioms. |
| 2021-05-27 22:00:16 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 264 seconds) |
| 2021-05-27 22:00:23 | <davean> | monochrom: if i have infinite many axioms, do I get to choose from them? |
| 2021-05-27 22:00:32 | <monochrom> | So they call their approach "axiom schema", and the intention is to instantiate it on demand, instantiate only what you need. |
| 2021-05-27 22:01:57 | <monochrom> | As opposed to in higher-order logic, you just add one axiom, and it goes "forall p. ...", and it's instantiated inside the logic, not at the meta level. |
| 2021-05-27 22:02:33 | <monochrom> | So "schema" carries the connotation that you instantiate at a meta level, and I would associate it with how C++ does it. |
| 2021-05-27 22:02:58 | → | Guest2998 joins (~Guest29@212095008205.public.telering.at) |
| 2021-05-27 22:05:04 | × | mikoto-chan quits (~mikoto-ch@ip-213-49-189-31.dsl.scarlet.be) (Ping timeout: 264 seconds) |
| 2021-05-27 22:05:04 | × | Guest2998 quits (~Guest29@212095008205.public.telering.at) (Client Quit) |
| 2021-05-27 22:05:10 | × | Raito_Bezarius quits (~Raito@user/raito-bezarius/x-8759638) (Changing host) |
| 2021-05-27 22:05:10 | → | Raito_Bezarius joins (~Raito@wireguard/tunneler/raito-bezarius) |
| 2021-05-27 22:05:39 | → | ku joins (~ku@2601:280:c780:7ea0:40a4:e850:40ff:b5e) |
| 2021-05-27 22:07:04 | × | gehmehgeh quits (~user@user/gehmehgeh) (Quit: Leaving) |
| 2021-05-27 22:08:40 | × | MasterControl quits (~Master@238.140.4.85.dynamic.wline.res.cust.swisscom.ch) (Remote host closed the connection) |
| 2021-05-27 22:08:58 | → | MasterControl joins (~Master@238.140.4.85.dynamic.wline.res.cust.swisscom.ch) |
| 2021-05-27 22:10:23 | × | python476 quits (~user@88.160.31.174) (Ping timeout: 272 seconds) |
| 2021-05-27 22:10:27 | → | slack1256 joins (~slack1256@181.203.105.152) |
| 2021-05-27 22:12:37 | → | fizbin joins (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) |
| 2021-05-27 22:17:34 | × | fizbin quits (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Ping timeout: 264 seconds) |
| 2021-05-27 22:18:52 | × | spirgel_ quits (spirgel@gateway/vpn/protonvpn/spirgel) (Remote host closed the connection) |
| 2021-05-27 22:19:20 | <ski> | yes, and this parallels inferring a type schema, for an expfression/term in the simply-typed lambda calculus. the `forall' is on the meta-level |
| 2021-05-27 22:19:40 | × | michalz quits (~user@185.246.204.60) (Remote host closed the connection) |
| 2021-05-27 22:20:19 | × | ku quits (~ku@2601:280:c780:7ea0:40a4:e850:40ff:b5e) (Ping timeout: 272 seconds) |
| 2021-05-27 22:20:38 | × | dut quits (~dut@user/dut) (Ping timeout: 252 seconds) |
| 2021-05-27 22:22:43 | <ski> | you interpret `\ f. \ x. f x x : (alpha -> (alpha -> beta)) -> (alpha -> beta)' as claiming that for every actual two types (iow with no variables in them) we replace the schematic / meta variables `alpha' and `beta' with, the given term (`\ f. \ x. f x x') can be assigned the resulting type (with no variables left) |
| 2021-05-27 22:23:25 | → | Guest11 joins (~textual@146.212.240.255) |
| 2021-05-27 22:24:08 | <ski> | then you can compare this with `reverse :: [a] -> [a]', or `map :: (a -> b) -> ([a] -> [b])', in Haskell |
| 2021-05-27 22:24:56 | × | ego quits (~egoist@186.235.82.52) (Quit: WeeChat 3.1) |
| 2021-05-27 22:27:47 | × | geekosaur quits (~geekosaur@069-135-003-034.biz.spectrum.com) (Remote host closed the connection) |
| 2021-05-27 22:28:07 | → | peddie joins (~peddie@static-198-54-129-62.cust.tzulo.com) |
| 2021-05-27 22:28:54 | ← | peddie parts (~peddie@static-198-54-129-62.cust.tzulo.com) () |
| 2021-05-27 22:29:42 | → | geekosaur joins (~geekosaur@069-135-003-034.biz.spectrum.com) |
| 2021-05-27 22:30:09 | × | nsilv quits (~nsilv@host-82-50-119-12.retail.telecomitalia.it) (Quit: WeeChat 2.8) |
| 2021-05-27 22:32:42 | → | cdsmithus joins (~cdsmithus@c-73-184-127-183.hsd1.ga.comcast.net) |
| 2021-05-27 22:33:13 | × | meltedbrain_y2k quits (~tekserf@31.4.247.19) (Quit: Leaving.) |
| 2021-05-27 22:33:30 | × | cdsmithus quits (~cdsmithus@c-73-184-127-183.hsd1.ga.comcast.net) (Read error: Connection reset by peer) |
| 2021-05-27 22:34:55 | → | spirgel joins (spirgel@gateway/vpn/protonvpn/spirgel) |
| 2021-05-27 22:36:49 | → | vicfred joins (~vicfred@user/vicfred) |
| 2021-05-27 22:36:54 | × | ccntrq quits (~ccntrq@dynamic-077-008-079-078.77.8.pool.telefonica.de) (Ping timeout: 264 seconds) |
| 2021-05-27 22:37:00 | × | wagle quits (~wagle@quassel.wagle.io) (Ping timeout: 265 seconds) |
| 2021-05-27 22:37:35 | → | Guest22 joins (~Guest22@umbreller.kvi.sgsnet.se) |
| 2021-05-27 22:38:16 | → | wagle joins (~wagle@quassel.wagle.io) |
| 2021-05-27 22:41:28 | Guest22 | is now known as typesafety |
| 2021-05-27 22:41:33 | <boxscape> | oh, wow, in HEAD you can have actual `String`s, i.e. [Char], on the type level |
| 2021-05-27 22:41:41 | <boxscape> | they're still distinct from Symbol though |
| 2021-05-27 22:41:45 | <safinaskar> | monochrom: "such that the only kinds are * and *^n -> *, such as Java and C++" - c++ allows quite complicated kinds. for example, one could write "template <template <typename> typename T> class X { ... }". this means "data X (T :: * -> *) = ...", i. e. X will have kind ((* -> *) -> *) |
| 2021-05-27 22:43:45 | <boxscape> | hmm looking at the merge request it might even be in a released ghc version |
| 2021-05-27 22:44:10 | → | fizbin joins (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) |
| 2021-05-27 22:45:25 | <safinaskar> | monochrom: also, in c++20 we can pass compile-time struct values as template parameters, this can be used to implement very ugly ad hoc theorem checker in type-level compilation-type c++, similary to how this is possible in type-level haskell |
| 2021-05-27 22:45:50 | <safinaskar> | monochrom: type system of c++ is quite complicated |
| 2021-05-27 22:46:04 | ← | safinaskar parts (~user@109.252.90.89) () |
| 2021-05-27 22:48:05 | × | ddellacosta quits (~ddellacos@89.46.62.25) (Remote host closed the connection) |
| 2021-05-27 22:48:34 | → | ddellacosta joins (~ddellacos@89.46.62.25) |
| 2021-05-27 22:48:59 | × | typesafety quits (~Guest22@umbreller.kvi.sgsnet.se) (Quit: Client closed) |
| 2021-05-27 22:49:01 | × | fizbin quits (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Ping timeout: 272 seconds) |
| 2021-05-27 22:49:26 | × | favonia quits (~favonia@user/favonia) (Ping timeout: 244 seconds) |
| 2021-05-27 22:49:31 | × | MasterControl quits (~Master@238.140.4.85.dynamic.wline.res.cust.swisscom.ch) (Remote host closed the connection) |
| 2021-05-27 22:49:47 | → | MasterControl joins (~Master@238.140.4.85.dynamic.wline.res.cust.swisscom.ch) |
| 2021-05-27 22:50:08 | → | favonia joins (~favonia@user/favonia) |
| 2021-05-27 22:50:38 | × | ddellacosta quits (~ddellacos@89.46.62.25) (Read error: Connection reset by peer) |
| 2021-05-27 22:51:42 | × | haskman quits (~haskman@106.212.143.206) (Quit: Going to sleep. ZZZzzz…) |
| 2021-05-27 22:51:54 | × | zeenk quits (~zeenk@2a02:2f04:a310:b600:b098:bf18:df4d:4c41) (Quit: Konversation terminated!) |
| 2021-05-27 22:53:26 | → | xwx joins (~george@user/george) |
| 2021-05-27 22:54:00 | → | chisui joins (~chisui@200116b8663f48001b1ac13283537396.dip.versatel-1u1.de) |
| 2021-05-27 22:55:28 | × | chisui quits (~chisui@200116b8663f48001b1ac13283537396.dip.versatel-1u1.de) (Client Quit) |
| 2021-05-27 22:55:32 | × | sm[m] quits (~sm@plaintextaccounting/sm) (Quit: node-irc says goodbye) |
| 2021-05-27 22:55:43 | → | chisui joins (~chisui@200116b8663f48001b1ac13283537396.dip.versatel-1u1.de) |
| 2021-05-27 22:55:48 | → | sm[m] joins (~sm@plaintextaccounting/sm) |
| 2021-05-27 22:57:20 | → | kline joins (~freedom0@libera/staff/kline) |
| 2021-05-27 22:57:37 | → | allbery_b joins (~geekosaur@069-135-003-034.biz.spectrum.com) |
| 2021-05-27 22:57:44 | ← | kline parts (~freedom0@libera/staff/kline) (*.bannana *.split) |
| 2021-05-27 22:57:50 | → | tonyday joins (~user@202-65-93-249.ip4.superloop.com) |
| 2021-05-27 22:58:37 | <chisui> | Hey, is there a special name for categories that have `a -> (a, a)` for all `a`? |
| 2021-05-27 22:59:22 | <dolio> | If (a, a) means product, then every category with products has that. |
| 2021-05-27 22:59:56 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 2021-05-27 23:00:39 | → | dy joins (~dy@user/dy) |
| 2021-05-27 23:00:41 | <tonyday> | Hello haskellers, how would I programmatically get core for a particular function, or just all of core if that's too hard? |
| 2021-05-27 23:00:47 | × | geekosaur quits (~geekosaur@069-135-003-034.biz.spectrum.com) (Ping timeout: 252 seconds) |
| 2021-05-27 23:01:18 | <boxscape> | tonyday -ddump-simpl |
| 2021-05-27 23:02:30 | <chisui> | dolio: Yes, sorry I meant Product. Thank you, after looking again it's kind of in the Definition. |
| 2021-05-27 23:02:32 | <tonyday> | thx, and if I'm sitting inside a haskell program, analysing some code? |
| 2021-05-27 23:02:55 | <monochrom> | No. |
| 2021-05-27 23:03:09 | <boxscape> | (I overread the "programmatically" part I think) |
| 2021-05-27 23:03:19 | → | bilegeek joins (~bilegeek@2600:1008:b01a:69cf:a58b:76f2:71:1386) |
| 2021-05-27 23:03:29 | <boxscape> | (and by overread I mean "missed") |
| 2021-05-27 23:04:08 | → | pe200012_ joins (~pe200012@218.107.17.245) |
| 2021-05-27 23:04:24 | × | boxscape quits (~boxscape@user/boxscape) (Quit: Connection closed) |
| 2021-05-27 23:04:33 | <tonyday> | I dont even know if it's a thing. But I'd like to add the core for a function as a comment above the function itself. |
| 2021-05-27 23:04:39 | × | pe200012 quits (~pe200012@119.131.208.84) (Ping timeout: 272 seconds) |
| 2021-05-27 23:05:03 | <monochrom> | Manual copy-paste. |
| 2021-05-27 23:05:48 | <tonyday> | Yep, that's what I'm doing now - just getting bored! |
All times are in UTC.