Logs: liberachat/#haskell
| 2021-06-22 16:55:54 | × | Erutuon quits (~Erutuon@user/erutuon) (Quit: WeeChat 2.8) |
| 2021-06-22 16:56:50 | × | Topsi1 quits (~Tobias@dyndsl-095-033-016-151.ewe-ip-backbone.de) (Read error: Connection reset by peer) |
| 2021-06-22 16:58:43 | → | ph88 joins (~ph88@2a02:8109:9e00:7e5c:7c55:3c65:74e1:3dc5) |
| 2021-06-22 16:58:45 | × | justBull quits (~justache@user/justache) (Remote host closed the connection) |
| 2021-06-22 16:59:07 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 268 seconds) |
| 2021-06-22 16:59:58 | → | justBull joins (~justache@user/justache) |
| 2021-06-22 16:59:59 | <Cale> | tomsmeding: You mean like, reflecting the work of the pattern match checker back into the type system? |
| 2021-06-22 17:00:58 | × | wagle quits (~wagle@quassel.wagle.io) (Ping timeout: 268 seconds) |
| 2021-06-22 17:01:04 | × | argento quits (~argent0@168-227-96-26.ptr.westnet.com.ar) (Ping timeout: 252 seconds) |
| 2021-06-22 17:01:20 | → | wagle joins (~wagle@quassel.wagle.io) |
| 2021-06-22 17:01:23 | oats | is now known as ot |
| 2021-06-22 17:01:29 | ot | is now known as ailur |
| 2021-06-22 17:01:31 | ailur | is now known as hugs |
| 2021-06-22 17:01:33 | hugs | is now known as oats |
| 2021-06-22 17:01:38 | → | ddellacosta joins (~ddellacos@ool-44c73aff.dyn.optonline.net) |
| 2021-06-22 17:02:40 | <dminuoso> | Cale: So I havent done much type level programming, but I'd have thought that knowing whether type types are equal might be as interesting as knowing that they are not. |
| 2021-06-22 17:02:45 | <dminuoso> | Perhaps Im wrong |
| 2021-06-22 17:02:48 | <thyriaen> | guys |
| 2021-06-22 17:02:54 | <thyriaen> | i think i am in love |
| 2021-06-22 17:02:57 | <tomsmeding> | Cale: my point was that theoretically, you might be able to have e.g. data Foo a where { A :: Int -> Foo 'True ; B :: Bool -> Foo 'False } ; foo :: (a !~ 'False) => Foo a -> Int ; foo (A i) = i |
| 2021-06-22 17:03:11 | <tomsmeding> | and then the pattern match checker would be fine with that because of the inequality context |
| 2021-06-22 17:03:14 | <thyriaen> | why do non-functional languages even exist |
| 2021-06-22 17:03:21 | <tomsmeding> | not sure how useful this ability would even be |
| 2021-06-22 17:03:32 | → | Erutuon joins (~Erutuon@user/erutuon) |
| 2021-06-22 17:04:02 | <tomsmeding> | thyriaen: ease of compiler implementation, more control over the compiled form, more natural expression of imperative algorithms, inertia |
| 2021-06-22 17:04:11 | <tomsmeding> | not necessarily in that order :p |
| 2021-06-22 17:04:17 | <dminuoso> | tomsmeding: Because it took decades before a half way efficient encoding of a lazy functional programming language was found. Imperative languages tend to be simpler to compile into locally good code? |
| 2021-06-22 17:04:36 | <Cale> | thyriaen: Because lots of stuff got done before people had any idea how to compile functional programs into a reasonably efficient form, and people kept using those languages because relearning how to program is annoying. |
| 2021-06-22 17:04:41 | <dminuoso> | Err thyriaen ^- |
| 2021-06-22 17:05:13 | → | econo joins (uid147250@user/econo) |
| 2021-06-22 17:05:36 | → | warnz joins (~warnz@2600:1700:77c0:5610:799f:ce24:eb20:cceb) |
| 2021-06-22 17:06:21 | × | ddellacosta quits (~ddellacos@ool-44c73aff.dyn.optonline.net) (Ping timeout: 265 seconds) |
| 2021-06-22 17:06:34 | × | chomwitt quits (~Pitsikoko@athedsl-351576.home.otenet.gr) (Ping timeout: 252 seconds) |
| 2021-06-22 17:06:38 | <safinaskar> | thyriaen: ha-ha. i hate haskell. currently i write my parser lib in haskell and my prover in haskell. The whole reason why i pick haskell is this: because I already wrote a lot of code. :) If I started now, I'd pick rust. because it is impure. and gives full control on speed |
| 2021-06-22 17:08:37 | <mikko> | isn't that how it usually goes, every language seems really good until you do something bigger with and then it's too late to change :) |
| 2021-06-22 17:09:17 | → | arjun joins (~user@user/arjun) |
| 2021-06-22 17:09:59 | <arjun> | hi all |
| 2021-06-22 17:10:01 | → | pretty_dumm_guy joins (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) |
| 2021-06-22 17:10:09 | <tomsmeding> | safinaskar: this experimentation with moving stuff to the type level that you're doing would be completely impossible from the start in rust :p |
| 2021-06-22 17:10:25 | <arjun> | how do i deal with if this throws an error ?-> https://hackage.haskell.org/package/directory-1.3.6.2/docs/System-Directory.html#v:removeDirectory |
| 2021-06-22 17:10:57 | <safinaskar> | tomsmeding: yes, still rust has more benefits |
| 2021-06-22 17:11:29 | → | Scotty_Trees joins (~Scotty_Tr@162-234-179-169.lightspeed.brhmal.sbcglobal.net) |
| 2021-06-22 17:11:32 | <tomsmeding> | safinaskar: for your purpose / in your opinion :) |
| 2021-06-22 17:11:36 | × | haveo quits (~haveo@sl35.iuwt.fr) (Quit: leaving) |
| 2021-06-22 17:11:39 | <Cale> | tomsmeding: Which is possibly a point in rust's favour on its own, since it would save him wasting time messing around with fancy types, haha :D |
| 2021-06-22 17:11:46 | <tomsmeding> | :D |
| 2021-06-22 17:12:10 | <safinaskar> | tomsmeding: also, surprisingly, c++ has dependent types! (but arguments to type-level expressions should be compile-time values) |
| 2021-06-22 17:12:17 | × | jess quits (~jess@libera/staff/jess) () |
| 2021-06-22 17:12:36 | <tomsmeding> | and rust is getting that same capability (const generics) |
| 2021-06-22 17:12:38 | <Cale> | For some value of "has", yeah |
| 2021-06-22 17:13:21 | <dminuoso> | GHC Haskell has capabilities too! |
| 2021-06-22 17:13:50 | <tomsmeding> | % Control.Concurrent.getNumCapabilities |
| 2021-06-22 17:13:51 | <yahb> | tomsmeding: 1 |
| 2021-06-22 17:14:28 | → | wallymathieu joins (~wallymath@81-234-151-21-no94.tbcn.telia.com) |
| 2021-06-22 17:14:56 | × | curiousgay quits (~curiousgg@178.217.208.8) (Remote host closed the connection) |
| 2021-06-22 17:14:56 | <tomsmeding> | arjun: try 'catch' from Control.Exception |
| 2021-06-22 17:15:12 | → | curiousgay joins (~curiousgg@178.217.208.8) |
| 2021-06-22 17:15:46 | × | alx741 quits (~alx741@181.196.68.152) (Ping timeout: 268 seconds) |
| 2021-06-22 17:18:11 | × | Guest75 quits (~Guest75@166.70.242.157) (Quit: Ping timeout (120 seconds)) |
| 2021-06-22 17:18:51 | × | lavaman quits (~lavaman@98.38.249.169) (Ping timeout: 268 seconds) |
| 2021-06-22 17:18:51 | <safinaskar> | tomsmeding: C++ can be used as a prover! look here: https://godbolt.org/z/MzhedqeKE . I can write more code to show the point, i. e. give some example proofs |
| 2021-06-22 17:20:05 | → | chisui joins (~chisui@200116b866492700f0ddc72238639ee4.dip.versatel-1u1.de) |
| 2021-06-22 17:20:38 | → | sheepduck joins (~sheepduck@user/sheepduck) |
| 2021-06-22 17:20:40 | <tomsmeding> | hah, neat |
| 2021-06-22 17:20:45 | <chisui> | Hey, is there a reason why there are no closed data families? |
| 2021-06-22 17:21:29 | <Cale> | The static nature of template instantiation will eventually get in your way trying to do that stuff in C++, and of course the syntax is insanely cumbersome and not really meant for that, but you can do a fair amount. |
| 2021-06-22 17:22:11 | <Cale> | chisui: How would that differ from a GADT? |
| 2021-06-22 17:22:42 | <chisui> | Cale You can't have the instance be newtypes. |
| 2021-06-22 17:22:55 | <Cale> | ah, fair |
| 2021-06-22 17:26:03 | → | haveo joins (~haveo@sl35.iuwt.fr) |
| 2021-06-22 17:27:20 | <safinaskar> | Cale: "What behaviour do you get if you turn on AllowAmbiguousTypes by the way?": my (final) code still gives nearly same error if I enable AllowAmbiguousTypes: https://paste.debian.net/1202054/ |
| 2021-06-22 17:28:00 | → | Guest9 joins (~Guest9@43.250.158.34) |
| 2021-06-22 17:28:28 | → | alx741 joins (~alx741@181.196.68.156) |
| 2021-06-22 17:28:49 | <arjun> | tomsmeding: i'll do that, thanks! |
| 2021-06-22 17:31:27 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-06-22 17:32:17 | × | justsomeguy quits (~justsomeg@user/justsomeguy) (Quit: WeeChat 3.0.1) |
| 2021-06-22 17:33:10 | <Cale> | safinaskar: On 3868, your code compiles without warning, but I'm not sure I'm actually happy about that, since an attempt to use proof will result in a type error. |
| 2021-06-22 17:36:30 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 258 seconds) |
| 2021-06-22 17:36:40 | × | kuribas quits (~user@ptr-25vy0i89phmaoo2wmls.18120a2.ip6.access.telenet.be) (Quit: ERC (IRC client for Emacs 26.3)) |
| 2021-06-22 17:37:00 | × | mikoto-chan quits (~mikoto-ch@ip-213-49-189-31.dsl.scarlet.be) (Ping timeout: 252 seconds) |
| 2021-06-22 17:41:46 | × | azeem quits (~azeem@dynamic-adsl-84-220-246-231.clienti.tiscali.it) (Ping timeout: 252 seconds) |
| 2021-06-22 17:42:32 | → | azeem joins (~azeem@176.201.6.138) |
| 2021-06-22 17:45:53 | × | thyriaen quits (~thyriaen@45.178.73.238) (Quit: Leaving) |
| 2021-06-22 17:47:08 | ← | safinaskar parts (~safinaska@109.252.90.89) () |
| 2021-06-22 17:47:25 | → | notzmv joins (~zmv@user/notzmv) |
| 2021-06-22 17:49:23 | → | safinaskar joins (~safinaska@109.252.90.89) |
| 2021-06-22 17:51:34 | <safinaskar> | is there any other uses for GADTs except for writing type checkers and provers? |
| 2021-06-22 17:53:27 | <dminuoso> | No, they were built for that sole usage. They are forbidden for all other things like modelling ASTs |
| 2021-06-22 17:53:47 | <dminuoso> | (that was sarcasm, by the way) |
| 2021-06-22 17:56:06 | × | azeem quits (~azeem@176.201.6.138) (Read error: Connection reset by peer) |
| 2021-06-22 17:56:26 | × | arjun quits (~user@user/arjun) (Ping timeout: 258 seconds) |
| 2021-06-22 17:56:38 | <safinaskar> | dminuoso: "modelling ASTs" - this is type checking, again. is there any example where GADTs can be used for AST modeling, but not for type checking? |
| 2021-06-22 17:56:48 | <dminuoso> | this is not type checking. |
| 2021-06-22 17:58:10 | → | azeem joins (~azeem@dynamic-adsl-84-220-246-231.clienti.tiscali.it) |
| 2021-06-22 17:58:48 | × | fresheyeball quits (~fresheyeb@c-71-237-105-37.hsd1.co.comcast.net) (Quit: WeeChat 2.9) |
| 2021-06-22 18:00:00 | × | fef quits (~thedawn@user/thedawn) (Ping timeout: 244 seconds) |
| 2021-06-22 18:00:07 | <tomsmeding> | safinaskar: probably no, but "provers" is very general |
| 2021-06-22 18:00:42 | __monty__ | is now known as SirJection |
| 2021-06-22 18:00:49 | <tomsmeding> | e.g. a compiler can represent the AST of the program being compiled with a GADT; by doing so, the act of writing the compiler using that data type proves that all compiler passes are type-correct with respect to the language being compiled |
| 2021-06-22 18:00:58 | → | mikoto-chan joins (~mikoto-ch@ip-213-49-189-31.dsl.scarlet.be) |
All times are in UTC.