[07:45] <imadper> ...
[07:46] <imadper> contrun[m]: .
[07:52] <contrun[m]> imadper: .
[07:53] <imadper> contrun[m]: 有啥好玩的吗?
[07:53] <imadper> contrun[m]: 不想上班啊
[07:53] <contrun[m]> 武汉 中南海
[07:53] <contrun[m]> 最好 先去武汉
[07:54] <contrun[m]> 我他妈的现在送水的也害怕
[07:54] <contrun[m]> 不知道还有没有勇气自杀
[07:54] <imadper> contrun[m]: 还好我家里有ro反透
[07:55] <imadper> contrun[m]: 没事儿干工信部投诉着玩呗?
[07:55] <imadper> 我已经投诉了一波了
[07:56] <contrun[m]> imadper: 什么叫 ro 反透
[07:57] <imadper> contrun[m]: 小米净水器搜一下?
[07:57] <imadper> contrun[m]: 陶氏反透膜过滤出来的水
[07:57] <contrun[m]> imadper: 艹
[07:57] <imadper> contrun[m]: 我家里的蔬菜还能再吃一周多.
[07:58] <imadper> contrun[m]: 先捡着保质期短的吃
[07:58] <imadper> contrun[m]: 我就是觉得, 我得买点儿方便面啊
[07:58] <contrun[m]> imadper: 出租房好装？
[07:58] <imadper> contrun[m]: 好装
[07:58] <imadper> contrun[m]: 你能保证租下去, 住三年以上, 就行
[07:58] <contrun[m]> imadper: 那真是简单
[07:59] <imadper> contrun[m]: 恩, 安装不用你动手
[07:59] <contrun[m]> imadper: 我已经吃面包吃到吐了
[07:59] <imadper> contrun[m]: 妈了个鸡, 我年前买了两个水龙头, 想要换上去
[07:59] <imadper> contrun[m]: 但是tmd我不敢去借管钳
[08:00] <contrun[m]> imadper: 不知道 新型冠状病毒在普通状况下 多久才能失去活性
[08:00] <imadper> contrun[m]: 干燥空气里, 俩小时足够了吧
[08:01] <contrun[m]> imadper: 你到网上买个不行？ 就是怕快递员而已
[08:01] <imadper> contrun[m]: 大钳子用不到及此处
[08:01] <imadper> 用不了几次
[08:01] <imadper> contrun[m]: 买一个多亏啊
[08:02] <contrun[m]> imadper: 是时候学当水管工了
[08:02] <imadper> contrun[m]: 我早就干过这事儿了
[08:03] <imadper> contrun[m]: 毕竟我改过三次水电了
[08:03] <imadper> contrun[m]: 还有给水管加螺纹的那个东西, 我也玩过
[08:04] <contrun[m]> imadper: 不行 你不能一个人干啊
[08:04] <contrun[m]> imadper: 一个人干谁来接你的钳子
[08:05] <imadper> contrun[m]: ... ...
[08:22] <contrun[m]> imadper: 我们县县城据说也已经封了
[08:23] <imadper> contrun[m]: 好事儿啊
[08:24] <imadper> contrun[m]: 就是要所有人都不出家门才好
[08:24] <imadper> contrun[m]: 所有宿主都死光就完事儿了
[08:24] <imadper> contrun[m]: 或者自然痊愈
[08:24] <contrun[m]> imadper: 疫情加重才会封
[08:25] <imadper> contrun[m]: 肯定会加重的
[08:25] <imadper> contrun[m]: 我估计啊, 真要大家都开工, 就北京地铁这个鸟样子
[08:25] <imadper> contrun[m]: 一趟车怎么也得多几十个病例
[08:26] <contrun[m]> imadper: 主要还是现在没有摸清 怎么传播的 没法有效抑制传播
[08:26] <albet70> 接触 飞沫 空气传播
[08:26] <contrun[m]> imadper: 没有感染的人也能传播
[08:27] <imadper> contrun[m]: 坐等 remdesivir
[08:27] <imadper> contrun[m]: 我决定了, 我司系统下一版代号: remdesivir
[08:28] <contrun[m]> imadper: 你说 你司快还是 remdesivir 快
[08:28] <contrun[m]> albet70: 我应该说没法辨识传播源
[08:28] <imadper> contrun[m]: 那当然是我司快了.
[08:28] <imadper> 不是还有粪口传播?
[08:29] <imadper> 吃别人的排泄物导致的?
[08:29] <albet70> 过几天都返京了，北京会不会有爆发
[08:29] <contrun[m]> 不知道现在有多少返京了
[08:29] <imadper> 好像是说, 有可能会因为楼里共用一个排水道, 导致交叉感染
[08:30] <imadper> contrun[m]: 我妈他们小区一例确诊, 两个密切接触
[08:30] <albet70> 我们公司延迟到10号
[08:30] <contrun[m]> 近来各地其实增加不多了 除了那些好像控制不住的省份 比如湖北 湖南 广东 浙江
[08:30] <albet70> 我们部门没有一个回去的
[08:30] <imadper> contrun[m]: 我过年去了一趟, 目前还没症状, 已经8天了
[08:31] <imadper> contrun[m]: 要不约出来喝咖啡啊?
[08:31] <contrun[m]> imadper: 我他妈的现在都不敢去楼下取水
[08:31] <imadper> contrun[m]: 怂逼
[08:31] <imadper> contrun[m]: 我还敢去买菜呢
[08:31] <imadper> contrun[m]: 不过自来水煮沸也能喝啊
[08:32] <contrun[m]> albet70: 我室友一个也没回来 不知道 返程高峰是啥时候
[08:32] <albet70> contrun 2.10
[08:32] <contrun[m]> imadper:  我他妈就是怂啊 我还没女朋友
[08:32] <imadper> contrun[m]: 危险啊, 不要给你舍友开门啊
[08:32] <imadper> contrun[m]: 羡慕你
[08:32] <contrun[m]> imadper: 那不行 我要饿死了
[08:33] <contrun[m]> imadper: 天天吃面包 吃不下去了
[08:33] <imadper> contrun[m]: ... ...
[08:33] <contrun[m]> 室友回来可以吃她们做的
[08:33] <imadper> contrun[m]: 我再教你几道快手菜?
[08:33] <imadper> 她们???
[08:33] <contrun[m]> imadper: 懒 不做
[08:33] <imadper> contrun[m]: 你射友是姑娘?
[08:33] <contrun[m]> imadper: 怕 不去买蔬菜
[08:33] <contrun[m]> imadper: 室友是姑娘
[08:33] <albet70> contrun 你去超市买点菜或点外卖呀
[08:34] <imadper> contrun[m]: 还有房间吗?
[08:34] <albet70> 北京现在外卖还有吗？
[08:34] <imadper> contrun[m]: 加一个
[08:34] <imadper> albet70: 没吃过, 每天在家做饭.
[08:34] <imadper> albet70: 不过四五天之前, 叫了一个呷哺外卖, 还没问题
[08:34] <contrun[m]>  albet70 有吧 正月初三点过一次  呷哺呷哺
[08:35] <imadper> albet70: 而且吧, 我顺便多买了很多火锅涮料, 很多羊肉片, 牛百叶, 自己涮
[08:35] <albet70> 呷哺太贵了。。。
[08:35] <imadper> 说出来你们可能不信, 我家的蔬菜能抗一周, 肉能抗俩月, 大米/食用油能抗一年
[08:35] <contrun[m]> 点一次 吃了我三餐
[08:35] <albet70> 厉害👍
[08:36] <imadper> 买一些西红柿, 黄瓜, 这些存得住的
[08:36] <contrun[m]> 我的面包 够我一个人吃半个月吧
[08:36] <albet70> 我都是买鸡蛋 大葱
[08:36] <imadper> 我昨天还买了很多大蒜
[08:36] <imadper> 不然做饭没有灵魂
[08:37] <albet70> 买大蒜是为了防止你变僵尸吗？
[08:37] <imadper> albet70: 能变僵尸的话我早就变了
[08:39] <albet70> 北京过几天要是有爆发的话，会封城吧？
[08:40] <imadper> albet70: 你说的好有道理
[08:40] <imadper> 我都几周没吃过泡面了
[08:40] <imadper> 我要提前买几箱
[08:40] <imadper> 顺便买个switch吧.
[08:40] <albet70> 4号线 13号线 昌平线 5号线，这四个线到时估计。。。
[08:40] <imadper> 我觉得, 只要封锁公共交通, 就不怎么会爆发
[08:41] <imadper> 6号线前几天不是有个确诊的嘛?
[08:41] <imadper> 草房站
[08:41] <albet70> 。。。
[08:41] <contrun[m]> 我艹 这么牛逼
[08:41] <contrun[m]> 我们小区门口反正是有人站岗
[08:43] <imadper> contrun[m]: http://www.rfi.fr/cn/  这啥网站? 法国版的世界各国灾难?
[08:44] <imadper> contrun[m]: sb google瞎给我出搜索结果..
[08:44] <imadper> contrun[m]: 我操, 最下面合作伙伴... 竟然是sb轮子
[08:45] <contrun[m]> imadper: 法广当然不歌颂你国
[08:45] <contrun[m]> imadper: 不过这震惊也是够牛逼的
[08:46] <imadper> contrun[m]: 不管了, 我去做饭了
[08:46] <albet70> 在idea上配置Scala，恶心
[08:47] <albet70> 这国外的源速度怎么这么恶心
[08:49] <contrun[m]> albet70: 透明代理大法好
[08:49] <imadper> albet70: metals保平安
[08:49] <imadper> albet70: https://scalameta.org/metals/docs/editors/emacs.html
[08:49] <imadper> 不得不说, metals真是越来越好用
[08:50] <contrun[m]> imadper: 但是人家还是要下载库
[08:50] <contrun[m]> imadper: 速度还是很慢
[08:50] <imadper> proxychains sbt build
[08:50] <contrun[m]> imadper: graftcp 大法好
[08:50] <imadper> contrun[m]: 我看看
[08:51] <imadper> contrun[m]: 好东西啊
[08:51] <contrun[m]> imadper: 妈妈再也不用担心我 没法代理静态链接的程序了
[08:51] <imadper> contrun[m]: 我大jvm就没有不能代理的
[08:51] <contrun[m]> imadper: 垃圾 jvm 迟早要完
[08:52] <imadper> contrun[m]: jvm美得很
[08:52] <contrun[m]> imadper: 我王镜泽就是饿死也不用jvm
[08:53] <imadper> contrun[m]: 扔掉你的安卓手机
[08:53] <albet70> lsp... 在win10上编译lsp-server简直就是找罪受
[08:53] <contrun[m]> albet70: 用 win10不是找罪受？
[08:53] <imadper> albet70: lsp-server还用编译?
[08:53] <imadper> lsp-server不就是metals吗?
[08:54] <contrun[m]> imadper: 不一定有变异好的包释放出来啊
[08:54] <albet70> 以前想在win10上编译hsdev，社区的人直接告诉我，依赖文件的数量都够地球到月球了
[08:54] <imadper> contrun[m]: 我在想, jar文件在win10上跑, 还需要重新编译?
[08:54] <imadper> 没用过win10, 不知道诶
[08:55] <imadper> contrun[m]: 前几天倩倩的wsl不工作了, 我怎么也没给她修好
[08:55] <contrun[m]> imadper: 不需要
[08:55] <imadper> 对啊
[08:55] <imadper> contrun[m]: 你haskell能跨平台吗?
[08:55] <imadper> contrun[m]: 垃圾
[08:55] <imadper> contrun[m]: 我scala可以!
[08:55] <contrun[m]> imadper:  真牛逼
[08:56] <imadper> contrun[m]: 说个正经的, fs-cache这个module需要改进啊
[08:56] <contrun[m]> imadper: 但是我王镜泽还是不用
[08:56] <albet70> kotlin也可以呀
[08:56] <imadper> albet70: kotlin有这么复杂的implicit吗?
[08:56] <contrun[m]> albet70: 神仙打架
[08:56]  * imadper 做饭做饭
[08:56] <albet70> 呵呵
[08:58] <albet70> contrun haskel入门时间太长了
[08:58] <contrun[m]> albet70: 值得
[08:58] <albet70> 我学习快一年了，还没入门
[08:59] <contrun[m]> albet70: 都看了啥？
[08:59] <albet70> 一开始就是monad monad transformers 然后就是直接写代码呀
[08:59] <albet70> 中间有大量的概念学习
[09:00] <albet70> cont monad花了我两个月
[09:00] <albet70> 还有那些神奇的features RankNTypes
[09:01] <albet70> 还有ad-hoc polymorphism, parametric polymorphism
[09:01] <contrun[m]> albet70: 最好系统地学习概念 我是学完 functional programming in scala  再看 typeclassopedia 就了解基本的概念了 之后就是了解 generics、lens、type level programming 以及 ghc 很多扩展了
[09:01] <albet70> 代码没怎么写，全花时间在理解概念上了
[09:02] <albet70> lens还没接触
[09:03] <albet70> 倒是用scotty yesod pgsql写过一些简单的后台
[09:03] <contrun[m]> cont monad 其实就是 yoneda 引理的一个特例
[09:03] <albet70> 用telegram做了个irc bridge
[09:04] <albet70> cont monad，CPS，callCC这三个花了很多时间理解。。。
[09:04] <contrun[m]> albet70: 你说的后面这些 我推荐你看 thinking with tyoes 这书
[09:04] <imadper> thinking with typos?
[09:05] <albet70> 你对kind有理解吗？
[09:05] <contrun[m]>   foundations of algebraic  geometry 是这么描述 yoneda 引理的 有些定理需要你花一些时间去消化他 之后你就可以完全忘了它
[09:05] <albet70> 据说kind之上还有sort
[09:05] <imadper> <thinking with typos> 上来就讲 kind 的...
[09:05] <imadper> 我也就看了上来这几页
[09:05] <contrun[m]> types
[09:05] <contrun[m]> 没讲太多 kinds
[09:05] <albet70> 我到现在依然不知道Curry-Howard 那个到底是干啥的
[09:06] <contrun[m]> 我也不知道啊 看了一阵子 lectures on Curry-howard correspondence  后来没看了
[09:07] <contrun[m]> 学习 coq 的话 肯定是需要这个的
[09:07] <albet70> Haskell的system F在lambda cube里是lambda-2，没有dependent type，人家rust整天吹这个，为什么Haskell没有？
[09:07] <contrun[m]> 不了解你说的这些概念
[09:07] <contrun[m]> rust 吹了啥？
[09:07] <contrun[m]> rust 也没有 dependent type
[09:08] <albet70> lambda cube是介绍type system的
[09:08] <albet70> rust有
[09:08] <contrun[m]> rust 显然没有啊 发我参考连接？
[09:09] <contrun[m]> haskell 是可以写出 dependent types 的 不过比较蛋疼
[09:09] <albet70> 你Google看看
[09:09] <contrun[m]> 语言本身有 dependent type 的我只知道 idris
[09:10] <contrun[m]> thinking with types 最后一章就是说的 dependent type
[09:10] <contrun[m]> rust 肯定本身是不支持 dependent type的 不需要 google
[09:10] <albet70> 哦
[09:10] <contrun[m]> rust 有 haskell 没有的东西 是 ownership
[09:11] <albet70> 但Haskell有一坨扩张
[09:11] <albet70> 扩展
[09:12] <contrun[m]> 了解这些才是真的要花好多时间
[09:12] <albet70> 你了解natural transform吗？
[09:13] <imadper> contrun[m]: 还有agda.
[09:13] <contrun[m]> ghc魔法还是太多了 好多东西没法理解 要看论文才能理解背后的故事
[09:13] <imadper> 我有个问题啊, 这么多东西记不住, 认不出来, 怎么办啊?
[09:13] <contrun[m]> 比如？imadper
[09:13] <imadper> 我随便找个scala的库, 一行都看不懂.
[09:13] <albet70> agda和Coq这种能做proof assistant的，我感觉不用学了
[09:14] <contrun[m]> albet70: agda 是general purpose
[09:14] <imadper> contrun[m]: 贵司年后有岗吗?
[09:14] <imadper> contrun[m]: 写haskell的?
[09:15] <contrun[m]> imadper:  可以为你创造一个
[09:15] <imadper> contrun[m]: 贵司蛋疼吗?
[09:15] <albet70> codewars上kata 1的题是论证加法交换律，别人说这是Coq这种Hello world级别的
[09:15] <imadper> contrun[m]: 我司无比蛋疼.
[09:16] <albet70> 我做kata 4这种fixed-point combinator的都快做不动了
[09:16] <albet70> 还有什么Church number之类的
[09:16] <contrun[m]> albet70: kata 是啥 不了解
[09:17] <contrun[m]> albet70: 你可以看下 types and programming languages
[09:17] <albet70> 一个rank标志
[09:17] <contrun[m]> albet70: church number 和 fixed point combinator 都是有介绍的的
[09:18] <albet70> 你看过simple typed lambda calculus吗？
[09:18] <contrun[m]> 一本书？
[09:18] <albet70> 嗯
[09:18] <albet70> 还有个untyped lambda calculus
[09:19] <albet70> 这个就是lambda cube里的lambda-1
[09:19] <contrun[m]> 这个就是 types and programming languages 前几章讲的
[09:19] <albet70> 哦
[09:19] <contrun[m]> types and programming languages 据说是 plt 的入门圣经
[09:19] <contrun[m]> 我还只看了前几章
[09:19] <contrun[m]> 这个假期看的
[09:20] <albet70> 里面有讲皮亚诺公理吗？
[09:20] <contrun[m]> 本来打算多看点 但是女人啊女人 我为什么和尚摸得我却摸不得
[09:20] <contrun[m]> 没有
[09:21] <contrun[m]> 利亚诺公理你可以看陶哲轩的分析一书
[09:21] <contrun[m]> 只看前面部分就行了
[09:21] <albet70> 后期需要的数学知识太多了，我到现在都不知道Category Theory到底讲啥
[09:21] <contrun[m]> 你看过 category theory for programmer 吗
[09:22] <albet70> 没有
[09:22] <contrun[m]> 简单的 category theory 可以看看 foundations of algebraic geometry  只看前面部分就行 有了感觉之后就看其他的书
[09:22] <albet70> 需要对monad monoid semigroup functor applicative 这些概念有一定的理解吗？
[09:23] <contrun[m]> 不需要
[09:23] <albet70> 我到现在都不知道ADT到底有啥用处。。。倒是知道有Product type和Sum type
[09:23] <contrun[m]>  category theory 一般不会讲 applicative 和 monad
[09:24] <albet70> type family见过就忘
[09:24] <contrun[m]> 比看比如 你需要一个 evaluator
[09:25] <contrun[m]> 你想要对一个表达式 进行求值 有了 adt 就只要模式匹配了
[09:26] <contrun[m]> product 和 sum 在范畴论里面也有这两个概念  学一点范畴论还是有好处的
[09:26] <contrun[m]> 你知道 product 和 sum 的泛性质之后 就会理解为什么它们到处出现
[09:26] <albet70> haskell wiki上有些概念讲解直接用数学上的那一套，或者直接给wikipedia上的数学定义，太难理解了
[09:27] <contrun[m]> 你要先看看基础的东西 自己动手算一算 脑子里面有了几个例子 才能看懂他们的语言
[09:28] <albet70> 那些数学符号看不懂。。。
[09:28] <albet70> 比如forall exists
[09:29] <contrun[m]> 数学符号？
[09:31] <contrun[m]> 全称量词不是高中知识吗
[09:33] <albet70> https://twitter.com/iceland_jack/status/1220326760589471744?s=21
[09:33] <albet70> forall可不是高中知识
[09:34] <albet70> https://wiki.haskell.org/Category_theory/Natural_transformation
[09:58] <albet70> 还有first-order logic这种怎么理解？是不是还有higher-order logic?
[10:14] <contrun[m]> 有 高阶逻辑 我不懂
[10:15] <contrun[m]> 你说的这是 https://wiki.haskell.org/Existential_type
[10:15] <contrun[m]> 可以看 thinking with types 一书
[11:20] <bsdplayer> rust现在在大型项目上不一定合适
[11:22] <bsdplayer> 据说巨硬要用rust来重写内核, 其他的信息不多...
=== bsdplayer is now known as chobitsbsd
[11:35] <imadper> 没有东西一定合适...
[11:35] <imadper> 所以任何语言都可以说不一定合适嘛
[11:39] <chobitsbsd> 是啊
[11:40] <chobitsbsd> 记得hurd
[11:40] <chobitsbsd> 为了完美的内核,结果现在都没开发成功...
[11:53] <imadper> 没动力吧
[11:53] <imadper> 现在去开发hurd, 得不偿失.
[12:11] <imadper> contrun[m]: ceph 还挺复杂啊
[12:11] <imadper> contrun[m]: 比我大zfs难多了
[12:12] <chobitsbsd> zfs太吃内存了
[12:12] <imadper> chobitsbsd: 限制一下arc_max_size
[12:12] <chobitsbsd> 以前在本子上安装各种bug...
[12:13] <imadper> zfs_arc_max
[12:13] <imadper> zfs bug肯定没有btrfs多嘛
[12:14] <chobitsbsd> 是啊
[12:14] <chobitsbsd> 毕竟还是企业级的东西
[12:15] <chobitsbsd> 当时想在笔记本上安装freebsd10, 现在想想真是闲的...
[12:20] <albet70> why not archlinux?
[12:21] <albet70> linux唯一无法忍受的就是systemd...
[12:21] <albet70> 偏偏各大发行版全用systemd,除了gentoo
[12:22] <albet70> 但在笔记本上装gentoo那也很不爽
[12:25] <chobitsbsd> win10 最好的linux发行版
[12:25] <chobitsbsd> O(∩_∩)O哈哈~
[12:29] <imadper> 难道有比systemd好用的init程序?
[12:29] <imadper> 你们这些异教徒
[12:29] <imadper> 烧死
[12:30] <albet70> systemd还只是Init程序吗?
[12:30] <albet70> systemd-homed都有了
[12:30] <imadper> 那不挺好的?
[12:31] <albet70> 以后直接把gnu/linux改名叫gnu/linux/sysmtemd得了
[12:31] <imadper> 叫啥有什么关系呢?
[12:31] <albet70> systemd接管太多东西了
[12:31] <albet70> 已经成了一个巨无霸
[12:52] <imadper> 好事儿啊
[13:00] <chobitsbsd> 相当于模块化了
[13:00] <chobitsbsd> 算是好事儿
[14:14] <albet70> 3x - sinx 是有界的吗?
[15:54] <tangzc> 大家好，来自新人小白的问候
[17:48] <FishOneeyed> 估计这里都只剩下机器人了.
[19:05] <miketang> hi
[19:05] <miketang> 有人吗？
[19:44] <FishOneeyed> mikecao:有
[19:44] <FishOneeyed> 还在吗？