来分享点心得吧~ \囧/ 最近几个月接触的东西 顺便看看能不能稍稍激起一点这个版的活力.. 有错烦请各位多指教~ o(_ _)o ==前言分隔线== Type System Type System是一个Programming Language中很重要的一个部分 它可以帮助我们把程式中的values和expressions给分类好 Type System可以检查出我们程式的一些错误 也可以帮助我们最佳化我们的程式 举例来说 > int i = 10; 这样就是宣告变数i具有int的type 後面都用 i:int 这样来表示variable及其所拥有的type 假设我们今天有个function:foo foo吃一个int,吐出另一个int > int foo(int i){ > return i + i; > } > > String v = foo(10); //error 如此一般,compiler会吐出一个error 告诉你 v 和 foo(10) 这两个的type是不同的 v:String foo(10):int 这就是type system的功能之一 它会帮我们做一些检查 ====== 接着是让人欢乐无限的Dependent Type \囧> 在真正讲到dependent type之前 回忆一下我们一开始的糖炒栗子 > int i = 10; 我们知道 i:int 也就是说,我们知道我们的资料(也就是i) 有一个叫做int的特性(属性) 一个复杂一点的宣告可以告诉我们更多关於我们的资料的特性 > class List<E e>{ ... } > List<String> myList = new List<String>; class List<E e> 表示我们定义一个叫做List的class 这个class本身会需要一个"型别参数" 也就是说,我们可以在实体化List物件时写 List<Integer>或List<String>之类的 分别表示"装Integer的List"和"装String的List" 上面那样的作法称为generic programming(泛型) 不过,在这里我们先不讨论泛型的用法与意义 (这里比我了解泛型的人应该是多到数不完,我还是不要丢脸好了XD) 不过必须一提的是,我们确实可以用这样的方法来实做出dependent type 这点,希望在各位看官看完这篇文章以後,可以自行想像出来 题外话一下 据说,这个版的版主之前有尝试过以这样的方式来实做 也许可以请版主大人稍微讲一下实做的心得 = =+ 回到主题,上面程式片段第二行的意思就很明显了 一言以蔽之,就是 myList:List<String> 讲的白话一点,我们知道我们的myList这个变数具有两个特性 1)他是一个list 2)他不但是list,而且这个list里面装的所有资料的型态都是String 和上面那个阳春的 i:int (只单纯的显示了资料的种类) 来做比较 我们现在的 myList:List<String> 不但显示了资料结构,也显示了资料内容物的型别 回到我们一开始的名词: dependent type 这个东西指就是"把资料的特性给建立进形别之中" dependent type - 相依(於资料)的形别 这东西能做什麽呢?? 很简单,他能扩充我们的type身上能装载的特性 我们可以把各个资料结构的特性给放进type里面 这对於checking和最佳化等等都有不错的帮助 例如说,我们可以把一个list的长度给放进type里面 [1,2,3]和[1,2,3,4]这两个list的type就会是不一样的: [1,2,3] : List Integer 3 [1,2,3,4] : List Integer 4 而,如果我们把两个list接起来 新的list一定是某个type是List Integer 7的list 如果我们拿到的list的type不是这样 那就一定是有问题的,也许是有资料遗失或是重复了 而不是在我们真的要用这个list的时候才发现不对劲 小结论 \囧/ dependent type是用来强化我们工具的东西 它会让我们programming变的复杂且充满限制 而他确实的好处,其实只是让我们程式提高"正确性" 以上,是我对dependent type粗浅的了解 相信一定很多高手想要帮我补充 请大家鞭小力点啦 >/////< ====== 实际上 我在摸索上面那些东西的时候 使用的工具不是java或是C++ 而是一些functional language 所以针对这个也做点"我所知道的介绍" 顺便附上一点个人的感想 Haskell(GHC-6.6.1) 最一开始使用的语言 不过因为他对於dependent type的支援不是很好 ( 虽说好像有GADT,但是我不太知道那是什麽 也许哪个高手可以帮我补充一下,囧> ) 没试几次以後就转向其他语言了 Omega http://web.cecs.pdx.edu/~sheard/Omega/index.html 没有试过,只有看过程式码 感觉语法和Haskell很像 Epigram http://www.e-pig.org/ 据说有比较完整的dependent type 也是我试最久却最让人动怒的东西.. 他是个editor-typechecker-interpreter的综合体 编辑上,实在是不太好用 undo的时候容易当掉 存档读档也都很麻烦 与其说是个editor,还不如说是一个"填空软体" 语言本身,实在是.. 难以形容的诡异.. 有兴趣的人可以去下载example来看.. 他另外有一个compiler 但是难用程度不下於那个editor 网站上的说明和下载下来的不一样 http://www.dcs.st-and.ac.uk/~eb/esc.php Agda2 http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php 现在才要开始尝试的东西 希望会比Epigram好用很多 Orz (谜之声:话说我一开始是想写agda,怎麽反而这个讲最少?? XD) ======以下是顺便问问题区 有哪位高手可以提供一点锻链自己逻辑能力的方法.. 最近觉得自己逻辑没有学好 很多证明的东西常常没法很快转过来 但是,对於要怎麽学好,我实在是没有个概念 @"@ 以上,谢谢 o(_ _)o --

※ 发信站: 批踢踢实业坊(ptt.cc) ◆ From: 220.132.126.239