Logs: liberachat/#haskell
| 2021-08-16 08:59:44 | × | Obo quits (~roberto@78.77.166.185) (Quit: WeeChat 2.8) |
| 2021-08-16 09:00:11 | <tomsmeding> | kuribas: if idris would get more libraries somehow, and compiler bugs get fixed, would that be a good enough language for you? I feel like dependently-typed languages are cool but actually proving anything non-trivial about realistic programs with them is still nigh impossible |
| 2021-08-16 09:00:42 | <tomsmeding> | not due to anything technical but just because we somehow don't know how to do that on a theory level, apparently |
| 2021-08-16 09:01:15 | <tomsmeding> | integrating SMT solvers is one good step in the right direction; I'm not sure how far that gets you nowadays in theorem proving |
| 2021-08-16 09:01:31 | <kuribas> | tomsmeding: yeah, I tried some proving in idris, and I found it not very practical. |
| 2021-08-16 09:01:43 | × | burnsidesLlama quits (~burnsides@dhcp168-025.wadham.ox.ac.uk) (Remote host closed the connection) |
| 2021-08-16 09:01:57 | <kuribas> | I'd use idris more for the type system programming, like type safe printf, servant like specifications, etc... |
| 2021-08-16 09:02:17 | → | burnsidesLlama joins (~burnsides@dhcp168-025.wadham.ox.ac.uk) |
| 2021-08-16 09:02:41 | <tomsmeding> | so, slightly stronger type-correctness-like properties |
| 2021-08-16 09:03:03 | <tomsmeding> | that's indeed probably what one can realistically expect of such languages today |
| 2021-08-16 09:03:48 | tomsmeding | needs to experiment with such things in idris or agda one day |
| 2021-08-16 09:04:11 | <kuribas> | tomsmeding: not just type correctness, type expressivity. |
| 2021-08-16 09:04:30 | <kuribas> | I just find that type level programming like in servant feels very ad-hoc in haskell. |
| 2021-08-16 09:04:39 | <kuribas> | Like coding in lisp :-) |
| 2021-08-16 09:04:44 | <tomsmeding> | right, but I was talking about the kind of properties that you want verified |
| 2021-08-16 09:05:10 | × | nsilv quits (~nsilv@host-79-17-175-58.retail.telecomitalia.it) (Ping timeout: 240 seconds) |
| 2021-08-16 09:05:15 | <tomsmeding> | "servant like specifications" still sounds like a type-correctness-like property to me, as distinct from a correctness property about program _behaviour_ |
| 2021-08-16 09:05:16 | <kuribas> | right |
| 2021-08-16 09:05:42 | <kuribas> | yeah, the idea is to prove that your implementation follows the spec, expressed as a type. |
| 2021-08-16 09:05:48 | <tomsmeding> | like, I wouldn't be able to give a rigorous definition of what is and isn't a property like that, but that's my feeling :p |
| 2021-08-16 09:06:20 | <tomsmeding> | session types fall into this category too, maybe? Though those move towards behaviour already |
| 2021-08-16 09:06:38 | × | burnsidesLlama quits (~burnsides@dhcp168-025.wadham.ox.ac.uk) (Remote host closed the connection) |
| 2021-08-16 09:06:45 | → | burnsidesLlama joins (~burnsides@dhcp168-025.wadham.ox.ac.uk) |
| 2021-08-16 09:06:58 | <tomsmeding> | (I agree about Haskell being quite ad-hoc for this) |
| 2021-08-16 09:08:32 | <tomsmeding> | perhaps some well-designed dep.typed language can use Csaba Hruska's work to use the GHC RTS by compiling to STG :p |
| 2021-08-16 09:09:56 | <kuribas> | idris has a GRIN backend... |
| 2021-08-16 09:10:11 | <tomsmeding> | ;p |
| 2021-08-16 09:10:21 | <tomsmeding> | I never have original ideas |
| 2021-08-16 09:11:33 | <lortabac> | another idea might be to invent a "pragmatic" standard library for Agda, less suited for proving and more for common engineering tasks |
| 2021-08-16 09:11:56 | <lortabac> | Agda is already mature and generates Haskell code |
| 2021-08-16 09:12:19 | <lortabac> | and it has a Haskell FFI |
| 2021-08-16 09:12:22 | <tomsmeding> | with sub-par performance because of the amount of unsafeCoerce generated, I hear |
| 2021-08-16 09:12:31 | <tomsmeding> | but true |
| 2021-08-16 09:14:10 | <lortabac> | tomsmeding: why is unsafeCoerce slow? |
| 2021-08-16 09:19:37 | → | peterhil joins (~peterhil@dsl-hkibng32-54fb52-57.dhcp.inet.fi) |
| 2021-08-16 09:19:55 | → | Gurkenglas joins (~Gurkengla@dslb-002-203-144-156.002.203.pools.vodafone-ip.de) |
| 2021-08-16 09:20:56 | → | timCF joins (~timCF@200-149-20-81.sta.estpak.ee) |
| 2021-08-16 09:23:49 | → | ubert joins (~Thunderbi@77.119.161.84.wireless.dyn.drei.com) |
| 2021-08-16 09:25:03 | <tomsmeding> | lortabac: I have that second-hand only: https://www.reddit.com/r/haskell/comments/ku1zsm/nextgen_haskell_compilation_techniques/gir7tzo/?context=3 (second paragraph) |
| 2021-08-16 09:25:15 | × | adam1 quits (~adam@2001-b011-4007-2996-b067-af20-17c7-8c20.dynamic-ip6.hinet.net) (Quit: WeeChat 3.2) |
| 2021-08-16 09:25:16 | → | pfurla joins (~pfurla@ool-3f8fcb0f.dyn.optonline.net) |
| 2021-08-16 09:28:10 | × | pfurla_ quits (~pfurla@ool-3f8fcb0f.dyn.optonline.net) (Ping timeout: 240 seconds) |
| 2021-08-16 09:29:05 | → | dschrempf joins (~dominik@92-249-159-252.pool.digikabel.hu) |
| 2021-08-16 09:34:52 | <lortabac> | tomsmeding: thanks |
| 2021-08-16 09:37:40 | <lortabac> | tomsmeding: anyway, it still takes less work to make Agda faster than to invent a whole new language |
| 2021-08-16 09:37:54 | <tomsmeding> | probably! |
| 2021-08-16 09:38:44 | <tomsmeding> | but I think kuribas wasn't necessarily aiming for a whole new language, just a language that satisfies certain properties -- be that a new one or an evolution of an existing one |
| 2021-08-16 09:39:01 | <kuribas> | indeed :) |
| 2021-08-16 09:42:38 | × | zfnmxt quits (~zfnmxtzfn@2001:470:69fc:105::2b32) (Changing host) |
| 2021-08-16 09:42:38 | → | zfnmxt joins (~zfnmxtzfn@user/zfnmxt) |
| 2021-08-16 09:43:10 | × | kayprish quits (~kayprish@cable-188-2-229-172.dynamic.sbb.rs) (Ping timeout: 240 seconds) |
| 2021-08-16 09:46:09 | → | __monty__ joins (~toonn@user/toonn) |
| 2021-08-16 09:46:45 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Quit: WeeChat 3.2) |
| 2021-08-16 09:49:17 | <kuribas> | Or just fleshing out one language, cleaning up the modules, adding common packages (csv, database, etc...). |
| 2021-08-16 09:50:14 | × | timCF quits (~timCF@200-149-20-81.sta.estpak.ee) (Quit: leaving) |
| 2021-08-16 09:50:26 | → | raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 2021-08-16 09:52:11 | → | nsilv joins (~nsilv@host-79-17-175-58.retail.telecomitalia.it) |
| 2021-08-16 09:52:18 | <kuribas> | lortabac: is proving in agda more ergonomic that in idris? |
| 2021-08-16 09:52:23 | × | zfnmxt quits (~zfnmxtzfn@user/zfnmxt) (Quit: Reconnecting) |
| 2021-08-16 09:52:30 | <tomsmeding> | "cleaning up the modules" -- if you manage in the chorus of "don't break my 10-year old code" |
| 2021-08-16 09:52:37 | → | zfnmxt joins (~zfnmxtzfn@2001:470:69fc:105::2b32) |
| 2021-08-16 09:52:49 | <kuribas> | like, does it have an IDE which helps visualising proofs, can it automate some proofs? |
| 2021-08-16 09:53:09 | <lortabac> | kuribas: I am not a mathematician, but as far as I know Agda is mostly for proving |
| 2021-08-16 09:53:14 | × | econo quits (uid147250@user/econo) (Quit: Connection closed for inactivity) |
| 2021-08-16 09:53:23 | <lortabac> | but you are more or less forced to use emacs |
| 2021-08-16 09:53:32 | → | Guest64 joins (~Guest64@185.133.181.17) |
| 2021-08-16 09:53:34 | <kuribas> | emacs is fine for me :) |
| 2021-08-16 09:53:45 | <lortabac> | from what I hear, Agda without emacs is almost unusable |
| 2021-08-16 09:54:09 | <tomsmeding> | vim works somewhat, for a _very_ lenient interpretation of somewhat |
| 2021-08-16 09:54:58 | <lortabac> | tomsmeding: I've never managed to make the vim plugin work |
| 2021-08-16 09:55:17 | <lortabac> | but my experience with Agda is just a couple of weekends |
| 2021-08-16 09:55:20 | <tomsmeding> | it's been a while, but it worked for me a few years ago |
| 2021-08-16 09:55:31 | <tomsmeding> | my experience is a uni course :D |
| 2021-08-16 09:58:35 | → | eggplantade joins (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 2021-08-16 09:58:51 | <lortabac> | coming back to my idea of making a "pragmatic Agda"... if someone manages to integrate Agda with GHC (similarly to what has been done for liquid-haskell) there is hope to reuse cabal/hackage infrastructure |
| 2021-08-16 10:00:29 | <lortabac> | but I'm just brainstorming, I don't know if this makes sense |
| 2021-08-16 10:02:57 | × | eggplantade quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 245 seconds) |
| 2021-08-16 10:03:57 | jehugawa | is now known as JeHugawa |
| 2021-08-16 10:04:10 | × | nsilv quits (~nsilv@host-79-17-175-58.retail.telecomitalia.it) (Ping timeout: 240 seconds) |
| 2021-08-16 10:07:25 | × | wootehfoot quits (~wootehfoo@user/wootehfoot) (Ping timeout: 258 seconds) |
| 2021-08-16 10:08:04 | × | Guest64 quits (~Guest64@185.133.181.17) (Ping timeout: 246 seconds) |
| 2021-08-16 10:12:46 | → | acidjnk_new3 joins (~acidjnk@p200300d0c72b9586fc3405b671925cb2.dip0.t-ipconnect.de) |
| 2021-08-16 10:14:28 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 268 seconds) |
| 2021-08-16 10:15:19 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-08-16 10:15:52 | × | acidjnk_new quits (~acidjnk@p200300d0c72b9503f052fac21b551e32.dip0.t-ipconnect.de) (Ping timeout: 245 seconds) |
| 2021-08-16 10:16:23 | <tomsmeding> | I doubt Agda can be integrated in GHC like liquid haskell is, it being quite a larger departure from Haskell than a, well, addon to Haskell :p |
| 2021-08-16 10:17:08 | <tomsmeding> | but maybe on a lower level, where agda compiles to STG and cabal gets support for calling agda or something |
| 2021-08-16 10:17:10 | × | slavaqq quits (~slavaqq@sdmail.sdserver.cz) (Ping timeout: 246 seconds) |
| 2021-08-16 10:17:21 | <__monty__> | I don't see why it needs to be integrated in GHC at all to make use of hackage. |
| 2021-08-16 10:20:28 | × | jtomas quits (~jtomas@233.red-83-34-2.dynamicip.rima-tde.net) (Remote host closed the connection) |
| 2021-08-16 10:20:40 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds) |
| 2021-08-16 10:21:04 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-08-16 10:23:17 | → | oxide joins (~lambda@user/oxide) |
| 2021-08-16 10:24:49 | → | thyriaen joins (~thyriaen@dynamic-078-054-183-239.78.54.pool.telefonica.de) |
| 2021-08-16 10:26:17 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 245 seconds) |
| 2021-08-16 10:26:35 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-08-16 10:34:11 | × | dextaa quits (~DV@user/dextaa) (Ping timeout: 268 seconds) |
| 2021-08-16 10:35:53 | → | wonko joins (~wjc@62.115.229.50) |
| 2021-08-16 10:37:01 | haritzondo | is now known as haritz |
| 2021-08-16 10:37:01 | × | haritz quits (~hrtz@62.3.70.206) (Changing host) |
All times are in UTC.