分享一篇文章和一本开源书

540 views
Skip to first unread message

Xinyu LIU

unread,
Jun 26, 2013, 1:31:23 AM6/26/13
to pon...@googlegroups.com
文章很好，书我还没有细看。
书是讲type theory的：
http://audrey.fmf.uni-lj.si/hott.html

Zhao Boran

unread,
Jun 26, 2013, 1:48:33 AM6/26/13
to pon...@googlegroups.com
谢谢！

2013/6/26 Xinyu LIU <liuxi...@gmail.com>:
> --
>
> ---
> 您收到此邮件是因为您订阅了 Google 网上论坛的“TopLanguage”论坛。
> 要退订此论坛并停止接收此论坛的电子邮件，请发送电子邮件到 pongba+un...@googlegroups.com。
> 要查看更多选项，请访问 https://groups.google.com/groups/opt_out。
>
>

Xinyu LIU

unread,
Jun 26, 2013, 2:12:41 AM6/26/13
to pon...@googlegroups.com
还是人多力量大！将近30人，只用了半年就写出了这么一本数学书。
累计15人年。我的AlgoXY用了5人年，还差得远啊。

另外，确切说是Homotopy type theory
http://homotopytypetheory.org/book/

以前我对这个也是没有什么直观认识，只是觉得Haskell以及ML家族(Standard ML, OCaml等）的类型inference很酷。
后来读了MIT的Types and programming langauge才认识到这个水非常的深。现在终于看到一本严肃的数学书了。

任何对类型系统的理论和实现感兴趣的朋友都推荐读一读。



2013/6/26 Zhao Boran <zha...@gmail.com>

Taurus

unread,
Jun 26, 2013, 5:47:12 AM6/26/13
to pon...@googlegroups.com
��������İ档

On 2013/6/26 14:12, Xinyu LIU wrote:
�����˶������󣡽���30�ˣ�ֻ���˰����д������ôһ����ѧ�顣
�ۼ�15���ꡣ�ҵ�AlgoXY����5���꣬�����Զ����

���⣬ȷ��˵��Homotopy type theory
http://homotopytypetheory.org/book/

��ǰ�Ҷ����Ҳ��û��ʲôֱ����ʶ��ֻ�Ǿ���Haskell�Լ�ML����(Standard ML, OCaml�ȣ�������inference�ܿᡣ
��������MIT��Types and programming langauge����ʶ�����ˮ�dz�����������ڿ���һ���������ѧ���ˡ�

�κζ�����ϵͳ�����ۺ�ʵ�ָ���Ȥ�����Ѷ��Ƽ���һ����
2013/6/26 Zhao Boran <zha...@gmail.com>
лл��

2013/6/26 Xinyu LIU <liuxi...@gmail.com>:
> ���ºܺã����һ�û��ϸ����
> ���ǽ�type theory�ģ�
> --
>
> ---
> ���յ����ʼ�����Ϊ������ Google ������̳�ġ�TopLanguage����̳��
> Ҫ�˶�����̳��ֹͣ���մ���̳�ĵ����ʼ����뷢�͵����ʼ��� pongba+un...@googlegroups.com��
> Ҫ�鿴���ѡ������ https://groups.google.com/groups/opt_out��
>
>

--

---
���յ����ʼ�����Ϊ������ Google ������̳�ġ�TopLanguage����̳��
Ҫ�˶�����̳��ֹͣ���մ���̳�ĵ����ʼ����뷢�͵����ʼ��� pongba+un...@googlegroups.com��
Ҫ�鿴���ѡ������ https://groups.google.com/groups/opt_out��



--
 
---
���յ����ʼ�����Ϊ������ Google ������̳�ġ�TopLanguage����̳��
Ҫ�˶�����̳��ֹͣ���մ���̳�ĵ����ʼ����뷢�͵����ʼ��� pongba+un...@googlegroups.com��
Ҫ�鿴���ѡ������ https://groups.google.com /groups/opt_out��
 
 

Quinn Lu (Qian Lv)

unread,
Jun 26, 2013, 12:27:20 PM6/26/13
to pon...@googlegroups.com
请问type theory是讲什么的呢？


2013/6/26 Taurus <huangge...@gmail.com>
建议出中文版。


On 2013/6/26 14:12, Xinyu LIU wrote:
还是人多力量大！将近30人，只用了半年就写出了这么一本数学书。
累计15人年。我的AlgoXY用了5人年，还差得远啊。

另外，确切说是Homotopy type theory
http://homotopytypetheory.org/book/

以前我对这个也是没有什么直观认识，只是觉得Haskell以及ML家族(Standard ML, OCaml等）的类型inference很酷。
后来读了MIT的Types and programming langauge才认识到这个水非常的深。现在终于看到一本严肃的数学书了。

任何对类型系统的理论和实现感兴趣的朋友都推荐读一读。
2013/6/26 Zhao Boran <zha...@gmail.com>
谢谢！

2013/6/26 Xinyu LIU <liuxi...@gmail.com>:
> 文章很好，书我还没有细看。
> 书是讲type theory的：
> --
>
> ---

> 您收到此邮件是因为您订阅了 Google 网上论坛的“TopLanguage”论坛。
> 要退订此论坛并停止接收此论坛的电子邮件，请发送电子邮件到 pongba+un...@googlegroups.com。
> 要查看更多选项，请访问 https://groups.google.com/groups/opt_out。
>
>

--

---
您收到此邮件是因为您订阅了 Google 网上论坛的“TopLanguage”论坛。
要退订此论坛并停止接收此论坛的电子邮件，请发送电子邮件到 pongba+un...@googlegroups.com。
要查看更多选项，请访问 https://groups.google.com/groups/opt_out。


--
 
---
您收到此邮件是因为您订阅了 Google 网上论坛的“TopLanguage”论坛。
要退订此论坛并停止接收此论坛的电子邮件，请发送电子邮件到 pongba+un...@googlegroups.com。
要查看更多选项，请访问 https://groups.google.com /groups/opt_out。
 
 

Hao Wang

unread,
Jun 26, 2013, 12:42:45 PM6/26/13
to pon...@googlegroups.com



2013/6/26 Xinyu LIU <liuxi...@gmail.com>

文章很好，书我还没有细看。
书是讲type theory的：
http://audrey.fmf.uni-lj.si/hott.html

+1, 之前在HN上看到新闻，下到Kindle里去了，不过看肯定得花很多精力。

Xinyu LIU

unread,
Jun 27, 2013, 4:49:13 AM6/27/13
to pon...@googlegroups.com
Type theory有很多应用，包括自动证明系统等等。其中一个有趣的应用，就是用来设计计算机语言。

简单来说，type theory为类型系统的设计和实现提供了理论基础。

传统观念认为，类型系统是一个工程问题。例如我们看到的传统C++以及Java 1.5版本前的类型系统。
实际上，类型系统可以被formalize。并且存在一些强大的数学工具用于指导人们设计和实现计算机语言。

考虑下面的例子
a + b，如果a的类型是T，b的类型是T，则其结果的类型也是T
稍微复杂一点 if pred then a else b 我们可以推导，pred的类型是bool, 而a与b的类型必然一致。
再复杂一点f(x, y), 如果其类型是 a -> b -> c， 则lambda x . f(x, y)的类型是b -> c

这些都很直观，但是存在着非常难的类型inference的情形。
当涉及组合类型，递归类型，sub type，等等，问题就会变得非常难以推导。在某些情况下，推导过程等价于图灵机问题，从而是undetermine的。

人们来过去的几十年里，不断研究更加高效、更加强大的类型系统。这些在以ML为代表的函数式语言中得到了很多应用。

注：type inference和type induction有很大的不同，C++的模板推导，一般称之为type induction。
type inference则是在type theory的理论下，进行的类型计算和检查。
2013/6/27 Quinn Lu (Qian Lv) <lvqia...@gmail.com>

Jie Xu

unread,
Jun 27, 2013, 3:50:22 PM6/27/13
to pon...@googlegroups.com

背后就是各种逻辑的 expressiveness 和 tractableness 这类问题


2013/6/27 Xinyu LIU <liuxi...@gmail.com>

chenbo li

unread,
Jun 26, 2013, 2:50:05 PM6/26/13
to pon...@googlegroups.com
大爱Type Theory！感谢楼主


2013/6/27 Hao Wang <iswa...@gmail.com>

--

lu haorui

unread,
Jun 26, 2013, 9:39:47 PM6/26/13
to pon...@googlegroups.com
不错不错


2013/6/27 Hao Wang <iswa...@gmail.com>

--

chenbo li

unread,
Jun 29, 2013, 1:54:25 AM6/29/13
to pon...@googlegroups.com
Type Theory一般是研究生在上的课吗？我在本科阶段学了数理逻辑和自动机，但是感觉并没有接触到Type Theory。请问大家本科的什么课程一般会包含这方面的知识？



2013/6/27 lu haorui <luha...@gmail.com>

Shuai Wang

unread,
Jun 29, 2013, 1:56:34 AM6/29/13
to pon...@googlegroups.com
没有学过编译原理么？

chenbo li

unread,
Jun 29, 2013, 9:05:13 AM6/29/13
to pon...@googlegroups.com
下学期学…… 好吧，我竟然忘了这门课……


2013/6/29 Shuai Wang <wangsh...@gmail.com>

chenbo li

unread,
Jun 29, 2013, 9:06:11 AM6/29/13
to pon...@googlegroups.com
不过貌似我听说过其他学校有一门课就叫做“类型论”，但是我们学校没有类似的课名……


2013/6/29 chenbo li <lichen...@gmail.com>

chenbo li

unread,
Jun 30, 2013, 10:57:12 AM6/30/13
to pon...@googlegroups.com
汗，学长说我们编译原理不会讲类型论方面的东西


2013/6/29 chenbo li <lichen...@gmail.com>

milo

unread,
Jul 1, 2013, 9:10:54 PM7/1/13
to pon...@googlegroups.com
谢谢分享

Zhang Xiang

unread,
Jul 1, 2013, 9:21:41 PM7/1/13
to TopLanguage

原来F#的type infere是靠这个理论支持的

webman li

unread,
Jul 4, 2013, 9:49:54 PM7/4/13
to pon...@googlegroups.com
大概看了一下这个理论， Homotopy type theory：可翻译为：同伦类型论。 这个理论的本质，是类型论与拓扑同伦有相同的结构。
在拓扑同伦里，以空间的道路同伦为基础，可构造出基本群， 然后有2-dimensional path，3-dimensional path，......这些不同层次的homotopy between homotopies between homotopies..就产生一个范畴 ∞-groupoid 。
这个∞-groupoid 就成为类型伦对比拓扑同伦的基础。因为，类型论也产生一样的∞-groupoid 。 在类型论里，对类型A，可以有表示相等的类型 x =A y，而一个元素p: x =A y，这个p,就可以表达为x到y的path（数学书上翻译为道路），类似拓扑同伦里的path。有了path，就可以构造出和拓扑空间里类似的∞-groupoid范畴。 下面一小段直接copy过来的：
"  Thus, we will frequently refer to an element p : x =A y as a path from x to y; ...  an element r : p =(x=Ay) q can be thought of as a homotopy,or a morphism between morphisms; we will often refer to it as a 2-path or a 2-dimensional path....The structure
of this tower of identity types corresponds precisely to that of the continuous paths and (higher)
homotopies between them in a space, or an ∞-groupoid. "

Homotopy type theory里并没有连续，开集等概念。基本概念，就是类型论和拓扑都有∞-groupoid范畴。 这应该是这个理论的出发点。      我也只花了数小时，看了个大概。 里面的无穷无尽细节，太费时间了。 也就了解到此为止。在此大概记录下，以对有兴趣的看此书的朋友有点点启发

在 2013年6月26日星期三UTC+8下午2时12分41秒，Larry, LIU Xinyu写道：
Reply all
Reply to author
Forward
0 new messages