duangsuse::Echo
彻底给跪,我重写一个普适性不那么强的吧...
还不如我给
说起来,Java 也不给内置一个动态 Number 自动转换提升功能... 非得都成 BigInteger 或者都成 Long 再转换好低效的说...
java.awt.image.BufferedImage 和 typealias Point2D = Pair<Axis2D, Axis2D> 写的 operator extension 好用呢...说起来,Java 也不给内置一个动态 Number 自动转换提升功能... 非得都成 BigInteger 或者都成 Long 再转换好低效的说...
duangsuse::Echo
还不如我给 java.awt.image.BufferedImage 和 typealias Point2D = Pair<Axis2D, Axis2D> 写的 operator extension 好用呢... 说起来,Java 也不给内置一个动态 Number 自动转换提升功能... 非得都成 BigInteger 或者都成 Long 再转换好低效的说...
立刻告一段落,实在是太花时间了 没时间写编译器了
GitHub
duangsuse-valid-projects/Essay-Kotlin-AsciiArt
Kotlin ascii art generator. Contribute to duangsuse-valid-projects/Essay-Kotlin-AsciiArt development by creating an account on GitHub.
duangsuse::Echo
开源在 GitHub:Essay-DIP-BMP-SIMD-Operation 正在准备完成剩下的东西... 这周事情挺多的,看来又是做不完 👉 Essay-Fibonacci-Generator Essay-Cached-Factorial-Stream Essay-Java-Annotations (Runtime, Processor, Andriod) JavaPrefer (Preference DSL) Essay-Android-Lime-Tokenize (Fragments & Item…
看起来全 TM 没时间写了,不过不要紧,因为过两天高考放假(这里希望各位都能取得好成绩哦~我知道很多同学也都是很努力的,努力就一定有收获呢)
我还会回来的~ 🐱
所以,我要先巩固一下 LLVM Cookbook 的学习结果
写一下 Toy 语言的前端和代码生成器、JIT、FunctionPass
这些是编译器工程师的基本操守,大概从会写 (for LLVM like frameworks) Pass 开始就算是一个 CE 了,加油哦。
我还会回来的~ 🐱
所以,我要先巩固一下 LLVM Cookbook 的学习结果
写一下 Toy 语言的前端和代码生成器、JIT、FunctionPass
这些是编译器工程师的基本操守,大概从会写 (for LLVM like frameworks) Pass 开始就算是一个 CE 了,加油哦。
duangsuse::Echo
看起来全 TM 没时间写了,不过不要紧,因为过两天高考放假(这里希望各位都能取得好成绩哦~我知道很多同学也都是很努力的,努力就一定有收获呢) 我还会回来的~ 🐱 所以,我要先巩固一下 LLVM Cookbook 的学习结果 写一下 Toy 语言的前端和代码生成器、JIT、FunctionPass 这些是编译器工程师的基本操守,大概从会写 (for LLVM like frameworks) Pass 开始就算是一个 CE 了,加油哦。
这个编译器接受这样的语法,它的 tokenizer 基本是使用 libc 的 API(e.g. isalpha, isalnum, isspace from ctype.h)弄的
然后数值的解析基本都是 atoi, strtod 什么的。
这里,因为我实在是没有时间,所以支持特性的很少
以后我会给它增添浮点类型(就是所谓的 “两种基本类型:Long integer 和 Double Prec floating point,不支持类型组合”)first-class 支持
和支持 hex, binary 字面数值
— 语言部分
这是一门简单的计算器语言:它支持 Int 值,可以进行 +, -, *, / 操作
可以进行 function definition:
数值:C
标识符(名字): C
空格:C
注释:支持行注释,以
好吧,因为原版支持了
关键字在词法上和标识符采取一样的规则:
type { name "add2"; args (!!) ["x"] }
body {
Expr {
me IdentRef(ident("x")); op '+';
rhs NulLit(number(2))
}
}
} (1)
REPL 其实就是
比如
然后数值的解析基本都是 atoi, strtod 什么的。
这里,因为我实在是没有时间,所以支持特性的很少
以后我会给它增添浮点类型(就是所谓的 “两种基本类型:Long integer 和 Double Prec floating point,不支持类型组合”)first-class 支持
和支持 hex, binary 字面数值
— 语言部分
这是一门简单的计算器语言:它支持 Int 值,可以进行 +, -, *, / 操作
可以进行 function definition:
def <name> ArgList Expr
Tokens数值:C
isdigit+标识符(名字): C
isalpha isalnum*空格:C
isspace+注释:支持行注释,以
# 开始直到 "\n", 换句话说,自动支持 CRLF 和 LF, 可怜的 Windows!(默认 CR \r)好吧,因为原版支持了
\r,我也支持一下算了,于是 Windows 也可以用data TokenEOF:因为不用 EOFException,什么?Haskell 为什么不用 Maybe 或者 Exception Monad?因为这是要用 C 写的!
= Num Int | Iden String
| Spaces Count | Comment String
| KwDef | ExpGrouper Bool
| Operator | EOF
关键字在词法上和标识符采取一样的规则:
def只要不是上面任何一种,即为 Operator,支持:
() 作为表达式组合的标记, 作为列表分割的记号infixl + < - < * < /
就有这样的语法 EBNF 规则,首先我们想的是 def 定义函数,entry 规则是一个表达式组,我们可以像 REPL 一样用:Entry -> Expr这样就可以弄出这些示例:
TERMINATOR def, extern
TERMINATOR SYMBOL +, -, *, /, COMMA, (, )
Expr -> Primary . "BinRhs" (binop Primary)*
where binop -> '+' | '-' | '*' | '/'
Params -> Expr (',' Expr)* -- Recursive
Names -> ident (',' ident)*
Primary ->
"Derefing" (IdentRef | IdentCall) | NumLit | ParenExpr
where
ParenExpr -> '(' Expr ')' -- Recursive
NumLit -> number
IdentRef -> ident
IdentCall -> ident '(' Params? ')'
— Function
FunTypedef -> ident '(' Names? ')'
ExternFun -> extern FunTypedef
DefFun -> def FunTypedef Expr
def add2(x) x +2
DefFun {type { name "add2"; args (!!) ["x"] }
body {
Expr {
me IdentRef(ident("x")); op '+';
rhs NulLit(number(2))
}
}
} (1)
def sub1mul3(x) (x-1)*3
def add(x, y) x + y
def sumWeight(x, wei) (x-1) + wei*10然后我们又是分开来 handle FunDef 和 Expression 的求值的
REPL 其实就是
forever do {
expr = parse!(gets)
expr.evaluate!
}
其中 Expr.evaluate!
when expr {
is Expr -> puts this.treeEvaluate!
is ExternFun -> module.externFunction(this.type)
is DefFun -> module.createFunction(this.type, this.body.compileAll())
otherwise -> error("Cannot handle expression $this.name")
}
比如上面的例子 (1),只需后序遍历 AST 就可以面向某种目标生成代码:walk DefFun {
val signature = type.createSignature()
unless my_module.hasExtern(signature) and my_module.hasDefinition(signature)
my_module.createFunction(signature, body.walk())
else error("Defined function does not match (for $signature)")
}
walk Expr: Value {
return when op {
'+' then Builder.createI32Add(me.walk(), rhs.walk(), "sum")
otherwise error("Unknown operator $op")
}
}
walk IdentRef: Value {
return scope.get(name).mapError { error("Failed to resolve symbol in context $scope.ctx") }
}
walk NumLit: Value {
ConstantInt.get(Types::getInt32Ty(my_ctx), value)
}
LLVM 是基于 SSA 架构的,这个架构假设 LLVM 有无数个机器寄存器,它的指令结构是线性的,但是任何指令的结果都可以被其他指令引用而无须显示指定目标存储器,这样的指令虽然是线性序列,但实际上可以被归纳到树形结构或者从树形结构被创建比如
data Ast = Lit Int | Add Ast Ast(Haskell)eval :: Ast -> Int上面的 walker 对于 (1) 应该能生成这种代码(LLVM IR)
eval (Lit x) = x
eval (Add lhs rhs) = eval lhs + eval rhs
evalSsa :: Ast -> Value
eval (Lit x) = constInt x
eval (Add lhs rhs) = add (eval lhs) (eval rhs)
define i32 @add2 (i32 %x) {
entry:
%sum = add i32 %x, 2
ret i32 %sum
}
这是对 Ast 进行后序遍历(一种括扑排序)的结果,当然有多少个 Add 都一样,结果肯定是正确的def add2_3(x) 3+(x+2)
define i32 @add2 (i32 %x) {
entry:
%sum = add i32, %x, 2
%sum1 = add i32 %sum, 3
ret i32 %sum1
}
duangsuse::Echo
这个编译器接受这样的语法,它的 tokenizer 基本是使用 libc 的 API(e.g. isalpha, isalnum, isspace from ctype.h)弄的 然后数值的解析基本都是 atoi, strtod 什么的。 这里,因为我实在是没有时间,所以支持特性的很少 以后我会给它增添浮点类型(就是所谓的 “两种基本类型:Long integer 和 Double Prec floating point,不支持类型组合”)first-class 支持 和支持 hex, binary…
试用! #CE
source_filename = "add.ll"
!llvm.module.flags = !{!0}
!llvm.ident = !{!1}
!0 = !{i32 1, !"wchar_size", i32 4}
!1 = !{!"duangsuse version ??? (Fedora 7.0.1-6.fc29)"}
@.fmt = private unnamed_addr constant [9 x i8] c"res: %i\0a\00", align 1
[DuangSUSE@duangsuse]~/projects% lli add.ll
res: 8
source_filename = "add.ll"
!llvm.module.flags = !{!0}
!llvm.ident = !{!1}
!0 = !{i32 1, !"wchar_size", i32 4}
!1 = !{!"duangsuse version ??? (Fedora 7.0.1-6.fc29)"}
define i32 @add2_3 (i32 %x) {
entry:
%sum = add i32 %x, 2
%sum1 = add i32 %sum, 3
ret i32 %sum1
}
declare i32 @printf(i8*, ...) @.fmt = private unnamed_addr constant [9 x i8] c"res: %i\0a\00", align 1
define i32 @main (i32, i8**) {
enrty:
%res = call i32 (i32) @add2_3(i32 3)
%_r = call i32 (i8*, ...) @printf(i8* getelementptr inbounds ([9 x i8], [9 x i8]* @.fmt, i32$
ret i32 0
}
—[DuangSUSE@duangsuse]~/projects% lli add.ll
res: 8
Forwarded from XiNGRZ's (XiNGRZ)
响应国家号召,本频道明天将进行技术升级,停更一天。
#PL #PLT 推荐,当然本频道之前也有讲类似的东西,非常感谢 LEXUGE 一直能关注这种弱鸡频道...(是的,在同为非应用向编程的人前我丝毫不会感觉自己容易被喷、或者对方要秀我一脸什么的,而且也不会莫名“自大” — 这类人显然在我说些可能他们还没学到的东西时候不会有任何不适感,各弄各的) 因为我在 GitHub 更新上看到他 Star 我最近改名的一个 repo,说起来,最近大家(一些可以认为是『学院派』一点的博主)都开始用纯 English 写作了,有点看不懂的样子,看来英文还是得学啊
Telegram
duangsuse::Echo
+ Intersection type
Intersection types are types describing values that belong to both of two other given types with overlapping value sets.
For example, in most implementations of C the signed char has range -128 to 127 and the unsigned char has range…
Intersection types are types describing values that belong to both of two other given types with overlapping value sets.
For example, in most implementations of C the signed char has range -128 to 127 and the unsigned char has range…
https://github.com/DirClean/BackwardParser #life #dev 唉,果然还是没法逃过应用向的追击嘛。只是花了整整一天的时间而已,使用了 Java 的 IO、File、Gson 和 Kotlin 语言设计的 :: reference、clinit block,虽然我不清楚是不是翻译器生成的,不过要生成那玩意怕不是翻译器有点高级(因为需要把一个 nullable 翻译成 lateinit,空判断也要翻译好)(为什么?是因为它很 Kotlin,但是不够 Kotlin,排除 const val 而不是 enum 这类无关紧要的问题外,它居然使用了 System.out.println 而不是 kotlin 的 ForceInline 的 println 函数,虽然)比如 Java 8 的 Stream(StreamSupport.stream(?, boolean);Spliterator.spliteratorUnknownSize;Gson 的 JsonElement、JsonObject;函数式编程都常用的 map 操作;Kotlin 里自己明明都... 抑或是 Spring ORM Repositories 里的 findFirst),虽然我对 Stream 的理解还是有的,可是还是莫名觉得威胁....
我果然还是不喜欢应用,看来 Yuuta 开发的速度果然是变快了呢,但是总是觉得自己虽然,工程向的人总是还不够令人满意呢... 不够包容
总是觉得会被喷,现在看来只会越来越严重了呢... 我也必须得赶快想想办法... 虽然对我来说阅读堆砌的逻辑已经不存在任何难点了,有没有办法证明我自己也能来写这些有时候会用所谓不常用抽象和逻辑的代码呢?
可能还是我不够包容吧... 为什么我会变成对那些写了很多东西但都是『不够学术向』的人有被害倾向的说呢?
记得刚才看见 Trumeet/XXXParser 的时候立刻就点进去看了,大概是害怕自己的技能会被轻易复制的那种吧。我果然还是有病。
顺便说一下,Trumeet 的英文语法水平值得练习一下,虽然我的语法也很差,但是 Trumeet 这里似乎的确有点很容易发现的语法错误,我想即便是初中生的话也大概是不能容忍的吧。
说实在话,我觉得为什么很多人的洋文语法都比我还辣鸡... 虽然我是从小训练语感稍微强一点啦
英文歌唱起来稍微有点困难,某些连音就不会连,但是音标上也开始到感受到所谓音位音标和音素音标的区别了呢,看起来语音学这种启蒙的课程也是很有用的...
https://github.com/DirClean/BackwardParser/blob/master/src/main/kotlin/moe/yuuta/ruleconverter/SourceParser.kt#L198
最后一段时间我看了一下这个函数,顿时觉得好魔法,虽然逻辑很易懂但是我弄不清 Name 是什么以及所谓的 RelativePath 是怎么单单通过最后的一个“append”操作加上自己的目录什么的弄出来的
我果真是老了么...
val path = file.absolutePath.substring(baseFolder.absolutePath.length)
啊终于知道了...val paths = path.split(Pattern.compile(File.separator))
这里 path 是一个 String;file 是一个 kotlin.io.File /* alias for java.io.File in Kotlin JVM */噢终于知道这是干什么的了,为啥不直接用 File 的 getRelativePath(因为这是 VFS,虚拟文件系统操作,文件夹,或者说树路径的名字是有语义的)
不过函数式编程的话可以这么写(抽象一个
VFS.simplifiedFile (Dir) Name(String): String 出来):typealias FilePath = String
private fun relativePath(file: kotlin.File): FilePath {
// 首先我们拿到相对 base dir 的 file path(直接通过路径线性表,噢不是 String 的 subseq)
val relCanonicalPath = file.absolutePath.subsequence((myBaseDir as FilePath).size).split(File.seprator)
// 然后直接 foldl 好了,至于如何解决最后一个文件名字的问题,不是可以先 subseq,反正性能不敏感
// Empty 的情况... 虽然我觉得不太可能,直接在 VFS 里面处理呗、异常直接传递或者捕获,如果捕获目的只能是为了提示这是第一次循环,当然 fold 又是不计数的...
val dirPath = relCanonicalPath.let { it.subsequence(0, it.size -1) }.fold(StringBuilder()) { ac, x -> ac.append(VFS.simplifiedDirName(x)).append(File.seprator) }
dirPath.append(VFS.simplifiedFileName(relCanonicalPath.last.name))
// 然后
return dirPath.toString()
}
至于异常什么的就传递吧,毕竟这个操作把异常吞掉什么的,可能这还不属于应用本身的逻辑,这一层不用处理异常呢GitHub
DirClean/BackwardParser
A rule parser to convert rules for Dir clients which are below 2.0 - DirClean/BackwardParser
duangsuse::Echo
https://github.com/DirClean/BackwardParser #life #dev 唉,果然还是没法逃过应用向的追击嘛。只是花了整整一天的时间而已,使用了 Java 的 IO、File、Gson 和 Kotlin 语言设计的 :: reference、clinit block,虽然我不清楚是不是翻译器生成的,不过要生成那玩意怕不是翻译器有点高级(因为需要把一个 nullable 翻译成 lateinit,空判断也要翻译好)(为什么?是因为它很 Kotlin,但是不够 Kotlin,排除…
弄了半天我还是觉得自己低端一些,发现我把别人写了二十行的程序不仅少用了不少逻辑减少了不少分支,还少写了不少代码啊....
但我真的不觉得自己低端,只是我的思路就是这样而已... 真的就是这样而已,我没第一个想到要用
但这真的就是我的直觉...
但我真的不觉得自己低端,只是我的思路就是这样而已... 真的就是这样而已,我没第一个想到要用
for until (我没说这是『特殊』的语法,其实只是扩展方法) 也没有想到要在 val 里用 elvis (?:) 操作决定提前返回 null(实际上这样导致某 val 的值可能为 Nothing,即便实践上后面的代码无法访问到这种情况,因为 Nothing 显然不会出现,它只能在类型的角度被讨论)但这真的就是我的直觉...
#task 嗯嗯,那么明天又要上学了啊... 看来本来打算完成基本的计划都无法完成了呢,那计划就只有继续讲一些理论向的东西和开发一个应用算了
+ #PLT Zero sized types、Empty type(bottom type) 的 Sum(+) 和 Product(*): 为什么要给他们起这种名字
+ #Qt 5 Widgets 开发一个支持插件的 "Dullboy" 应用,其目的在于利用和 KDE Applet / Systemd 的集成,定时启动强制锁死用户界面一段时间,让我这种“工作狂”(无褒义,仅仅是我对自己的戏称)不能随便糟蹋身体健康 的说。
+ 顺带讲一下关于传统序列解析器架构策略相关的内容(比如命令行参数解析器)
+ 回复在 #Bilibili 《黑子的篮球》 S1 里看到的一个 NOIP 同好,虽然我不是 #OI 方面的说... 也不是不可能,但现在不是
== 这些是明显做不完的
+ #PL C++ 弄一个 REPL 支持的计算器,有所谓的 MidTreeParser 抽象和 ReplLexer 这种支持 Hook 上输入事件的 Lexer
+ LLVM 开发 Toy 语言的编译器,当然是照 LLVM Cookbook 画瓢,不过我是不会抄里面的不良实践的(比如,明明是返回
+ Android 视图应用:Lime tokenize view
尝试开发一个使用 RecyclerView, Fragments, Services 的 Android 应用
应用向的人不准喷!不准喷!与你们无关!你们熟悉的我只是暂时没有时间去熟悉,也不要拿冰封哥的 CastleGame 数据库访问 show 我,比起 SQLite RDBMS,还是等会关系代数了或者说会图数据库了才能来说话!
+ Android 版本的 AllDreamWall & SDK
SDK 想做成 Maven 管理库的形式,不过不用为 Central 填写元数据,而且也只是自己发布的说
同样不准喷,真的不能喷啊... 这有什么的呢?
+ 默写一点关于 HTML4(5) 和 CSS 相关的东西,写点布局
+ 继续写完 smms.es6 (这个使用的 requests-promise-native)
+ #PLT Zero sized types、Empty type(bottom type) 的 Sum(+) 和 Product(*): 为什么要给他们起这种名字
+ #Qt 5 Widgets 开发一个支持插件的 "Dullboy" 应用,其目的在于利用和 KDE Applet / Systemd 的集成,定时启动强制锁死用户界面一段时间,让我这种“工作狂”(无褒义,仅仅是我对自己的戏称)不能随便糟蹋身体健康 的说。
+ 顺带讲一下关于传统序列解析器架构策略相关的内容(比如命令行参数解析器)
+ 回复在 #Bilibili 《黑子的篮球》 S1 里看到的一个 NOIP 同好,虽然我不是 #OI 方面的说... 也不是不可能,但现在不是
== 这些是明显做不完的
+ #PL C++ 弄一个 REPL 支持的计算器,有所谓的 MidTreeParser 抽象和 ReplLexer 这种支持 Hook 上输入事件的 Lexer
+ LLVM 开发 Toy 语言的编译器,当然是照 LLVM Cookbook 画瓢,不过我是不会抄里面的不良实践的(比如,明明是返回
nullptr 却写成返回 0、到处使用 global linkage 的 static 变量)+ Android 视图应用:Lime tokenize view
尝试开发一个使用 RecyclerView, Fragments, Services 的 Android 应用
应用向的人不准喷!不准喷!与你们无关!你们熟悉的我只是暂时没有时间去熟悉,也不要拿冰封哥的 CastleGame 数据库访问 show 我,比起 SQLite RDBMS,还是等会关系代数了或者说会图数据库了才能来说话!
+ Android 版本的 AllDreamWall & SDK
SDK 想做成 Maven 管理库的形式,不过不用为 Central 填写元数据,而且也只是自己发布的说
同样不准喷,真的不能喷啊... 这有什么的呢?
+ 默写一点关于 HTML4(5) 和 CSS 相关的东西,写点布局
+ 继续写完 smms.es6 (这个使用的 requests-promise-native)
Math notes | 数学笔记
https://lexuge.github.io/2019/05/30/Set-Theory-in-Rust-s-trait-system/
这个是真心推荐,作者还为我们排版了数学公式,讲的就是 Rust 的 Trait (in its type system) 和集合论之间的联系(子类型和可取操作) #PLT
作者用的是英文,不过推荐依然要阅读,我过会也会阅读的
当然,因为我最近有在设计一门叫做 Radium 的新高级程序设计语言的说(而且它支持 Trait)
所以这个理论比较有用,但是我之前也有考虑过 trait 类型和其他相关类型的干系(基本没有理论基础的情况下,而且 Ra 的类型系统也没有被规范化,仅仅是我想了一些常见的例子中的类型检查和关系而已)
上面的转发评论可能是误解... LEXUGE 应该是有看我的频道,但这个和我之前的 PLT 入门没有很大联系(之前没有讨论到 Traits,只是简单的给了一个直觉,而且还没有贴 Agda 之类的来强化直觉... 真的是我没有时间...)
作者用的是英文,不过推荐依然要阅读,我过会也会阅读的
当然,因为我最近有在设计一门叫做 Radium 的新高级程序设计语言的说(而且它支持 Trait)
所以这个理论比较有用,但是我之前也有考虑过 trait 类型和其他相关类型的干系(基本没有理论基础的情况下,而且 Ra 的类型系统也没有被规范化,仅仅是我想了一些常见的例子中的类型检查和关系而已)
上面的转发评论可能是误解... LEXUGE 应该是有看我的频道,但这个和我之前的 PLT 入门没有很大联系(之前没有讨论到 Traits,只是简单的给了一个直觉,而且还没有贴 Agda 之类的来强化直觉... 真的是我没有时间...)
Telegram
duangsuse::Echo
#PL #PLT 推荐,当然本频道之前也有讲类似的东西,非常感谢 LEXUGE 一直能关注这种弱鸡频道...(是的,在同为非应用向编程的人前我丝毫不会感觉自己容易被喷、或者对方要秀我一脸什么的,而且也不会莫名“自大” — 这类人显然在我说些可能他们还没学到的东西时候不会有任何不适感,各弄各的) 因为我在 GitHub 更新上看到他 Star 我最近改名的一个 repo,说起来,最近大家(一些可以认为是『学院派』一点的博主)都开始用纯 English 写作了,有点看不懂的样子,看来英文还是得学啊
duangsuse::Echo
搞🐔一点的东西,毕竟我也不是只 🐔(是的,🐔 是一种 🥬🐔 但是 🥬🐔 不是一种 🐔[1]),没有办法理解也自然不可能误人子弟了,我只是来做乡村怨̶妇̶基础科普... 咳咳 基本都是用 Haskell、Scala、Agda、ML 这类要命 🐸的语言写一点可能并不简单的程序时候需要了解的,不过说起来类型上面讨论的毕竟还是一个高层抽象... 只能给个链接。 + Kinds A kind is the type of a type constructor or, less commonly, the type…
constructed types
忽然发现上面有一个很弱智的错误:
不是不对(因为
非常抱歉,我说错了一个非常基础的 Haskell 知识...
这里实际上,他们的类型是(
-
-
因为 Show 是
∀a.
这就是 Haskell 里的 typeclass,类型约束这种东西其实 C# 里面都有(
当然,PHP5 里的『类型约束』就不是我们这里所讨论的类型约束了(虽然有相似之处,其实更类似 Python 3 里的...),照顾一下人家,毕竟 PHP 是动态弱类型哈?
下面是 Set Theory in Rust's trait system 这篇文章的阅读笔记 #PLT
== 问题:
有 trait 类型
(讲个笑话,这里我写的正好是有效的 Ra 代码,它定义
where:
- 我们是这么抽象 trait 类型 A, B 的:他们有效操作(method)的 Set(集合)
比如说
Haskell 里的 Show typeclass (一种版本):
-
== 第一个推论(实际上是从 T 的实际类型倒着推 A 和 B 上的属性...)
T = {
因为,
forall method_a in A
forall method_b in B
都有
method_a in T &&
method_b in T 成立
所以(啊,这是初中数学啊,还不是奥数,这样的简单逻辑快̶没̶有̶写̶出̶来̶的̶必̶要̶了̶...)
在子类型上,我们只能说 T 是 A 和 B 的子类型,A, B 不能是 T 的子类型
== 第二个推论
现在 A, B 是(各自)他们的 type instance 的集合
T⊂C
T⊂(A∩B)
这里 ⊂ 是 subsetof 的意思
∩ 是 unionset 的意思,(A∩B) 实际上就是 type A, B 所谓的 intersection type
show :: Show a => a -> String
(/) :: Fractional a => a -> a -> a
说到 traits (属性)忽然发现上面有一个很弱智的错误:
show :: Show a => a -> String
(/) :: Fractional a => a -> a -> a
(Show a) & (Fractional a) constructed types ???不是不对(因为
Show a 是 一个 Constraint,它在 Haskell 里也是类型,哦不,类型的类型,好吧还是类型... 刚才说那个不是类型的是 typeclass,它不是类型)但是这里角度错了非常抱歉,我说错了一个非常基础的 Haskell 知识...
这里实际上,他们的类型是(
a 是类型变量,String 是一个类型,它的 kind 是 ∗;(->) 是柯里化函数类型架构器;:: 表示 "has type";() 包裹的 infix operator 是 Haskell 的语法特性,被称为 "sectioning")-
show :: a -> String
- (/) :: a -> a -> a
不过!-
show 里的这个 a "是" forall a. (universal qunatifier ∀) 不过还有个额外的类型约束:a 必须是 typeclass (Haskell 类型类) Show 的实例 (Show a) :: *, 当然它是一种类型 (Constraint) 因为 Show 是
(* -> Constraint)
ghci> :kind ShowShow :: * -> Constraint
Show String :: Constraint
换句话说,show 就是 show :: forall a satisfies (Show a). a -> String
- (/) 里的这个 a 也是 forall a. 不过也有个额外的类型约束:∀a.
(Fractional a) => a -> a -> a有了 a 还不够,还得 "有"(就是
=>)(Fractional a)成立才能有
(/) :: a -> a -> a 这个操作符(operator) 存在这就是 Haskell 里的 typeclass,类型约束这种东西其实 C# 里面都有(
where T: class 什么的来让 type checker 保证某种 operation 在这个 type 上有效,比如这里 C# struct 就不能进行强制转换为 C# class 的操作)当然,PHP5 里的『类型约束』就不是我们这里所讨论的类型约束了(虽然有相似之处,其实更类似 Python 3 里的...),照顾一下人家,毕竟 PHP 是动态弱类型哈?
下面是 Set Theory in Rust's trait system 这篇文章的阅读笔记 #PLT
== 问题:
有 trait 类型
A 和 B
假设有 type T = A & B,你能从中推断出什么?(讲个笑话,这里我写的正好是有效的 Ra 代码,它定义
T 为 A 和 B 的 intersection type,跑)where:
- 我们是这么抽象 trait 类型 A, B 的:他们有效操作(method)的 Set(集合)
比如说
Haskell 里的 Show typeclass (一种版本):
class Show t where这里
show :: t -> String
Show t 类型就是集合 {(show::t->String)} — Show 是表示类型约束的 Kind((* ->)... Constraint),Kind 不是类型,它是类型架构器-
TI 是 Type Instance 的缩写(acronym) == 第一个推论(实际上是从 T 的实际类型倒着推 A 和 B 上的属性...)
T = {
method | method is method that implemented by T}因为,
forall method_a in A
forall method_b in B
都有
method_a in T &&
method_b in T 成立
所以(啊,这是初中数学啊,还不是奥数,这样的简单逻辑快̶没̶有̶写̶出̶来̶的̶必̶要̶了̶...)
T supersetof (A unionset B)当然这实际上表达了『T: A + B,A 和 B 都是 T .... 的子集 的意思』
在子类型上,我们只能说 T 是 A 和 B 的子类型,A, B 不能是 T 的子类型
== 第二个推论
现在 A, B 是(各自)他们的 type instance 的集合
T = {TI | TI ∈ type T}
定义集合C = {TI | TI implements A ∧ TI implements B} = A insect B
如果 T 是 A 和 B 实例T⊂C
T⊂(A∩B)
这里 ⊂ 是 subsetof 的意思
∩ 是 unionset 的意思,(A∩B) 实际上就是 type A, B 所谓的 intersection type
en.wikibooks.org
Haskell/Classes and types
Back in Type basics II we had a brief encounter with type classes as the mechanism used with number types. As we hinted back then, however, classes have many other uses.
duangsuse::Echo
constructed types show :: Show a => a -> String (/) :: Fractional a => a -> a -> a 说到 traits (属性) 忽然发现上面有一个很弱智的错误: show :: Show a => a -> String (/) :: Fractional a => a -> a -> a (Show a) & (Fractional a) constructed types ??? 不是不对(因为 Show a 是 一个 Constraint,它在…
==
我们总结一下,上面这一堆瞎眼但其实是初中数学混高二逻辑和证明的... 集合式子到底是在说什么:
— 对作者:非常抱歉我是这么评价上面这些式子的,但这完全是因为我不习惯数学表达方式导致的,和式子本身以及作者水平之类无关
关于
第一个:
作者的本意是告诉大家,
比如
第二个:
在类型类的实例(Trait type instance)角度看:
— Trait Type Intersection 则是没有意义的,因为 trait 只是讨论 operators,不包含 values
— 在值(values)集合意义上讨论
+ A, B 的 Union type T 是两者值的并集;T 的实例可以应用到所有 A, B 『都支持』的 Operator 上
子类型理论里;亲类型和子类型的 union 是亲类型 (ancestor); 这意味着只有亲类型的 operator 可用,而子类型自然包括所有亲类型的值
子类型理论了;伴类型(subtyping 关系中存在相同亲类型的类型)的 union T' 是他们最近的亲类型
但是这个 T' 依然可以包括他们共有的 operator
+ A, B 的 Intersection type T 是两者值的交集;T 的实例可以应用到所有 A 『或者』 B 『支持』的 Operator 上(T 和 A, B 都
子类型理论里;亲类型和子类型的 intersection 是被派生最多的类型(子类型阶更高的类型)
Eq Int 可以 (==) :: Int -> Int -> Bool
假设有
(Show|Eq) 的操作集合是 show, (==)
(Show&Eq) 的操作集合是 emptyset(空集)
这里 intersection type "我们共有的属性" 是 union type "你或者我有的属性" 的子类型吗?是!
(Haskell 用 Constraint 有点头晕了,我想 Ra 的类型系统应该会直接一点)
从集合角度看
供参考:
Ra 的类型系统与上面的集合式子之间的关系大概是:
Intersection type
(A & B) <=> A ∩ B
Union type
(A | B) <=> A ∪ B
Subtyping:
R is T <=> T⊂R
T is R <=> T⊃R
根据我自己刚才的思考以及作者的这个 issue,Rust generic type constraint 里的 + operator 获得的 trait 约束类型采取的是并集运算
Ra 里,并集对应的类型操作符是
唉,其实讨论的太抽象了,实际上 Ra 要支持 Traits,还得再多下点功夫才行啊...
我们总结一下,上面这一堆瞎眼但其实是初中数学混高二逻辑和证明的... 集合式子到底是在说什么:
— 对作者:非常抱歉我是这么评价上面这些式子的,但这完全是因为我不习惯数学表达方式导致的,和式子本身以及作者水平之类无关
关于
type T = (A :: Constraint) | (B :: Constraint) (T 就是 Rust 里的 T: A + B)的推论第一个:
T 是 A, B 的子类型,因为 T 实现了 A 和 B 的所有操作(超集或者同一集合)T is (A | B)T 是 A, B 的 Type union,至于为什么作者会把这个定义包含的属性写出来,因为原来我们是在讨论 Rust 的类型约束
T: A+B
我作了点弊,把使用的代码换成了自己设计的 Ra 语言的代码了... Ra 类型语法比较类似 PLT 上的表述,所以看起来就没有区别作者的本意是告诉大家,
T: A + B => T 是 A, B 的 Type Union (推导过程上面有说,就是讨论有效 operator 集合的问题)比如
forall t. A = Show t, B = Eq t
T 就是又实现 Eq t 又实现 Show t 的 Constraint第二个:
在类型类的实例(Trait type instance)角度看:
type C = A | B— C (trait)要求 Type instance 实现了 A 和 B trait(Trait Type Union)
pure assert C is A and C is B
— Trait Type Intersection 则是没有意义的,因为 trait 只是讨论 operators,不包含 values
— 在值(values)集合意义上讨论
+ A, B 的 Union type T 是两者值的并集;T 的实例可以应用到所有 A, B 『都支持』的 Operator 上
子类型理论里;亲类型和子类型的 union 是亲类型 (ancestor); 这意味着只有亲类型的 operator 可用,而子类型自然包括所有亲类型的值
子类型理论了;伴类型(subtyping 关系中存在相同亲类型的类型)的 union T' 是他们最近的亲类型
的子类型
这意味着只有最近亲类型的 operator 可用(至少的),而子类型自然包括所有亲类型的值但是这个 T' 依然可以包括他们共有的 operator
+ A, B 的 Intersection type T 是两者值的交集;T 的实例可以应用到所有 A 『或者』 B 『支持』的 Operator 上(T 和 A, B 都
兼容)子类型理论里;亲类型和子类型的 intersection 是被派生最多的类型(子类型阶更高的类型)
Num & Int 是 Num
伴类型之间的 intersection 与原类型不存在子类型关系type T = A | B 的话C is T
(A | B) is T这样就好理解多了,如果 A 是
(A|B) is (A|B)
Show Int、B 是 Eq Int
Show Int 可以 show :: Int -> StringEq Int 可以 (==) :: Int -> Int -> Bool
假设有
ShowEq Int 是 Show Int 或者 Eq Int (Show | Eq)BothShowEq Int 是 (Show Int) 和 (Eq Int) (Show & Eq)(Show|Eq) 的操作集合是 show, (==)
(Show&Eq) 的操作集合是 emptyset(空集)
这里 intersection type "我们共有的属性" 是 union type "你或者我有的属性" 的子类型吗?是!
(Haskell 用 Constraint 有点头晕了,我想 Ra 的类型系统应该会直接一点)
从集合角度看
T = A union B
T subsetof (A insect B)
==供参考:
Ra 的类型系统与上面的集合式子之间的关系大概是:
Intersection type
(A & B) <=> A ∩ B
Union type
(A | B) <=> A ∪ B
Subtyping:
R is T <=> T⊂R
T is R <=> T⊃R
根据我自己刚才的思考以及作者的这个 issue,Rust generic type constraint 里的 + operator 获得的 trait 约束类型采取的是并集运算
Ra 里,并集对应的类型操作符是
| (交集的则为 &)唉,其实讨论的太抽象了,实际上 Ra 要支持 Traits,还得再多下点功夫才行啊...
GitHub
「第三章」`3.4.2 泛型约束` 数学角度描述 trait 中的概念混淆与逻辑错误 · Issue #99 · ZhangHanDong/tao-of-rust-codes
页码与行数 第 70 页 理解 trait 限定 文本或排版错误 文中说 trait 也是一种类型,是一种方法集合,或者说是一种行为的集合 然后举了 Paginate、Page、Perpage 三者之间的关系,并推导出 这样的联系。 整个段落混淆了 泛型标记 和 实类型,同时也引发了逻辑错误 对于 trait Paginate: Page + Perpage 根据大前提 trait 是 方法...
duangsuse::Echo
== 我们总结一下,上面这一堆瞎眼但其实是初中数学混高二逻辑和证明的... 集合式子到底是在说什么: — 对作者:非常抱歉我是这么评价上面这些式子的,但这完全是因为我不习惯数学表达方式导致的,和式子本身以及作者水平之类无关 关于 type T = (A :: Constraint) | (B :: Constraint) (T 就是 Rust 里的 T: A + B)的推论 第一个: T 是 A, B 的子类型,因为 T 实现了 A 和 B 的所有操作(超集或者同一集合) T is (A | B) T…
果然还是 PLT 说多了... 然后一事无成么...
既然这样待会继续 PLT 吧,不过那个时间管理软件依然必须开发,明天也一样
绝对不能再熬夜了!!!
既然这样待会继续 PLT 吧,不过那个时间管理软件依然必须开发,明天也一样
绝对不能再熬夜了!!!
duangsuse::Echo
果然还是 PLT 说多了... 然后一事无成么... 既然这样待会继续 PLT 吧,不过那个时间管理软件依然必须开发,明天也一样 绝对不能再熬夜了!!!
This media is not supported in your browser
VIEW IN TELEGRAM