• 2019年3月5日 03:55

    行为类型系统的简介:
    资料来源:
    rholang.org/wiki/index.php?title=Research
    Behavioral Type System
    Traditionally there has been a distinction between statically-typed languages like C, Java, and Haskell and dynamically typed languages like Javascript and Python. The benefits of static typing are clear in the helpful type-checking messages that arise when programming a language like Haskell. However, even these static type systems can reason only about the structure of the data that is passed into or out of a function. By way of example, functions like shuffle, sort, and identity all satisfy the type signature Ord a => [a] -> [a]. A behavioral type system allows the same kind of type-checking on the behavior of a function. So the previous functions could be distinguished by their behavior. This allows the type checker to assist the programmer with compile-time errors to the effect of, “You can’t call the shuffle function because you expected a function that sorts the list, and shuffle doesn’t do that.”
    译文:
    传统上静态类型语言如C、Java、Haskell和动态类型语言如Javascript、Python之间有严格区别。用静态类型语言比如Haskell的好处是:编译期间会出现类型检查的消息,这非常有用。然而这些静态类型只能检查某个函数输入、输出的数据的结构。举一个例子,shuffle(把一个数组打乱),sort(排序),identity(编号)这三个函数都满足同样的签名(参数列表和类型完全一致):Ord a=>[a]->[a]。 行为类型系统允许同样的类型检查应用到函数的行为上,使得在上述例子里,这三个函数可以按照行为进行区分。这使得类型检查器可以帮助程序员在编译期就发现一些错误比如:你不能调用这个shuffle(乱序)的函数,因为这里你要调用一个行为是对数组排序的函数,shuffle显然通不过类型检查。

    Rholang社区已经做了一些工作在这个代码库里: github.com/rchain-community/behavr (作者Dan Conolly,discord id dckc)

    代码库的issue list里举了几个应用场景:
    防止DAO重入bug的类型检查: github.com/rchain-community/behavr/issues/7
    名字空间的liveness(不会锁死)和confinenment(防火墙机制):github.com/rchain-community/behavr/issues/8
    名字空间逻辑的结构化数据(比如XML语言):github.com/rchain-community/behavr/issues/9

    Dan最近举办的office hour解释了这部分工作,youtube视频链接:
    www.youtube.com/watch?v=otKa9BufRSI

    行为类型系统在RChain中的路线图中占据重要位置。在智能合约并发执行的环境下,用行为类型系统规范合约之间的交互方式,让程序员编写代码时“构造即正确”(correct by construction),无疑是非常重要的。在RChain的金星路线中,行为类型系统占据首位:
    rchain.atlassian.net/wiki/spaces/DOC/pages/464191564/Venus+plans