Logs: freenode/#haskell
| 2021-04-25 18:14:48 | <Uniaika> | nut: either you compile it with stack's option '--package lens' |
| 2021-04-25 18:14:55 | <Uniaika> | or you create a cabal or stack project |
| 2021-04-25 18:15:04 | → | knupfer joins (~Thunderbi@200116b82be79e0055f724416be108a9.dip.versatel-1u1.de) |
| 2021-04-25 18:15:26 | <nut> | ok, so have to be inside a cabal project(I'm not using stack) |
| 2021-04-25 18:15:37 | <Uniaika> | yes, you should |
| 2021-04-25 18:15:46 | <maerwald> | I don't know anything about emacs, but in cabal you can do: cabal repl --build-depends lens |
| 2021-04-25 18:15:48 | <ski> | actual dependent types, or approximating some usages of them, via singleons, GADTs ? |
| 2021-04-25 18:16:25 | <Uniaika> | gnumonic: you *do* realise that Haskell is *not* a dependently-typed language? |
| 2021-04-25 18:16:39 | <maerwald> | gnumonic: the f* tutorial |
| 2021-04-25 18:16:52 | × | tlaxkit quits (~konversat@185.228.155.197) (Quit: Konversation terminated!) |
| 2021-04-25 18:16:54 | <maerwald> | gnumonic: https://www.fstar-lang.org/tutorial/ |
| 2021-04-25 18:17:13 | <geekosaur> | hasochism :) |
| 2021-04-25 18:17:30 | <Uniaika> | hehehe |
| 2021-04-25 18:17:47 | <gnumonic> | Er, yeah, I know there are things you can't do in Haskell and that it's not dependently typed but it's kind of frustrating trying to figure out how to fake something with singletons when I have a somewhat poor understanding of the thing I'm trying to fake :p |
| 2021-04-25 18:18:11 | <tapas> | Uniaika: i'm pushing to get a BNF specified for the next or succ next major release so people can write these tools as they please. |
| 2021-04-25 18:19:00 | <tapas> | i don't care if someone wants to write dhall to specify a build. That's fine. As long as the build tool knows how to normalize it and turn it into somthing that works. |
| 2021-04-25 18:19:10 | <gnumonic> | Oh that fstar tutorial looks very good, thank you. |
| 2021-04-25 18:19:34 | <maerwald> | The language is also superior to haskell in term of verification features |
| 2021-04-25 18:21:05 | × | xff0x quits (~xff0x@2001:1a81:5378:d500:70a3:57b2:577c:e365) (Quit: xff0x) |
| 2021-04-25 18:22:13 | × | dyeplexer quits (~lol@unaffiliated/terpin) (Remote host closed the connection) |
| 2021-04-25 18:23:19 | <zzz> | does anyone know what this means? https://paste.jrvieira.com/1619374859564 |
| 2021-04-25 18:25:07 | <maerwald> | WSL? |
| 2021-04-25 18:25:07 | <geekosaur> | I'm getting a cert error from that url |
| 2021-04-25 18:25:30 | → | unclechu joins (unclechuma@gateway/shell/matrix.org/x-jmbbnkztqlxjmyvi) |
| 2021-04-25 18:25:49 | <zzz> | no wsl |
| 2021-04-25 18:26:05 | <zzz> | this is not the first time this happens and i fogot what i did last time |
| 2021-04-25 18:26:41 | <zzz> | geekosaur: what's the error? looks fine to me |
| 2021-04-25 18:27:12 | <gnumonic> | also, though maybe this is a dumb question, in what sense is e.g. the Sigma type in singletons an approximation of a dependent pair in "real" dependently typed language? The ergonomics are pretty bad but it's a real dependent pair, isn't it? |
| 2021-04-25 18:27:16 | → | philderbeast joins (~textual@bras-base-vldvpq5901w-grc-06-184-144-244-252.dsl.bell.ca) |
| 2021-04-25 18:28:08 | → | ADG1089 joins (~aditya@171.76.29.233) |
| 2021-04-25 18:29:10 | <monochrom> | fdTryLock? Is that 32-bit GHC? |
| 2021-04-25 18:29:13 | → | coot joins (~coot@37.30.50.130.nat.umts.dynamic.t-mobile.pl) |
| 2021-04-25 18:29:22 | <zzz> | monochrom: yes it is |
| 2021-04-25 18:29:56 | <zzz> | ghc 8.10.4 |
| 2021-04-25 18:30:27 | <zzz> | linux 32bit |
| 2021-04-25 18:30:41 | <monochrom> | Actually I forgot whether it's GHC or cabal-install, but definitely either one's 32-bit linux build. |
| 2021-04-25 18:30:44 | → | ddellaco_ joins (~ddellacos@ool-44c73afa.dyn.optonline.net) |
| 2021-04-25 18:31:33 | <ski> | @where SF |
| 2021-04-25 18:31:33 | <lambdabot> | "Software Foundations" by Pierce,Casinghino,Greenberg,Sjöberg,Yorgey in 2011-06 at <http://www.cis.upenn.edu/~bcpierce/sf/> about "the mathematical theory of programming and programming languages", |
| 2021-04-25 18:31:34 | <lambdabot> | "It develops basic concepts of functional programming, logic, operational semantics, lambda-calculus, and static type systems, using the Coq proof assistant." |
| 2021-04-25 18:31:36 | <ski> | @where CPDT |
| 2021-04-25 18:31:36 | <lambdabot> | "Certified Programming with Dependent Types" by Adam Chlipala (aka Smerdyakov) (in progress) at <http://adam.chlipala.net/cpdt/>, "about practical engineering with the Coq proof assistant" |
| 2021-04-25 18:31:36 | <monochrom> | Ah, cabal-install, https://github.com/haskell/cabal/issues/7313 |
| 2021-04-25 18:31:45 | <ski> | iirc, there's also one called "Coq'Art" ? |
| 2021-04-25 18:31:50 | <ski> | gnumonic ^ |
| 2021-04-25 18:32:41 | <monochrom> | If you can downgrade to 3.2.0.0, that works beautifully. |
| 2021-04-25 18:32:56 | <unclechu> | hey, why if i define my own version of `$` exactly the same way as it’s defined in `base` library rankntypes get broken? |
| 2021-04-25 18:33:23 | <unclechu> | i get these: “Expected type: (SFoo α0 -> p0) -> String” “Actual type: (forall (β :: Foo). Singleton β -> String) -> String” |
| 2021-04-25 18:33:41 | <monochrom> | If not, do your own build of 3.4.0.0 but add a flag like the link says near the end. |
| 2021-04-25 18:33:43 | <unclechu> | it works perfectly fine if i use `$` |
| 2021-04-25 18:33:44 | <zzz> | monochrom: thanks. i think that's what i had done, but must have forgotten and upgraded again thanks to ghcup suggesting me. trying it now |
| 2021-04-25 18:33:55 | <monochrom> | :) |
| 2021-04-25 18:34:01 | <maerwald> | is that a known bug? |
| 2021-04-25 18:34:03 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 252 seconds) |
| 2021-04-25 18:34:03 | <monochrom> | Yeah I think deja vu too. |
| 2021-04-25 18:34:05 | <monochrom> | Yes. |
| 2021-04-25 18:34:08 | <monochrom> | See the link. |
| 2021-04-25 18:34:08 | <ski> | unclechu : compiler magic |
| 2021-04-25 18:34:24 | <unclechu> | ski: do you know something about it? |
| 2021-04-25 18:34:35 | <ski> | special-casing of `$' in GHC |
| 2021-04-25 18:34:38 | <maerwald> | ok, I'll just build an unofficial bindist then |
| 2021-04-25 18:35:17 | <ski> | treating `... $ ...' as `(...) (...)', to avoid impredicativity problems |
| 2021-04-25 18:36:07 | <unclechu> | ski: i assume there is now way to make it handle my custom operator the same way without changing the compiler itself? |
| 2021-04-25 18:36:44 | <gnumonic> | ski: thanks for the links. i read through some of the upenn stuff a while ago for help with the STLC but had forgotten about it |
| 2021-04-25 18:37:06 | <unclechu> | ski: how about `(Data.Function.&)`? |
| 2021-04-25 18:37:26 | → | kuribas joins (~user@ptr-25vy0i72aubpu4xq2xw.18120a2.ip6.access.telenet.be) |
| 2021-04-25 18:37:43 | × | geowiesnot quits (~user@i15-les02-ix2-87-89-181-157.sfr.lns.abo.bbox.fr) (Ping timeout: 252 seconds) |
| 2021-04-25 18:37:50 | × | DTZUZU quits (~DTZUZO@205.ip-149-56-132.net) (Read error: Connection reset by peer) |
| 2021-04-25 18:38:01 | <unclechu> | ski: i can see that `&` is also have the same problem. |
| 2021-04-25 18:39:46 | <zva> | hey I'm using WSL and neovim and would like to have a developmentenvironment that proposes functions via a hotkey like eclipse for java. I found multiple complicated approaches googling and I wonder if there is an easy way out or something that you use? |
| 2021-04-25 18:40:04 | <zva> | *template proposals in neovim |
| 2021-04-25 18:40:21 | × | hendursa1 quits (~weechat@gateway/tor-sasl/hendursaga) (Ping timeout: 240 seconds) |
| 2021-04-25 18:41:29 | → | horatiohb joins (~horatiohb@159.89.43.106) |
| 2021-04-25 18:41:42 | → | DTZUZU joins (~DTZUZO@205.ip-149-56-132.net) |
| 2021-04-25 18:41:53 | <ski> | unclechu : afaik, no |
| 2021-04-25 18:42:05 | <unclechu> | okay, thanks for the info |
| 2021-04-25 18:43:28 | × | pjb quits (~pjb@2a01cb04063ec500ad42b45c394adc0f.ipv6.abo.wanadoo.fr) (Remote host closed the connection) |
| 2021-04-25 18:44:22 | <maerwald> | zva: the only option is HLS, which is a LSP server |
| 2021-04-25 18:44:39 | <maerwald> | neovim has an LSP client embedded I think |
| 2021-04-25 18:44:44 | <geekosaur> | zzz, it's saying the cert authority isn't trusted. ubuntu 13.04, which I'd expect to support all the cert authorities |
| 2021-04-25 18:44:46 | <maerwald> | otherwise there are enough options |
| 2021-04-25 18:44:58 | <geekosaur> | as usual the detail gets hidden by chrome |
| 2021-04-25 18:45:28 | <zva> | you mean as in enough options that are not neovim? |
| 2021-04-25 18:45:31 | <monochrom> | Isn't ubuntu 13.04 too old and un-updated? |
| 2021-04-25 18:45:42 | <geekosaur> | sorry 18.04 |
| 2021-04-25 18:45:45 | <geekosaur> | I typoed |
| 2021-04-25 18:46:01 | <geekosaur> | should be latest, I installed this machine only a month or so ago |
| 2021-04-25 18:46:18 | <geekosaur> | wow, I misread /etc/lsb-release. 20.04 |
| 2021-04-25 18:46:26 | <hpc> | yeah, i was going to say ubuntu is year.month |
| 2021-04-25 18:47:16 | → | xff0x joins (~xff0x@2001:1a81:5378:d500:c8e4:3d2e:19af:2ab8) |
| 2021-04-25 18:47:56 | <__minoru__shirae> | they're going to have to change the naming policy after the year 3000 |
| 2021-04-25 18:48:57 | <Uniaika> | tapas: <3 |
| 2021-04-25 18:50:41 | × | mozzarella quits (~sam@unaffiliated/sam113101) (Ping timeout: 240 seconds) |
| 2021-04-25 18:50:54 | <zzz> | geekosaur: i'm using let's encrypt |
| 2021-04-25 18:51:01 | <zzz> | hum... |
| 2021-04-25 18:51:14 | × | fox[m]1 quits (foxforestf@gateway/shell/matrix.org/x-ktrnqcmqwewsriyn) (Ping timeout: 245 seconds) |
| 2021-04-25 18:51:14 | × | slycelote[m] quits (slycelotem@gateway/shell/matrix.org/x-qxwtofvhhmvbqmln) (Ping timeout: 245 seconds) |
| 2021-04-25 18:51:14 | × | pqwy[m] quits (pqwymatrix@gateway/shell/matrix.org/x-oheqkealrnytrlhs) (Ping timeout: 245 seconds) |
| 2021-04-25 18:51:14 | × | alexfmpe quits (alexfmpema@gateway/shell/matrix.org/x-trjxzqvsyvzjueef) (Ping timeout: 245 seconds) |
| 2021-04-25 18:51:15 | × | CrabMan quits (phi-matrix@gateway/shell/matrix.org/x-ivwszzyccqpifjnv) (Ping timeout: 245 seconds) |
All times are in UTC.