Logs: liberachat/#haskell
| 2021-06-30 19:14:18 | <safinaskar> | i can easily write axiomatization, say, for whole ZFC as a single GADT |
| 2021-06-30 19:14:51 | × | listofoptions quits (~haha@nat.syssrc.com) (Read error: Connection reset by peer) |
| 2021-06-30 19:15:02 | × | derelict quits (~derelict@user/derelict) (Ping timeout: 256 seconds) |
| 2021-06-30 19:15:36 | <Cale> | I don't think GADTs give you everything you might want there, but they're closer to being able to specify that kind of thing than plain algebraic data types certainly. |
| 2021-06-30 19:16:18 | <Cale> | In particular, you're missing out on quantifiers that you're probably going to want at some point |
| 2021-06-30 19:16:35 | <Cale> | But that's just Haskell's lack of Pi and Sigma types |
| 2021-06-30 19:16:49 | → | Deide joins (~Deide@user/deide) |
| 2021-06-30 19:17:20 | <boxscape> | Cale: but GADTs allow you to write singletons |
| 2021-06-30 19:17:38 | <Cale> | But yeah, in Coq and Agda, they regularly define various classes of propositions as inductive datatypes |
| 2021-06-30 19:17:45 | <Cale> | (and Idris as well) |
| 2021-06-30 19:17:56 | <safinaskar> | i can write ZFC axiomatization using GADTs only. without code. and without advanced haskell features, such as singletons |
| 2021-06-30 19:18:25 | <safinaskar> | you just need to have explicit proofs of substitutions |
| 2021-06-30 19:18:32 | <Cale> | Can you? Have a gist or something I can look at? |
| 2021-06-30 19:18:53 | <safinaskar> | i. e. propositions like "A is B with C substituted for x" are provable propositions on its own |
| 2021-06-30 19:19:42 | <safinaskar> | Cale: yes, i can. give me 10 minutes, i hope i will write |
| 2021-06-30 19:19:56 | <dsal> | I've still never actually used GADTs (I think). Every time I've thought it'd help me, it made things worse. |
| 2021-06-30 19:20:27 | → | acarrico joins (~acarrico@dhcp-68-142-39-249.greenmountainaccess.net) |
| 2021-06-30 19:21:16 | × | favonia quits (~favonia@user/favonia) (Ping timeout: 256 seconds) |
| 2021-06-30 19:21:37 | → | favonia joins (~favonia@user/favonia) |
| 2021-06-30 19:22:53 | → | Morrow joins (~MorrowM_@147.161.13.35) |
| 2021-06-30 19:24:25 | <Cale> | A practical place to use GADTs is for encoding protocols, where you use the index type as a way to express what type of response you expect back |
| 2021-06-30 19:25:14 | × | acarrico quits (~acarrico@dhcp-68-142-39-249.greenmountainaccess.net) (Ping timeout: 256 seconds) |
| 2021-06-30 19:25:15 | <Cale> | Also, I've had a fairly good time using fairly simple GADTs alongside DMap for a sort of extensible records. |
| 2021-06-30 19:25:58 | <Cale> | The terms of your GADT become the "field labels" and the index type is the type of the corresponding field. |
| 2021-06-30 19:26:55 | → | acarrico joins (~acarrico@dhcp-68-142-39-249.greenmountainaccess.net) |
| 2021-06-30 19:28:16 | <Cale> | Unlike most systems of extensible records, you don't get type-level information about which fields are present in a record, but you *do* get information about which "universe" of fields they come from, and lots of nice operations (effectively parallels to most of Data.Map) |
| 2021-06-30 19:29:36 | → | falafel joins (~falafel@pool-96-255-70-50.washdc.fios.verizon.net) |
| 2021-06-30 19:33:00 | <safinaskar> | (i am still writing that GADT) |
| 2021-06-30 19:35:52 | → | Pickchea joins (~private@user/pickchea) |
| 2021-06-30 19:37:30 | × | geekosaur quits (~geekosaur@xmonad/geekosaur) (Ping timeout: 240 seconds) |
| 2021-06-30 19:37:40 | × | chisui quits (~chisui@200116b868342600e075ba151a671095.dip.versatel-1u1.de) (Ping timeout: 246 seconds) |
| 2021-06-30 19:38:08 | → | derelict joins (~derelict@user/derelict) |
| 2021-06-30 19:40:42 | × | favonia quits (~favonia@user/favonia) (Ping timeout: 240 seconds) |
| 2021-06-30 19:41:07 | → | favonia joins (~favonia@user/favonia) |
| 2021-06-30 19:41:47 | × | johnw quits (~johnw@76-234-69-149.lightspeed.frokca.sbcglobal.net) (Quit: ZNC - http://znc.in) |
| 2021-06-30 19:43:06 | → | geekosaur joins (~geekosaur@xmonad/geekosaur) |
| 2021-06-30 19:45:09 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:dc49:b28b:5485:3e7e) (Remote host closed the connection) |
| 2021-06-30 19:46:01 | → | Codaraxis_ joins (~Codaraxis@ip68-5-90-227.oc.oc.cox.net) |
| 2021-06-30 19:47:13 | → | amahl joins (~amahl@dsl-jklbng12-54fbca-64.dhcp.inet.fi) |
| 2021-06-30 19:47:58 | → | waleee joins (~waleee@2001:9b0:216:8200:d457:9189:7843:1dbd) |
| 2021-06-30 19:50:00 | × | Codaraxis quits (~Codaraxis@user/codaraxis) (Ping timeout: 272 seconds) |
| 2021-06-30 19:59:06 | <safinaskar> | Cale: i am writing, and i already wrote definition of first order logic. i hope you are still interested |
| 2021-06-30 20:02:19 | <Cale> | sure |
| 2021-06-30 20:02:49 | → | tromp joins (~textual@dhcp-077-249-230-040.chello.nl) |
| 2021-06-30 20:02:52 | <Cale> | What do you do with respect to quantifiers? |
| 2021-06-30 20:02:55 | → | Bob_Esponja joins (~Bob_Espon@175.red-79-156-90.staticip.rima-tde.net) |
| 2021-06-30 20:02:55 | × | sm2n quits (~sm2n@user/sm2n) (Read error: Connection reset by peer) |
| 2021-06-30 20:02:57 | × | Bob_Esponja quits (~Bob_Espon@175.red-79-156-90.staticip.rima-tde.net) (Client Quit) |
| 2021-06-30 20:03:17 | → | sm2n joins (~sm2n@user/sm2n) |
| 2021-06-30 20:05:03 | × | unyu quits (~pyon@user/pyon) (Ping timeout: 268 seconds) |
| 2021-06-30 20:05:26 | × | juhp quits (~juhp@128.106.188.66) (Ping timeout: 252 seconds) |
| 2021-06-30 20:06:56 | → | dextaa joins (~DV@aftr-37-201-214-197.unity-media.net) |
| 2021-06-30 20:06:57 | → | unyu joins (~pyon@user/pyon) |
| 2021-06-30 20:07:10 | → | juhp joins (~juhp@128.106.188.66) |
| 2021-06-30 20:09:02 | → | cheater1__ joins (~Username@user/cheater) |
| 2021-06-30 20:09:14 | × | cheater quits (~Username@user/cheater) (Ping timeout: 272 seconds) |
| 2021-06-30 20:09:15 | cheater1__ | is now known as cheater |
| 2021-06-30 20:11:14 | × | falafel quits (~falafel@pool-96-255-70-50.washdc.fios.verizon.net) (Ping timeout: 265 seconds) |
| 2021-06-30 20:13:11 | × | _ht quits (~quassel@82-169-194-8.biz.kpn.net) (Remote host closed the connection) |
| 2021-06-30 20:14:51 | <safinaskar> | look everybody! ZFC as single GADT! https://paste.debian.net/1202948/ |
| 2021-06-30 20:15:38 | <safinaskar> | Cale: ping. quantifiers exists in my language as usual. i use explicit proof objects of type "Subst", this proof objects proofs that substitutions are possible |
| 2021-06-30 20:16:05 | <safinaskar> | s/proof objects proofs that/proof objects prove that/ |
| 2021-06-30 20:21:59 | × | norias quits (~jaredm@c-98-219-195-163.hsd1.pa.comcast.net) (Ping timeout: 268 seconds) |
| 2021-06-30 20:22:43 | <Cale> | safinaskar: Ahh, that is interesting |
| 2021-06-30 20:22:46 | <Cale> | hmm |
| 2021-06-30 20:23:39 | × | takuan quits (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection) |
| 2021-06-30 20:24:10 | × | favonia quits (~favonia@user/favonia) (Ping timeout: 256 seconds) |
| 2021-06-30 20:24:28 | → | favonia joins (~favonia@user/favonia) |
| 2021-06-30 20:25:15 | <Cale> | safinaskar: Yeah, that's a deeper embedding than I was thinking of :) |
| 2021-06-30 20:25:46 | <tomsmeding> | I think people seldomly explicitly list the axioms of the theory when trying stuff like this; generally I think people want to model type theory using the rules already in the type system |
| 2021-06-30 20:26:09 | <tomsmeding> | and then you run into trouble where a non-dependent type system isn't strong enough to handle forall |
| 2021-06-30 20:26:19 | <Cale> | But yeah, this gives a logic which you wouldn't normally get as a type theory, even |
| 2021-06-30 20:26:34 | <Cale> | Note the double negation elimination, for example |
| 2021-06-30 20:26:44 | → | cloudy` joins (~user@2600:8807:c207:f00:d022:dd81:f0f8:bb22) |
| 2021-06-30 20:27:46 | <safinaskar> | so, are there posts about this? |
| 2021-06-30 20:30:25 | <safinaskar> | are there some articles/theories about all possible logics? for example, i want some definition of what it is mean to be syntax-directed for logic |
| 2021-06-30 20:30:30 | <tomsmeding> | I'm not aware of significant work in this direction (only people using type theory in dependent languages, or when they want to work in different logics, designing a new language to let them work in that theory -- e.g. adding aximos to Coq) |
| 2021-06-30 20:30:52 | <Cale> | Somehow I'd be surprised if nobody had ever written something like this in Coq |
| 2021-06-30 20:31:02 | <tomsmeding> | but that doesn't say that there isn't such work, and that _especially_ doesn't mean that there haven't been isolated people trying this before :) |
| 2021-06-30 20:31:05 | <Cale> | But I'm not sure exactly where to look for it :) |
| 2021-06-30 20:31:06 | <tomsmeding> | yes |
| 2021-06-30 20:31:10 | <dolio> | Yeah, this is pretty basic stuff in lots of proof assistants. |
| 2021-06-30 20:31:17 | <safinaskar> | Cale: i just have read that coq has no GADTs |
| 2021-06-30 20:31:21 | <safinaskar> | Cale: but agda has |
| 2021-06-30 20:31:32 | <safinaskar> | Cale: and my code is trivially convertible to agda |
| 2021-06-30 20:31:37 | → | motherfsck joins (~motherfsc@user/motherfsck) |
| 2021-06-30 20:31:39 | <Cale> | safinaskar: Coq has inductive data types, which are basically like GADTs |
| 2021-06-30 20:32:49 | <safinaskar> | maybe there is some provers, which can take logic in similar form and check some its properties? |
| 2021-06-30 20:33:25 | <safinaskar> | somebody on this channel already pointed me to twelf. i will check it. are there other links? |
| 2021-06-30 20:33:51 | <safinaskar> | my method lets me define my own notion of substitution, alpha-beta-equivalency, etc |
| 2021-06-30 20:34:56 | × | MQ-17J quits (~MQ-17J@8.21.10.15) (Ping timeout: 256 seconds) |
| 2021-06-30 20:35:12 | → | MQ-17J joins (~MQ-17J@d14-69-206-129.try.wideopenwest.com) |
| 2021-06-30 20:36:58 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-06-30 20:39:51 | → | falafel joins (~falafel@pool-96-255-70-50.washdc.fios.verizon.net) |
| 2021-06-30 20:45:33 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:dc49:b28b:5485:3e7e) |
| 2021-06-30 20:46:42 | × | favonia quits (~favonia@user/favonia) (Ping timeout: 240 seconds) |
| 2021-06-30 20:47:33 | × | nshepperd2 quits (~nshepperd@li364-218.members.linode.com) (Remote host closed the connection) |
| 2021-06-30 20:47:45 | → | nshepperd2 joins (~nshepperd@li364-218.members.linode.com) |
| 2021-06-30 20:49:06 | × | Reyu[M] quits (~reyureyuz@matrix.reyuzenfold.com) (Ping timeout: 256 seconds) |
| 2021-06-30 20:49:17 | → | favonia joins (~favonia@user/favonia) |
All times are in UTC.