duangsuse::Echo via @vote
看完列表以后觉得怎么样
anonymous poll
我好菜啊 – 1
👍👍👍👍👍👍👍 50%
both – 1
👍👍👍👍👍👍👍 50%
大佬好多
▫️ 0%
👥 2 people voted so far.
anonymous poll
我好菜啊 – 1
👍👍👍👍👍👍👍 50%
both – 1
👍👍👍👍👍👍👍 50%
大佬好多
▫️ 0%
👥 2 people voted so far.
duangsuse::Echo
又给 GeekSpec 写了个小工具(脚本),代码质量依然非常的智障,而且我明显既不考虑设计模式也没多想复用也没有什么高级的东西... 目前 Spectrum (对不起这个酷酷的名字)的打算是作为一个测试工具,以后的重构版本可能支持自己内建 DSL 解析器和更灵活的 API 客户端 endpoints 自动绑定
./spectrum.rb spectrum_geekapk_v1b_api.json
ruby 2.5.3p105 (2018-10-18 revision 65156) [x86_64-linux]
Spectrum v0.1.0: usage: ./spectrum.rb <spec json file> [command]{show,licence,help,json}
[1] pry(#<ClientShowcase>)>This media is not supported in your browser
VIEW IN TELEGRAM
duangsuse::Echo
#FP 现在还没弄懂 Monad 是什么的 duangsuse 感到很难受。但至少稍微了解了一点 Functor,emmm... 🤔 (哭哭)
如果一个月以后还是这么菜的话,那每天晚上早点睡算了,至少我还可以靠脸吃饭(喷)就不用熬夜写代码了(迫 真 自 演)
(无力证明了...)
(瞎玩 inm 梗...)
(无力证明了...)
(瞎玩 inm 梗...)
duangsuse::Echo
又给 GeekSpec 写了个小工具(脚本),代码质量依然非常的智障,而且我明显既不考虑设计模式也没多想复用也没有什么高级的东西... 目前 Spectrum (对不起这个酷酷的名字)的打算是作为一个测试工具,以后的重构版本可能支持自己内建 DSL 解析器和更灵活的 API 客户端 endpoints 自动绑定
现在这个小工具效果还不错,大家可以在见到它的第一个版本,大家有 IDEA / gradle 什么环境的可以下载下来玩玩,目前可以玩这些:
[DuangSUSE@duangsuse]~/文档/geekapk_spring% ./spectrum.rb
json spec 还是 geekspec 都是 SPEC 文件,只不过是表达方式稍有不同而已,本质没有区别。
后面跟 show 可以打印 API 列表、跟 debug 以调试 API 客户端,普通用户不需要调试(因为我测试好了)
./spectrum.rb spectrum_geekapk_v1b_api.json
然后可以进入 REPL
https://github.com/duangsuse/GeekApk/blob/finish_spectrum/spectrum.rb#L260
所有逻辑(命令)都可以在这里查到
我要讲的是 list, list_from, show, status, tree 这几个有用的命令
有四种格式可以选择,plain 只有 URL、return 包含返回值、args 侧重参数、all 全部都有,默认 plain,识别不出选项都是 all
pry -r./spectrum
[1] pry(main)> Spectrum::ClientShowcase
client.instance_api_methods
client.show
client.serverDetail
(当然还有稍微实用一点的玩法,比如 Mapper,具体看这里)
当然 Spectrum 的代码质量虽然垃圾,但也没有垃圾到一定程度,所以还是能用的(迫真)(神逻辑
所以以后,使用 Spectrum 生成其他弱类型/自动内存管理语言的客户端代码,其实也不是不可能,我个人觉得生成 Haskell 的结构然后用 Haskell 翻译也可以(跑(求不喷
Spectrum CLI 是基于 Pry 的,当然以后写 GeekApk CLI 的时候我会另外再写。
[DuangSUSE@duangsuse]~/文档/geekapk_spring% ./spectrum.rb
ruby 2.5.3p105 (2018-10-18 revision 65156) [x86_64-linux]使用
Spectrum v0.1.0: usage: ./spectrum.rb <spec json file> [command]{show,licence,help,json,debug}
./spectrum.rb <spec file> json 来自动解析生成 JSON 文件,多次操作可以节省资源json spec 还是 geekspec 都是 SPEC 文件,只不过是表达方式稍有不同而已,本质没有区别。
后面跟 show 可以打印 API 列表、跟 debug 以调试 API 客户端,普通用户不需要调试(因为我测试好了)
./spectrum.rb spectrum_geekapk_v1b_api.json
然后可以进入 REPL
ruby 2.5.3p105 (2018-10-18 revision 65156) [x86_64-linux]上面写明的就不用说了,用过 Ruby 的 Rubyist(废话)肯定清楚,很方便
Spectrum v0.1.0: usage: ./spectrum.rb <spec json file> [command]{show,licence,help,json,debug}
[i] Faraday connection: conn, Apis: apis, Auth configuration: auth
[+] run show [:apiName|apiNameRegex|apiLocationRegex] to see api documentation, run list to view api list, have fun!
spectrum(0.1)>
https://github.com/duangsuse/GeekApk/blob/finish_spectrum/spectrum.rb#L260
所有逻辑(命令)都可以在这里查到
我要讲的是 list, list_from, show, status, tree 这几个有用的命令
spectrum(0.1)> list 3不带列出全部名称
serverVersion
serverDescription
serverBoot
spectrum(0.5)> list_from :unStar
unStar(aid-path:AppId) -> [$oldCount:number, $newCount:number]
= DELETE /star/{aid}
stargazers(aid-path:AppId) -> array:App
= GET /star/{aid}
stars(uid-path:UserId) -> array:App
= GET /star/user/{uid}
=> 64
spectrum(0.2)> show :serverBoot之前没有考虑到 grep URL 的问题,算了,不如你们弄个 PR。
serverBoot() -> datetime
= GET /serverBoot
spectrum(0.3)> show /server/
serverVersion() -> plain
= GET /serverVersion
serverDescription() -> plain
= GET /serverDescription
serverBoot() -> datetime
= GET /serverBoot
spectrum(0.6)> statustree 可以列出 URL 列表(长得很像树,不过我这里它没被弄成树...)
[+] Total 67 APIs, method count: GET: 37; POST: 8; PUT: 11; DELETE: 11
receiving ["String", "UserId", "Int", "CategoryId", "AppId", "CommentId", "UserSize", "TimelineSize", "NotificationSize", "AppSize", "CommentSize"]
and returning 67 types (["string", "GeekUser", "Category", "App", "AppUpdate", "Timeline", "Notification", "number", "Comment"])
[+] 55 path params, 3 body params
有四种格式可以选择,plain 只有 URL、return 包含返回值、args 侧重参数、all 全部都有,默认 plain,识别不出选项都是 all
spectrum(0.7)> treeSpectrum 可以帮你从 spec 文件映射所有的参数,可选的还是必须的、是否是枚举、它的位置是在 body、query 还是 path... 都会帮你处理好,因为 Spectrum 是主打 CLI,参数不对它还会帮你指正。
GET /serverVersion
GET /serverDescription
spectrum(0.8)> tree :return
GET /serverVersion
= plain
GET /serverDescription
= plain
spectrum(0.9)> tree :args
...
POST /admin/makeUser
* username:String
PUT /admin/resetMetaHash/{uid}
* uid-path:UserId
* shash:String?
spectrum(0.10)> tree :all
...
GET /serverDetail ()
= object:string
POST /admin/makeUser (username:String)
= object:GeekUser
PUT /admin/resetMetaHash/{uid} (uid-path:UserId;shash:String?)
= plain
spectrum(0.1)> listUserSpectrum 也是设计为可以被用于真正的 Ruby GeekApk binding 库,虽然貌似 Faraday 这个 HTTP 客户端不支持异步,我们不是可以用 Fiber 么。实际上我打算之后 Ruby GeekApk CLI 就利用 Spectrum 写。
[!] Arity mismatch: expected 3 (not optional 0), got 0
[*] NOTE: fill first optional argument to get started
listUser(sort:String?{created, followers}, sliceFrom:UserSize?, sliceTo:UserSize?) -> array:GeekUser
= GET user/all
pry -r./spectrum
[1] pry(main)> Spectrum::ClientShowcase
=> Spectrum::ClientShowcase[2] pry(main)> Spectrum::ClientShowcase.from_
Spectrum::ClientShowcase.from_code Spectrum::ClientShowcase.from_file Spectrum::ClientShowcase.from_jsonclient = Spectrum::ClientShowcase.from_file
client.instance_api_methods
client.show
client.serverDetail
(当然还有稍微实用一点的玩法,比如 Mapper,具体看这里)
当然 Spectrum 的代码质量虽然垃圾,但也没有垃圾到一定程度,所以还是能用的(迫真)(神逻辑
所以以后,使用 Spectrum 生成其他弱类型/自动内存管理语言的客户端代码,其实也不是不可能,我个人觉得生成 Haskell 的结构然后用 Haskell 翻译也可以(跑(求不喷
Spectrum CLI 是基于 Pry 的,当然以后写 GeekApk CLI 的时候我会另外再写。
GitHub
duangsuse/GeekApk
GeekApk, the dying SpringBoot(a.k.a. Sping initializr) server for GeekApk(a.k.a 极安) (R - duangsuse/GeekApk
duangsuse::Echo
现在这个小工具效果还不错,大家可以在见到它的第一个版本,大家有 IDEA / gradle 什么环境的可以下载下来玩玩,目前可以玩这些: [DuangSUSE@duangsuse]~/文档/geekapk_spring% ./spectrum.rb ruby 2.5.3p105 (2018-10-18 revision 65156) [x86_64-linux] Spectrum v0.1.0: usage: ./spectrum.rb <spec json file> [command]{show,licence…
公正评价:目前 duangsuse 写很多弱类型语言的时候,尤其像 #Ruby 这种非常灵活(无论语法还是 inspect)的语言
该灵活的不灵活(该抽提的东西 hard code、该做成独立模块的绑在一块胡乱引用、该弄设计模式我偏要用 block 还不带文档),不该灵活的乱灵活(疯狂胡乱返回各种类型的对象,然后疯狂 Kernel#is_a? 判断处理...),设计毫无章法和规范、不考虑性能不注意算法,想哪里写哪里,怎么感觉 dalao 怎么写,控制流胡乱搞、代码健壮性很不行、软件测试完全没有考虑、注释胡乱放废弃代码也只是胡乱注释掉,似乎没有基本规格...
大概这就是所谓的脚本小子吧。
真真还不如 statically checked 弄设计模式 trait bounds 算了...
该灵活的不灵活(该抽提的东西 hard code、该做成独立模块的绑在一块胡乱引用、该弄设计模式我偏要用 block 还不带文档),不该灵活的乱灵活(疯狂胡乱返回各种类型的对象,然后疯狂 Kernel#is_a? 判断处理...),设计毫无章法和规范、不考虑性能不注意算法,想哪里写哪里,怎么感觉 dalao 怎么写,控制流胡乱搞、代码健壮性很不行、软件测试完全没有考虑、注释胡乱放废弃代码也只是胡乱注释掉,似乎没有基本规格...
大概这就是所谓的脚本小子吧。
真真还不如 statically checked 弄设计模式 trait bounds 算了...
duangsuse::Echo
人生苦短用 Python
Python 和 Ruby 这两种大佬语言都不需要给那些 PLT/FP 大佬们来用的
大佬们看得起 JavaScript 都懒得用 Ruby
大佬们看得起 JavaScript 都懒得用 Ruby
duangsuse::Echo
Python 和 Ruby 这两种大佬语言都不需要给那些 PLT/FP 大佬们来用的 大佬们看得起 JavaScript 都懒得用 Ruby
This media is not supported in your browser
VIEW IN TELEGRAM
duangsuse::Echo
现在这个小工具效果还不错,大家可以在见到它的第一个版本,大家有 IDEA / gradle 什么环境的可以下载下来玩玩,目前可以玩这些: [DuangSUSE@duangsuse]~/文档/geekapk_spring% ./spectrum.rb ruby 2.5.3p105 (2018-10-18 revision 65156) [x86_64-linux] Spectrum v0.1.0: usage: ./spectrum.rb <spec json file> [command]{show,licence…
在 GeekApk 项目正式启用 Spectrum (是的... GeekApk 有自己的一套『Swagger Tools』,OpenAPI 3.0 也就是 GeekSpec 0.1、Swagger codegen 也就是 Spectrum 0.1.0)之前,我打算用 Times 先测试一下它是否真的能用(确信
(目前看来,几乎是无论做什么请求,GA SB 均会给出类似如下响应)
(是的,Spectrum 还不够成熟,我去重构...)
如果 Spctrum 的确是可用的,那我将使用它来编写 GeekApk 服务器的黑盒测试逻辑(而 JUnit 则仅负责链接测试服务和这些测试逻辑,Ruby 负责实际执行他们,可能需要一些时间,我不想多花时间了解接口所以这部分我宁愿多写点模板代码,而不是写插件什么的),目前 Spectrum 可能只能在 POSIX 平台上用(部分功能依赖 Node.JS),总之 GeekApk 现在可能不会太考虑 POSIX 外的平台移植问题。
(目前看来,几乎是无论做什么请求,GA SB 均会给出类似如下响应)
spectrum(0.2)> listUser 'created'(好吧,其实更多的是 OperationNotImplemented...)
=> {"timestamp"=>1549876643013,
"status"=>500,
"error"=>"Internal Server Error",
"message"=>"Optional int parameter 'sliceFrom' is present but cannot be translated into a null value due to being declared as a primitive type. Consider declaring it as object wrapper for the corresponding primitive type.",
"path"=>"/user/all"}
(是的,Spectrum 还不够成熟,我去重构...)
如果 Spctrum 的确是可用的,那我将使用它来编写 GeekApk 服务器的黑盒测试逻辑(而 JUnit 则仅负责链接测试服务和这些测试逻辑,Ruby 负责实际执行他们,可能需要一些时间,我不想多花时间了解接口所以这部分我宁愿多写点模板代码,而不是写插件什么的),目前 Spectrum 可能只能在 POSIX 平台上用(部分功能依赖 Node.JS),总之 GeekApk 现在可能不会太考虑 POSIX 外的平台移植问题。
GitHub
geekapk-r/Times
Simple commentable news for geekapk(deprecated). Contribute to geekapk-r/Times development by creating an account on GitHub.
Forwarded from duangsuse Throws
这位先生也真是 🌚👍厉害厉害。
服,服,服。
可惜我没有某先生那么好的口才、没有大佬们那么犀利的语言,不然这种情况,这个大佬恐怕是要被公裁了(实际上已经是这样了)。
值不值:你骂得越多,他赚得越多
我的回答是不值,所以我选择不回骂他。
既然侯先生要拿这事说话,而且丝毫不顾及一点道德行为规范也不像机器人,我想请问我哪天在哪里问候过除了先生您之外您优秀的家人们了。
我非常诚恳地相信,您妈对她的儿子有这样优秀的语言和行为一定是无比的骄傲和自豪吧。为国争光在被国墙了的 Telegram 上举报不法翻墙。
也衷心祝愿先生您能在反违法 fq 的路上越走越远,离实际越走越远。
到时候已经肉身翻墙的人们可能会在墙外对着自己的孩子指着您,说千万别学这个人,和『不『法』』翻墙斗争一生,结果既没有做到什么有意义的事情,也没有被任何有关部门采纳自己的优秀情报,而且连墙是怎么工作的都不知道。
真的是两边走不通啊。
服,服,服。
可惜我没有某先生那么好的口才、没有大佬们那么犀利的语言,不然这种情况,这个大佬恐怕是要被公裁了(实际上已经是这样了)。
值不值:你骂得越多,他赚得越多
我的回答是不值,所以我选择不回骂他。
既然侯先生要拿这事说话,而且丝毫不顾及一点道德行为规范也不像机器人,我想请问我哪天在哪里问候过除了先生您之外您优秀的家人们了。
我非常诚恳地相信,您妈对她的儿子有这样优秀的语言和行为一定是无比的骄傲和自豪吧。为国争光在被国墙了的 Telegram 上举报不法翻墙。
也衷心祝愿先生您能在反违法 fq 的路上越走越远,离实际越走越远。
到时候已经肉身翻墙的人们可能会在墙外对着自己的孩子指着您,说千万别学这个人,和『不『法』』翻墙斗争一生,结果既没有做到什么有意义的事情,也没有被任何有关部门采纳自己的优秀情报,而且连墙是怎么工作的都不知道。
真的是两边走不通啊。
spectrum(0.6)> conn.url_prefix = 'http://0.0.0.0:234'
=> "http://0.0.0.0:234"
spectrum(0.7)> apiVersion
=> "0.1.0"
Spectrum 可以十分成功的完成基本接入...
不过,其实 Spectrum 的代码质量不怎么样(甚至对于目前的一些 Ruby 应用来说,要加个『很』字才行)
用打开类修改需要修改的方法,凑合着用吧... 🤔(把技术债务压给 Ruby 的元编程灵活性解决)
=> "http://0.0.0.0:234"
spectrum(0.7)> apiVersion
=> "0.1.0"
Spectrum 可以十分成功的完成基本接入...
不过,其实 Spectrum 的代码质量不怎么样(甚至对于目前的一些 Ruby 应用来说,要加个『很』字才行)
用打开类修改需要修改的方法,凑合着用吧... 🤔(把技术债务压给 Ruby 的元编程灵活性解决)
#Github 湖北襄阳这里偶尔有时候出现 SSL 证书异常,不知道你们有没有 🤔
duangsuse::Echo
累死,算是学习(确信)了一下 Ruby 和测试了 Spectrum... 感觉解耦合做得不是很好,response mapper 根本一点用都没有(因为要很多 mapper 必须要拿到一个 ClientShowcase 实例),另外给 ClientShowcase 添加一个 Hash 表来放诸如密码这样的东西隐式传递不错),考虑重构。
Times 是之前老 GeekApkR 里唯一一个能用的后端服务... Ruby + Sinatra 写的,其实现在看来都很不良实践(跑)
凑字数(代码行数)吧(
不过它的测试套件也算完整,虽然持久化层的不是 Mock,但也可以用,缺点是如果在生产环境用了很可能导致数据丢失
Times 没有使用 DBMS,而是,这是因为我以为它不会有太大的数据集性能要求,我觉得很可以重构(比方说,使用类似 MongoDB 的面向文档数据库替换纯手动)... 尤其是难看的 API...
值得注意的是我以前智商还低一些的时候,连常用的序列化这种弱智能力都没有...
JSON 序列化(Times 的数据持久化方式)当时非常的混乱,我非常智障的套模板(或许,因为我想我那时就是瞎搅合...)
我没有么写:
凑字数(代码行数)吧(
不过它的测试套件也算完整,虽然持久化层的不是 Mock,但也可以用,缺点是如果在生产环境用了很可能导致数据丢失
Times 没有使用 DBMS,而是,这是因为我以为它不会有太大的数据集性能要求,我觉得很可以重构(比方说,使用类似 MongoDB 的面向文档数据库替换纯手动)... 尤其是难看的 API...
值得注意的是我以前智商还低一些的时候,连常用的序列化这种弱智能力都没有...
JSON 序列化(Times 的数据持久化方式)当时非常的混乱,我非常智障的套模板(或许,因为我想我那时就是瞎搅合...)
我没有么写:
[foo, bar, baz].to_json而是:
[foo, bar, baz].map { |o| o.to_json }.to_json
然后反序列也一样... rofl.
duangsuse::Echo
Times 是之前老 GeekApkR 里唯一一个能用的后端服务... Ruby + Sinatra 写的,其实现在看来都很不良实践(跑) 凑字数(代码行数)吧( 不过它的测试套件也算完整,虽然持久化层的不是 Mock,但也可以用,缺点是如果在生产环境用了很可能导致数据丢失 Times 没有使用 DBMS,而是,这是因为我以为它不会有太大的数据集性能要求,我觉得很可以重构(比方说,使用类似 MongoDB 的面向文档数据库替换纯手动)... 尤其是难看的 API... 值得注意的是我以前智商还低一些…
回来了(因为身体素质真的开始有点 🌶🐔 了,而且非常需要休息,然后老是熬夜容易变丑,虽然其实长的就不咋地,大嘘),顺便添了一些任务
1. 部署文档添加 Systemd 低端口权限配置提示(服务程序部署安全,这样如果我们的 upstream 有严重的,例如 RCE、可以拿 Shell 的安全问题别人不至于一下子迫真
2. 把所有 Endpoint mapping 的 Int? 换成
3. 为了 Clients 数据交换开心,添加 PATCH Json API(现在创建用户之后可以直接拿 JSON 去 patch 属性了,不用一个一个属性去 update)
(现在还不是 RESTful 的)
4. 添加用户和管理员权限验证的 Middleware(WebFilter)、其中用户的权限验证和 Rate Limit 一起做(GeekHits API 也一起开放了)
5. 为 CI Intergation 添加 Node.JS 和 MRI Ruby 依赖,并且开始使用外围的 Spectrum Ruby 客户端接口测试(从 JUnit 启动服务器和 RSpec 客户端自动化测试程序)
GeekApk v1b 完成后可能有别的打算(包括 Android 客户端,不准喷我不会什么设计模式)(有些人不准喷我菜...)(虽然我有时候的确很菜,但我自己觉得我很有前途,嗯嗯。)
希望以后都是艳阳高照。冻死了天又黑...
1. 部署文档添加 Systemd 低端口权限配置提示(服务程序部署安全,这样如果我们的 upstream 有严重的,例如 RCE、可以拿 Shell 的安全问题别人不至于一下子迫真
rm -rf / 殃及池鱼)2. 把所有 Endpoint mapping 的 Int? 换成
java.lang.Integer? (要不然错误,说 int 不能是 optional 的,虽然本来有默认值 0)3. 为了 Clients 数据交换开心,添加 PATCH Json API(现在创建用户之后可以直接拿 JSON 去 patch 属性了,不用一个一个属性去 update)
(现在还不是 RESTful 的)
4. 添加用户和管理员权限验证的 Middleware(WebFilter)、其中用户的权限验证和 Rate Limit 一起做(GeekHits API 也一起开放了)
5. 为 CI Intergation 添加 Node.JS 和 MRI Ruby 依赖,并且开始使用外围的 Spectrum Ruby 客户端接口测试(从 JUnit 启动服务器和 RSpec 客户端自动化测试程序)
GeekApk v1b 完成后可能有别的打算(包括 Android 客户端,不准喷我不会什么设计模式)(有些人不准喷我菜...)(虽然我有时候的确很菜,但我自己觉得我很有前途,嗯嗯。)
希望以后都是艳阳高照。冻死了天又黑...
duangsuse::Echo
Times 是之前老 GeekApkR 里唯一一个能用的后端服务... Ruby + Sinatra 写的,其实现在看来都很不良实践(跑) 凑字数(代码行数)吧( 不过它的测试套件也算完整,虽然持久化层的不是 Mock,但也可以用,缺点是如果在生产环境用了很可能导致数据丢失 Times 没有使用 DBMS,而是,这是因为我以为它不会有太大的数据集性能要求,我觉得很可以重构(比方说,使用类似 MongoDB 的面向文档数据库替换纯手动)... 尤其是难看的 API... 值得注意的是我以前智商还低一些…
#Math Tips: 为什么任何数乘 0 都得 0,乘 1 都得原数?(放松一下系列)
(好吧,虽然我平时都不是很轻松(大嘘))
考虑一下自然数(正整数)的定义
那么 1 就是
那么,对于 Nat 这个 GADT(不准喷为什么用 GADT 而不是 plain 一点的 struct 或者 OO 的 class),怎么定义加法呢?
很简单,
当然 fold 是针对列表的,而且这里插入操作可能很迫真而且没有太大意义,而且我的智商很低,所以就不用。
那么乘法是什么呢?
数学告诉我们,乘法就是
一样很简单,
那么我们就可以做一个非常 immediate 的归纳证明(大嘘)
就是说
第二个我们可以考虑一下展开:
,只是我读书少不知道是不是应该怎么着才算是完成了(的确是比较
只要证明了
唉我数学还是差了,别打我,我是从数学书上看的数学归纳法(暴论)
首先我们(为了方便)证明为什么任何数 + 0 还得原数,换句话说,
add Zero n = n (1)
add n Zero = n (2)
(1) 直接得证不用说
对于 (2) 么
add Zero Zero = Zero (3)
add (Succ m) Zero = add m (Succ Zero) (4)
考虑我们的 Nat GADT,任何 Nat 只能是:
- Zero
- 另一个 Nat 的 Succ
证明等式 (2)
add Zero Zero = Zero
add (Succ m) Zero = add m (Succ Zero)
因为那个 Nat 的确是 Coinductive 的所以我只能这么做了(迫真)
为什么说是 Coinductive 呢?
inductive 的长什么样子呢?
证明不下去了... 太不熟悉了,耗时间...
(好吧,虽然我平时都不是很轻松(大嘘))
考虑一下自然数(正整数)的定义
data Nat = Zero | Succ Nat我们这么说:一个自然数可能是零,也可以是另一个自然数的『后继元(Succeeder)』
那么 1 就是
Succ Zero(1 + 0)、3 就是 Succ (Succ (Succ Zero)) (1 + 1 + 1 + 0)那么,对于 Nat 这个 GADT(不准喷为什么用 GADT 而不是 plain 一点的 struct 或者 OO 的 class),怎么定义加法呢?
很简单,
add :: Nat -> Nat -> Nat因为逻辑实在太弱智(是的,喷的是我自己弱智)所以不讲
add Zero n = n
add (Succ m) n = (add m (Succ n))
当然 fold 是针对列表的,而且这里插入操作可能很迫真而且没有太大意义,而且我的智商很低,所以就不用。
那么乘法是什么呢?
数学告诉我们,乘法就是
n × 0 = 0对于 Nat 怎么定义乘法呢?
n × 1 = n
n × 2 = n + n
n × 3 = n + n + n
n × m = n (+ n){repeat for m - 1 times}
一样很简单,
mul :: Nat -> Nat -> Nat因为我比较菜,而且这个问题非常弱智,所以我们来检验一下:
mul Zero n = Zero
mul (Succ m) n = (add n (mul m n))
natToInt :: Nat -> Int最后的代码 #Haskell
natToInt Zero = 0
natToInt (Succ m) = (natToInt m) + 1
five = Succ (Succ (Succ (Succ (Succ Zero))))
one = Succ Zero
two = Succ one
three = Succ two
data Nat = Zero | Succ Nat== 那么,为什么任何数乘 0 都得零?
add :: Nat -> Nat -> Nat
add Zero n = n
add (Succ m) n = (add m (Succ n))
mul :: Nat -> Nat -> Nat
mul Zero n = Zero
mul (Succ m) n = (add n (mul m n))
natToInt :: Nat -> Int
natToInt Zero = 0
natToInt (Succ m) = (natToInt m) + 1
five = Succ (Succ (Succ (Succ (Succ Zero))))
one = Succ Zero
two = Succ one
three = Succ two
main = do
print $ natToInt (add one three)
putLine
foldl (>>) (putLine) os
putLine
print $ natToInt (add three five)
putLine
printNat $ mul three five
printNat $ mul five three
printNat $ mul Zero five
where printNat = (print . natToInt)
os = print <$> (natToInt <$> [one, two, three, five])
putLine = putStrLn []
mul Zero one = Zero这个逻辑简单易懂,因为 mul 的定义就是这个
mul one Zero =对于
add Zero (mul Zero Zero)
mul one Zero 是的,但是我们肯定要问是不是对于所有 Nat "n" 都有 mul n Zero = Zero 这个等式成立那么我们就可以做一个非常 immediate 的归纳证明(大嘘)
就是说
mul Zero Zero = Zero第一个等式肯定成立不用说(基线,数学上叫奠基,只求你们别喷我知乎
mul (Succ _) Zero = Zero
@证明 民科,我一直在做科普从来没有做什么民科的意向...)第二个我们可以考虑一下展开:
mul (Succ m) Zero = (add Zero (mul m Zero))好吧,这个不是递推的,所以我们换个角度考虑,首先我们证明
mul one Zero = Zero,它是成立的(考虑 add 的定义)mul (Succ Zero) Zero = (add Zero (mul Zero Zero))然后是
mul (Succ one) Zero = Zero
mul (Succ qa1) Zero = (add Zero q1) = Zero我们(求不打)注意到对于任何 Nat (Succ m),都有 mul m Zero = (add (mul m Zero) Zero)
where qa1 = (Succ Zero)
q1 = (mul (Succ Zero) Zero)
,只是我读书少不知道是不是应该怎么着才算是完成了(的确是比较
只要证明了
(add Zero Zero) 是 Zero,是不是就可以说 ∀o∈Nat. mul o Zero = Zero 呢?(迫真自演)唉我数学还是差了,别打我,我是从数学书上看的数学归纳法(暴论)
首先我们(为了方便)证明为什么任何数 + 0 还得原数,换句话说,
add Zero n = n (1)
add n Zero = n (2)
(1) 直接得证不用说
对于 (2) 么
add Zero Zero = Zero (3)
add (Succ m) Zero = add m (Succ Zero) (4)
考虑我们的 Nat GADT,任何 Nat 只能是:
- Zero
- 另一个 Nat 的 Succ
证明等式 (2)
add n Zero = n 可以转化为证明等式 (3) 和 (4)add Zero Zero = Zero
add (Succ m) Zero = add m (Succ Zero)
add (Succ Zero) Zero
= add Zero (Succ Zero)
= (Succ Zero)(其实我感觉我是在给加法证明交换律,可是我太菜证明不了 23333)
add (Succ m) Zero
= add m (Succ Zero)
因为那个 Nat 的确是 Coinductive 的所以我只能这么做了(迫真)
为什么说是 Coinductive 呢?
inductive 的长什么样子呢?
((+1) . sum) = fold (+) 1这个是往 sum [] 的方向弄的... 上面那个的 Nat GADT 好像不是(跑)(但应该也是 inductive 的,我太垃圾还不能理解)
sum[ ]+ 1 = 1
sum(x:xs) + 1 =x+(sum xs+ 1)
sum [] + 1
= 0 + 1
= 1
sum (x:xs) +1
= (x + sum xs) + 1
= x + (sum xs + 1)
证明不下去了... 太不熟悉了,耗时间...