中文博客

欢迎来到千里冰封的中文博客。所有中文内容将于 2019 年 4 月后不再维护,感谢大家三年来的关注。


如果翻译器对程序进行了彻底的分析而非某种机械的变换,而且生成的中间程序与源程序之间已经没有很强的相似性,我们就认为这个语言是编译的。 彻底的分析和非平凡的变换,是编译方式的标志性特征。
如果你对知识进行了彻底的分析而非某种机械的套弄,在你脑中生成的概念与生硬的文字之间已经没有很强的相似性,我们就认为这个概念是被理解的。 彻底的分析和非凡的变换,是获得真知的标志性特征。

Agda 博客

点此进入 Literate Agda 博客

中文页面

中文文章

  1. 2019/03/13 - PLT 实现一个简单的 MLTT Type Checker
  2. 2019/01/28 - PLT 重新思考依赖类型编程语言的设计
  3. 2019/01/01 - Haskell Visitor Pattern 与 Finally Tagless:解决表达式问题
  4. 2018/12/08 - Misc 最近的计划
  5. 2018/11/23 - Haskell 如何处理可选的二维编程语言文法
  6. 2018/11/18 - PLT 关于依赖类型编程语言和完全函数的检查的一些想法
  7. 2018/11/16 - PLT dependent type 之上还有更高级的类型系统吗?
  8. 2018/11/09 - Water 终于换上 https 啦,新增 LAgda 子博客
  9. 2018/10/06 - Misc 又做了一个好玩的梦
  10. 2018/09/24 - Editor 代码编辑器系列 #3 文本的存储 进化篇
  11. 2018/09/07 - Water 为什么这么多人喜欢写编译器
  12. 2018/08/04 - Agda Agda 实现类型安全的 printf
  13. 2018/07/27 - Lua LuaIntf 初探
  14. 2018/07/07 - CXX C++ 模拟 Java 风格的 Vector
  15. 2018/06/16 - Arkirina 让博客的代码容器不换行
  16. 2018/06/13 - Agda 迟来的 Agda 环境搭建
  17. 2018/06/05 - Editor 代码编辑器系列 #2 文本的存储 远古篇
  18. 2018/06/04 - CXX 如何取消一个 C/C++ 的符号的定义
  19. 2018/05/30 - Agda Agda 中的 coinductive data type
  20. 2018/05/17 - Editor 知乎回答:编程软件界面的文本编辑器是如何制作的
  21. 2018/05/11 - Java 一个你可能没听说过的 Java 语法
  22. 2018/05/10 - CMake 使用 CMake 不用路径地调用 libclang
  23. 2018/05/06 - Arkirina 知乎那神一般的糖
  24. 2018/04/29 - Editor 代码编辑器系列 #1 架构与解耦
  25. 2018/04/27 - Editor 代码编辑器系列 #0 两种编辑器
  26. 2018/03/15 - Misc 整理几个最近写的比较正常的回答
  27. 2018/03/12 - Java 吐槽 IntelliJ 和 Eclipse 的实现细节
  28. 2018/03/09 - Java 简要介绍 IntelliJ 和 Eclipse 的插件系统
  29. 2018/03/07 - Misc 给博客换了新主题
  30. 2018/02/18 - Misc 一些有趣的语法设计的细节
  31. 2018/02/17 - Kotlin 聊两个 Kotlin 编译器的 bug
  32. 2018/02/16 - Water 又过去了半年了
  33. 2018/01/22 - IntelliJ 一些看了让人很爽的动态图
  34. 2018/01/20 - Kotlin 没有 lambda abstraction 的无聊 Kotlin
  35. 2018/01/07 - Misc 人类需要主动思考
  36. 2018/01/07 - Arkirina 安卓知乎客户端当然也会收集用户信息
  37. 2018/01/04 - Java Java 里的类型推导,上篇文章中的一个问题
  38. 2018/01/03 - Kotlin Kotlin 那些不仅仅是语法糖的好处
  39. 2018/01/02 - Haskell 计算机科学 (Haskell) 中的偏序理论(译,上)
  40. 2017/12/31 - Arkirina 在 Chrome 里面重定向网页资源
  41. 2017/12/25 - IntelliJ IntelliJ IDEA 复杂的重构操作
  42. 2017/12/21 - IntelliJ IntelliJ IDEA 复杂的重构技巧
  43. 2017/12/20 - Tools 基于图像的 LSB 隐写术科普
  44. 2017/12/15 - Git 为什么我用 merge 而不用 rebase
  45. 2017/12/07 - Java JavaFX 在 Ubuntu 上的一个 bug ,万恶的向前不兼容
  46. 2017/11/13 - Misc 给博客添加了部分文章可评论的功能
  47. 2017/11/12 - Kotlin 正确地使用 Kotlin 的 internal
  48. 2017/11/10 - CI 将 Flutter 项目部署到 Travis CI
  49. 2017/11/09 - Agda Agda 中的证明,从三到四
  50. 2017/11/08 - Agda Agda 中的证明,从二到三
  51. 2017/11/06 - Agda Agda 中的证明,从一点五到二
  52. 2017/11/02 - Agda Agda 中的证明,从一到一点五
  53. 2017/11/01 - Agda Agda 中的证明,从零到一
  54. 2017/10/12 - Kotlin Kotlin 1.2 跨平台模块初体验
  55. 2017/10/08 - Gradle Gradle 常见的几个自定义 Task
  56. 2017/10/03 - Emacs 搭建 Emacs 的 Haskell/Idris 环境教程
  57. 2017/09/20 - Water 给博客加上了访问量统计
  58. 2017/08/30 - Water 两年,能带来什么?
  59. 2017/08/26 - Lisp 写给 Java 程序员的 Lice 教程 3
  60. 2017/08/24 - Misc 如何写好技术文章
  61. 2017/08/18 - Misc 记录一个很有意思的梦
  62. 2017/07/27 - Haskell 使用 Haskell 编写灵活的 Parser (下)
  63. 2017/07/26 - Haskell 使用 Haskell 编写灵活的 Parser (上)
  64. 2017/07/21 - Koa Akiris 的 Koa 杂谈 1
  65. 2017/07/10 - Haskell 将 Haskell 翻译为 Rust, C# (上')标准库
  66. 2017/07/06 - Tools 简单粗暴的地图生成
  67. 2017/07/05 - Haskell 将 Haskell 翻译为 Rust Dart Java (上)标准库
  68. 2017/07/01 - OI 防止运算溢出的一些技巧
  69. 2017/06/15 - Java Java 竟然还能这样玩
  70. 2017/06/01 - CI 持续集成教程 1 通识科普
  71. 2017/05/26 - Haskell 函数式 dfs (深度优先搜索)
  72. 2017/05/16 - Flutter 初次见面, Flutter !(一个月试用报告)
  73. 2017/05/15 - Kotlin 暂时不会再写关于 Kotlin 的东西了
  74. 2017/05/13 - Misc 成都 Kotlin 线下聚会报告及科技汇总
  75. 2017/05/11 - Kotlin Kotlin 一个很厉害的 DSL 写法
  76. 2017/05/04 - Kotlin Kotlin 命令行环境搭建
  77. 2017/05/02 - Gradle Gradle 定制 artifact
  78. 2017/05/01 - Kotlin Kotlin : Lambda 也能递归
  79. 2017/04/26 - Kotlin Kotlin :强行 Point-Free
  80. 2017/04/24 - JNI 关于字典树( Trie 树)的一些想法(含 JNI 内容)
  81. 2017/04/23 - Kotlin Kotlin : forEach 也能 break 和 continue
  82. 2017/04/22 - Arkirina 解决一个神奇的webpack问题 - Cannot find module 'webpack/schemas/WebpackOptions.json'
  83. 2017/04/20 - Tools 把图片变成字符画
  84. 2017/04/20 - MPS 突然 MPS 教程(五),扩展 Java
  85. 2017/04/18 - Ruby Ruby 的 Tk 库的一个 bug
  86. 2017/04/14 - Gradle Gradle 其实是很好用的
  87. 2017/04/12 - MPS MPS 教程四:制作一个简易语言(下)
  88. 2017/04/07 - MPS MPS 教程三:制作一个简易语言(中)
  89. 2017/04/06 - Water 做了四张图片,太好玩了
  90. 2017/04/06 - MPS MPS 教程二:制作一个简易语言(上)
  91. 2017/04/02 - Tools 发布一个 GitHub 仓库时需要注意的东西
  92. 2017/04/02 - OI 多线程快排测试 CPU 性能
  93. 2017/04/01 - IntelliJ IntelliJ IDEA 进阶教程: 语言注入
  94. 2017/03/28 - Kotlin LiceIntelliJ 插件图标制作过程
  95. 2017/03/24 - JNI 使用内存池消除可能出现的野指针 delete 操作
  96. 2017/03/18 - MPS MPS 教程一:环境搭建+试运行一个语言
  97. 2017/03/11 - Lisp 写给 Java 程序员的 Lice 教程 2
  98. 2017/03/10 - Lisp 龙书撞枪系列 1 : Lice 的动态作用域实现
  99. 2017/03/09 - Kotlin Kotlin Primer 草稿 函数
  100. 2017/03/08 - Lisp 昨天说的编辑 AST 并导出代码做出来了
  101. 2017/03/07 - Lisp 给 Lice 写了俩工具
  102. 2017/03/01 - Lisp 写给 Java 程序员的 Lice 教程
  103. 2017/02/25 - Lisp 简单拿 Lice Clojure 在相同的方面对比一下
  104. 2017/02/24 - Lisp 人生第一个解释器, Lisp
  105. 2017/02/19 - JNI JNI 开发:结语+带逛一波
  106. 2017/02/18 - JNI JNI 开发:第五章 更多语言的尝试
  107. 2017/02/17 - Scala (翻译)从编程语言的角度看深度学习
  108. 2017/02/03 - JNI JNI 开发:第四章 个人经验分享
  109. 2017/02/02 - Kotlin 写代码不用变量 Kotlin
  110. 2017/01/29 - JNI JNI 开发:第三章 基本类型数组操作
  111. 2017/01/27 - JNI 用 CMake 开发 JNI :第二章 第二个环境搭建
  112. 2017/01/25 - Kotlin Kotlin 的一些好东西概览(不含 extension
  113. 2017/01/24 - Kotlin Kotlin 与 Java 交互技巧
  114. 2017/01/23 - JNI 用 Dev Cpp 开发 JNI :第一章 环境搭建
  115. 2017/01/21 - Misc 谈谈我对 GFW 的看法
  116. 2017/01/16 - Android Android 神器 Pocket Git 的使用
  117. 2017/01/07 - Java JetBrains 注解库, Contract 注解
  118. 2017/01/06 - Java 使用 JetBrains 注解库注释你的代码
  119. 2016/12/24 - Tools 连字及其在 IDE 中的使用
  120. 2016/12/20 - Water 喜大普奔 GitHub 一年连载达成
  121. 2016/12/11 - IntelliJ IntelliJ IDEA 进阶教程: 测试框架
  122. 2016/11/19 - IntelliJ IntelliJ IDEA 进阶教程: IDEA 中工程的基本概念
  123. 2016/10/28 - OI 如何正确使用 DEV C++
  124. 2016/10/28 - OI 树状数组离散化
  125. 2016/10/18 - IntelliJ IntelliJ IDEA 进阶教程: IDE 背景图片
  126. 2016/10/17 - Kotlin 如何让孩子爱上 Kotlin : DSL (下)
  127. 2016/10/01 - Kotlin 如何让孩子爱上 Kotlin : DSL (中)
  128. 2016/09/28 - Kotlin 如何让孩子爱上 Kotlin : DSL (上)
  129. 2016/09/09 - Java 在 JavaFX 中进行 Material Design :第三章
  130. 2016/09/09 - Java 在 JavaFX 中进行 Material Design :第二章
  131. 2016/08/28 - IntelliJ IntelliJ IDEA 进阶教程: 自定义代码模板
  132. 2016/08/23 - Game 轮子狂魔造引擎 第五章
  133. 2016/08/17 - Game 轮子狂魔造引擎 第四章
  134. 2016/08/16 - Game 轮子狂魔造引擎 第三章
  135. 2016/08/15 - Game 轮子狂魔造引擎 第二章
  136. 2016/08/14 - Game 轮子狂魔造引擎 第一章
  137. 2016/07/25 - Water 笑死我了
  138. 2016/07/12 - Kotlin 如何让孩子爱上 Kotlin 第四章:基本类型
  139. 2016/07/11 - Android 谷歌黑科技:为什么这么小啊
  140. 2016/07/09 - IntelliJ 传教之 IntelliJ IDEA 第四章:集成版本控制系统
  141. 2016/07/02 - Python 好东西推荐: PyCharm Edu
  142. 2016/07/02 - Kotlin 如何让孩子爱上 Kotlin 第三章:变量
  143. 2016/07/01 - Kotlin Kotlin 编译器内部报错,我受伤很深
  144. 2016/06/30 - Kotlin 如何让孩子爱上 Kotlin 第二章: Hello World
  145. 2016/06/29 - IntelliJ 传教之 IntelliJ IDEA 第三章:代码补全中的小技巧
  146. 2016/06/26 - Kotlin 如何让孩子爱上 Kotlin 第一章:环境搭建
  147. 2016/06/26 - IntelliJ 传教之 IntelliJ IDEA 第二章:快捷键(一)
  148. 2016/06/26 - IntelliJ 传教之 IntelliJ IDEA 第一章: IntelliJ IDEA 的下载与安装
  149. 2016/06/25 - Java 在 JavaFX 中进行 Material Design :第一章