Typed Shell：给Unix Shell加上类型系统（2）

by

at 2013-05-26 15:00:00

original http://www.soimort.org/posts/159

（上篇：Typed Shell：给Unix Shell加上类型系统（1））

To go wrong in one's own way is better than to go right in someone else's.
- Dostoyevsky

系统环境

GNU/Linux
GCC
GHC 7.6.2
Idris 0.9.7。可从Hackage或GitHub安装：
- $ cabal install idris
- https://github.com/edwinb/Idris-dev

C FFI

因为Idris的标准库中没有提供POSIX相关系统API的支持，所以第一步工作是为Unix系统调用创建相应的Idris wrapper。我们把头文件和辅助函数的定义放在一个C文件shell.h里。

C代码：（shell.h）

#include <stdio.h>
#include <stdlib.h>
#include <errno.h>
#include <string.h>
#include <sys/types.h>
#include <sys/stat.h>
#include <dirent.h>
#include <unistd.h>

在Idris中使用%include指定包含C的头文件。为系统调用opendir()创建一个foreign function call：

Idris代码：（Shell.idr）

module Shell

%include "shell.h"

opendir : String -> IO Ptr
opendir args = mkForeign (FFun "opendir" [FString] FPtr) args

TIPS：注意到Idris和Haskell语法上的一些重要差别：

module后不需要跟where从句。
因为依赖类型的本质使得类型推断（type inference）变得更困难，在Idris中无法省略函数签名。
类型签名使用:而不是::，强调类型的重要性。（相应地，cons运算采用了和ML/Scala相同的::而不是Haskell中的:）

创建用于读取下一个文件entry的C函数readdir_next，自动忽略"."和".."；若失败则指针返回NULL：

C：

struct dirent *readdir_next(DIR *dir)
{
    struct dirent entry;
    struct dirent *entryPtr = NULL;

    readdir_r(dir, &entry, &entryPtr);
    while (entryPtr != NULL && 
        (strncmp(entry.d_name, ".", PATH_MAX) == 0 ||
        strncmp(entry.d_name, "..", PATH_MAX) == 0))
        readdir_r(dir, &entry, &entryPtr);

    return entryPtr;
}

Idris：

readdir_next : Ptr -> IO Ptr
readdir_next args = mkForeign (FFun "readdir_next" [FPtr] FPtr) args

read_d_name函数用于读取struct dirent结构中的d_name域：

C：

char *read_d_name(struct dirent *entry)
{
    return entry->d_name;
}

Idris：

read_d_name : Ptr -> IO String
read_d_name args = mkForeign (FFun "read_d_name" [FPtr] FString) args

is_st_mode_dir函数根据struct stat的st_mode域判断该entry是否为一个文件夹。因为C89没有bool类型，故这里返回一个非0的int值表示是文件夹，否则返回0。

C：

unsigned int is_st_mode_dir(char *path)
{
    struct stat entryInfo;

    if (lstat(path, &entryInfo) == 0)
        return S_ISDIR(entryInfo.st_mode);
    else
        return 0;
}

在Idris中，我们可以根据判断C foreign function的返回值是否为0把它转成IO Bool类型。

Idris：

is_st_mode_dir : String -> IO Bool
is_st_mode_dir args =
  mkForeign (FFun "is_st_mode_dir" [FString] FInt) args >>=
    return . (/= 0)

read_st_size函数读取struct stat的st_size域，返回文件entry的大小：

C：

off_t read_st_size(char *path)
{
    struct stat entryInfo;

    if (lstat(path, &entryInfo) == 0)
        return entryInfo.st_size;
    else
        return 0;
}

Idris：

read_st_size : String -> IO Int
read_st_size args = mkForeign (FFun "read_st_size" [FString] FInt) args

剩下来的工作，只需要直接在Idris中创建 closedir()和remove()这两个系统调用即可：

closedir : Ptr -> IO ()
closedir args = mkForeign (FFun "closedir" [FPtr] FUnit) args

remove : String -> IO Int
remove args = mkForeign (FFun "remove" [FString] FInt) args

命令选项`Option`

我们约定，所有系统函数的第一个参数为我们自定义的List Option类型，表示需要传递的附加命令选项；第二个参数表示真正需要处理的值。

data Option = All | NoDir | Rec | OnePerLine

是否忽略以'.'打头的文件名。

-- Do not ignore entries starting with .
is_All : Option -> Bool
is_All All = True
is_All _ = False

是否处理文件夹。

-- Do not list directory entries
is_NoDir : Option -> Bool
is_NoDir NoDir = True
is_NoDir _ = False

是否递归地处理子文件夹。

-- List subdirectories recursively
is_Rec : Option -> Bool
is_Rec Rec = True
is_Rec _ = False

是否每行仅列出一项。（用于标准输出）

-- List one entry per line
is_OnePerLine : Option -> Bool
is_OnePerLine OnePerLine = True
is_OnePerLine _ = False

`ls`的实现

-- List directory contents
ls : List Option -> List String -> List String
ls options targets = ls' targets
  where
    -- Do not ignore entries starting with .
    has_All : Bool
    has_All = any is_All options

    -- Do not list directory entries
    has_NoDir : Bool
    has_NoDir = any is_NoDir options

    -- List subdirectories recursively
    has_Rec : Bool
    has_Rec = any is_Rec options

到这里，我们定义了三个函数has_All、has_NoDir、has_Rec，它们用来检查options中是否存在相应的选项。

该辅助函数用来检查文件名是否以'.'打头（隐藏）：

    -- Check if a name starts with .
    isEntryHidden : String -> Bool
    isEntryHidden name = case unpack name of
      '.' :: _ => True
      _ => False

主要的实现部分：

    lsPath : String -> List String
    lsPath path = unsafePerformIO $
      do
        dir <- opendir path
        result <- lsDir dir
        closedir dir
        return result
      where
        lsDir : Ptr -> IO (List String)
        lsDir dir = do
          entry <- readdir_next dir
          isNull <- nullPtr entry
          if not isNull
            then do
              d_name <- read_d_name entry
              let myPath = path ++ "/" ++ d_name

              xs <- lsDir dir

              let isHidden = isEntryHidden d_name
              if not has_All && isHidden
                then -- Ignore hidden entry when required
                  return xs
                else do
                  isDir <- is_st_mode_dir myPath
                  if not isDir
                    then -- Normal file entry
                      return (myPath :: xs)
                    else do -- Process directory...
                      let recs = lazy lsPath myPath

                      -- Recurse into subdirectory when required
                      return (has_Rec ? recs ++ xs : xs) >>=
                        has_NoDir ? -- Ignore directory entry when required
                          return
                        : -- Normal directory entry
                          return . (myPath ::)
            else
              return []

    ls' : List String -> List String
    ls' [] = []
    ls' (x :: xs) = lsPath x ++ ls' xs

在熟悉Haskell的前提下，基本可以毫无障碍地读懂用Idris写成的代码。但这里有几点仍然需要特别说明一下：

lsPath函数是实现的主要部分，它根据一个路径名返回所有文件名称的String List。
- 因为访问了文件系统，而返回值的类型又必须是一个List，所以我们在这里直接使用了unsafePerformIO来处理IO monad。
- 你可以认为“读文件系统”这个操作没有产生任何副作用，但显然这么做是有问题的。具体的分析放在后面。
在决定是否递归访问文件夹结构之前，lazy可以避免不必要的求值。这个问题在Haskell中不存在，但Idris是一种严格求值的语言。
- 当然，还可以有别的解决方式。这也将在后面提到。

Composition over Coupling

在面向对象的设计中，“Composition over inheritance”是一条重要的原则。

简单地讲就是：如果说法拉利Enzo需要一个V12引擎，LaFerrari需要一个V12引擎，那么最好的设计方式是把“引擎”这件东西抽象出来作为一个单独的类，而不是笼统地说：LaFerrari继承了Enzo，包括继承了它的V12引擎。把完成某特定子功能的、可以被重用的部分抽象出来作为一个独立的组件开发，这是较为合理的工程学方法。

在函数式编程中亦是如此。如果软件的一项功能是求得一个数据类型的值然后将其输出到文件；另一项功能是求得另一个同数据类型的值将其输出到文件。那么为这两项功能仅仅设计两个函数是不合理的；更好的选择是，考虑到这两种同类型的数据可以采取同一种方式输出，将其打印到文件的函数完全可以放到一个type class的instance中去定义。这样完成我们想要功能的部分就从一个单一的函数实现，变成了一个求值的纯函数与处理I/O的非纯函数的组合。Composition over coupling——Coupling意味着耦合度，意即功能上的相关性；而Composition可以更为直观地理解为函数的组合（function composition），越多的Composition象征着越高的聚合度。

这就是为什么我们应该让ls只返回一个求值结果的List，而不是同时做“求值”和“标准输出”这两件事情的原因。

更进一步，你会注意到我们前面定义的ls的目标参数是一个List。这不是必需的，因为你知道，如果ls能处理一个String，那么理所当然也能用它来处理一个List String——只要通过适当的函数组合就能达到我们的目的。如果需要有一个能够处理List参数的函数（假定它叫lss），那么至少我们可以把“处理单个String参数”的ls函数抽出来，然后把lss定义为ls和map的组合。问题解决。

从现在起，我们定义的函数均为处理单个参数，不再处理更多的List。

`fileSize`的实现

这个函数用来返回一个文件的大小（字节）。它的定义非常简单：

fileSize : List Option -> String -> Int
fileSize options file = unsafePerformIO $ read_st_size file

`rm`的实现

显而易见，rm必须放在IO Monad里去实现。它的返回值遵循POSIX惯例，为0则表示执行成功。

rm : List Option -> String -> IO Int
rm options = remove

如果要想显式地输出这个返回的Int值，可以为Show的type class创建一个instance：

instance Show a => Show (IO a) where
  show x = show $ unsafePerformIO x

System Call is Never Pure

在前面，我们已经完成了一些系统函数在Idris中的类型定义。在继续下去以前，我想问一个问题：它们是“纯”的吗？

rm操作修改了文件系统的状态，很显然它不是；问题在于我们用来“读”文件系统的这个ls函数。

记住这一点：系统调用永远是有副作用的，哪怕是只读不写的操作，也不例外；原因就在于人无法两次踏进同一条河流。操作系统与它的环境无法被抽象成某个可预测的数学模型，它的状态是可以随时改变的；上一个时间点对ls求值的结果很可能与下一个时间点求值的结果不同，类似种种的系统底层API，也就不符合函数式语言中对“纯函数”的定义——数学函数的定义是一个已知的从定义域到值域的映射，从函数的输入可以精确地计算出唯一的输出。而系统调用的行为并不符合这个定义。这也就是为什么Haskell和Idris这样的纯函数式语言要把所有调用C的FFI都默认放在IO Monad中去实现一样，因为确实除了少数做纯数学计算的函数（如math.h中的sin()、cos()），其他大多数C函数多半是不符合“纯函数”这个定义的。

结论是，ls求值的结果，虽然看来是一个List且无副作用，但是从本质上讲它并不是一个函数式的List；我们应该把它塞到一个IO List里去，这从纯函数和线程安全的角度考虑似乎更正确。

`echo`和标准输出符

到目前为止，我们所定义的函数仍然没有任何执行标准输出的能力。现在，可以实现这样一个把任意List输出到终端的函数：

echo : Show a => List Option -> List a -> IO ()
echo options = echo'
  where
    -- List one entry per line
    has_OnePerLine : Bool
    has_OnePerLine = any is_OnePerLine options

    echo' : Show a => List a -> IO ()
    echo' = has_OnePerLine ? sequence_ . map print : print

考虑到在未来的脚本程序中，标准输出会是非常常见的操作，我们定义这样一个前缀运算符：

prefix 0 #
(#) : Show a => a -> IO ()
(#) = print

它会把后面表达式求值的结果直接输出到终端。

文件重定向符

在Unix shell中，用>符号把标准输出重定向到文件的用法十分便利。在我们这个Shell的namespace中，同样可以定义这样的中缀运算符，让它覆盖Prelude中的原定义：

(>) : Show a => |(contents : a) -> String -> IO Int
contents > fileName = do
  output <- openFile fileName Write
  outputError <- ferror output
  outputFileValid <- validFile output
  status <-
    if not outputError && outputFileValid
      then do
        fwrite output $ show contents
        return 0
      else
        return (-1)
  closeFile output
  return status

这个也可以有：

(>>) : Show a => |(contents : a) -> String -> IO Int
contents >> fileName = do
  output <- fopen fileName "a"
  outputError <- ferror output
  outputFileValid <- validFile output
  status <-
    if not outputError && outputFileValid
      then do
        fwrite output $ show contents
        return 0
      else
        return (-1)
  closeFile output
  return status

注意contents参数采取了惰性求值方式，这样可以避免在文件写操作失败情况下不必要的求值。

管道机制

前面早就提到过，Unix的管道机制本身就可以和函数式编程中的概念加以类比。

现在，在我们的这个新Shell里面，将要定义4种管道运算符，它们有着不同的类型签名（实质上它们代表了函数式语言中的四个不同概念）。

1. Run-through `(|$)`

第一个管道符叫“Run-through”。

infixl 2 |$
(|$) : List a -> (List a -> List b) -> List b
(|$) = flip ($)

在Idris的标准库（Builtins.idr）中，flip和($)分别是这么定义的：

flip : (a -> b -> c) -> b -> a -> c
flip f x y = f y x

($) : (a -> b) -> a -> b
f $ a = f a

所以，我们刚才定义的东西事实上就等价于：

(|$) : List a -> (List a -> List b) -> List b
x |$ f = f x

你会说，这种东西定义出来有啥用？后面将展示它的实际用途。

2. Map `(|.)`

第二个管道相当于一个左右参数倒置的`map`。

infixl 2 |.
(|.) : List a -> (a -> b) -> List b
(|.) = flip map

3. Filter `(|&)`

第三个管道相当于一个左右参数倒置的`filter`。

infixl 2 |&
(|&) : List a -> (a -> Bool) -> List a
(|&) = flip filter

4. Foldl `(|+)`

对的，你一定已经猜到了，剩下最后一个要定义的，自然就是实现fold操作的管道！

infixl 2 |+
(|+) : List a -> (c -> a -> c) -> c -> c
(|+) xs f init = foldl f init xs

示例

现在，我们可以用前面的函数定义来做一些简单的系统任务了，

module Main
import Shell

main : IO ()
main = do
  echo [] $ ls [All, Rec, NoDir] ["db"]

它的作用是对ls [All, Rec, NoDir] ["db"]进行求值（递归地访问db/目录取得全部文件名的列表），并输出到终端。

加上OnePerLine选项让它每次输出一行：

  echo [OnePerLine] $ ls [All, Rec, NoDir] ["db"]

回想起前面定义过的标准输出符，我们有更简短的写法：

  # ls [All, Rec, NoDir] ["db"]

在REPL里当然可以直接使用：

ls [All, Rec, NoDir] ["db"]

来查看结果，不过这里是作为一个脚本程序运行，因此必须指定输出到终端。

输出文件的大小到终端：

  # fileSize [] "db/Movies.db"

以(文件名, 文件大小)的格式输出db/目录下的全部文件信息，借助Idris的List comprehension：

  # [ (f, fileSize [] f) | f <- ls [All, Rec, NoDir] ["db"] ]

利用Idris标准库函数中的sort，对文件名进行按ASCII顺序排序后输出：

  # sort (ls [All, Rec, NoDir] ["db"])

回想起我们前面定义的“Run-through”管道符，上面的写法其实可以等效改写为：

  # ls [All, Rec, NoDir] ["db"] |$ sort

这就是一个与Unix shell的管道非常相似的形式了。

我们也可以用Idris的map函数来对文件名的List执行操作，返回一个相应的文件大小列表：

  # map (fileSize []) (ls [All, Rec, NoDir] ["db"])

不过，既然有了现成的map管道符，以上的写法就可以等效成：

  # ls [All, Rec, NoDir] ["db"] |. fileSize []

同样，若要用filter过滤出所有文件中大小不为0的并输出：

  # filter ((> 0) . fileSize []) (ls [All, Rec, NoDir] ["db"])

它的仿Shell写法就是：

  # ls [All, Rec, NoDir] ["db"] |& (> 0) . fileSize []

对所有文件的大小进行求和：

  # foldl (flip $ (+) . fileSize []) 0 (ls [All, Rec, NoDir] ["db"])

等价于：

  # ls [All, Rec, NoDir] ["db"] |+ (flip $ (+) . fileSize []) $ 0

管道可以按照从左到右的顺序依次结合，这相当有用。如，定义获取文件扩展名的函数为：

extension : String -> String
extension s =
  let
    l : List String = reverse $ split (== '.') s
  in
    case l of
      x :: (y :: _) => x
      _ => ""

利用filter管道，找出db/下所有扩展名为.db的文件：

  # ls [All, Rec, NoDir] ["db"] |& (== "db") . extension

利用filter管道和map管道的结合，即可删除db/下所有扩展名为.db的文件：

  # ls [All, Rec, NoDir] ["db"] |& (== "db") . extension |. rm []

直接重定向输出到文件，这也十分容易做到：

  "hello, world" >> "output.txt"

  fileSize [] "db/Movies.db" > "output.txt"

Syntax is Important

上面给出了这么多例子，包括对Idris的一般写法和运用仿Shell管道符的写法进行了对比，其实只是为了说明一个道理：Syntax is important。

LISPer们喜欢声称语法（syntax）不重要，语法糖（syntactic sugar）是无益的；语义（semantics）才是程序语言的精髓。然而他们忘记了最重要的一点：Syntax是一种程序语言的User Interface。如果一个用户界面不去讨好用户反而去讨好编译器；如果一个用户界面反而不能让用户轻松地表达自己的思想，那么谈再多的semantics也毫无意义。

从我们的例子来看，首先，作为一个交互式shell，你设计的这种语言不能有过多的符号匹配；适当的空格和运算符都OK，但你不应该让用户敲命令的时候需要在脑子里面先建立一个栈，左括号进右括号出，这种反人类的表达方式注定要被自然选择所淘汰；其次，要有适当的中缀形式，比如，Unix shell的管道机制比起现有函数式语言中的map、filter，确实更容易被非程序员用户所理解，所以在新shell的设计中借鉴它们是理所当然的。

我们设计的shell其实做得还不够多。例如，为了吸收Zsh中的便利设计，应当支持直接使用目录名进入该目录的方式（在交互式shell中）；还应当支持在不引起歧义的情况下省略引号。但这在Idris的语言环境中我们做不到。

所以，未来的工作或许可以考虑以下两个方面，

一个完整的Shell interpreter或类似SML/NJ那样的interactive compiler。
一个REPL。显然，Idris自己的REPL非常不适合做Shell的交互式界面。

与Unix Shell的对比

最后简要地分析一下这个新的Typed shell与传统Unix shell之间的差异，当然，还有它自身存在的缺陷。

在Unix shell里：

find . -type f -name "*.db" -print0 | xargs -0 rm

这里管道的工作方式是：find和xargs命令同时被fork出独立的进程；find在执行过程中访问文件系统查找符合要求的文件，即时生成作为结果的字符stream，xargs负责即时接受这个stream，通过以NUL作为分隔符的方式解析出每个参数，然后将其传递给rm进程。Unix pipeline的缓冲机制可以确保这个stream的传输不受find和xargs处理效率不同步的影响。

而在这个新的Typed shell里，等效的写法为：

ls [All, Rec, NoDir] ["."] |& (== "db") . extension |. rm []

这段代码的执行方式是：对系统调用ls [All, Rec, NoDir] ["."]进行立即求值，求值的结果和lambda（(== "db") . extension）一同传递给filter函数（中缀形式的|&管道符），再次立即求值，求值的结果和lambda（rm []）一同传递给map函数（中缀形式的|.管道符），进行立即求值。

这比起传统的Unix shell来有哪些优/缺点呢？

优势很明显，

它基于一个full-fledged的程序语言（纯函数式的Idris，拥有可扩展的标准库，高度DSL表达能力），从语言本身的设计上大大超越了严重受限的Shell。
得益于类型系统，可以通过类型检查提供系统脚本本身的类型安全性，避开了无类型的Unix文本流导致的问题。

它最主要的缺陷，目前存在于两处：

系统调用不应被视作无副作用的纯函数，它应该一律放到IO Monad中去实现。这一点在前面已经提到过了。
我们采用Idris中的List取代了Unix用管道为进程间传递数据的方式，保证了类型的安全。但Unix管道仍然有一个重要的好处：它从本质上说是基于stream的。

很明显，stream的优势是按需求值，而不是一次性把所有值全部求出来之后才执行下一步操作；这对于处理较大的数据集，或者我们的程序干脆需要这种stream的工作方式时尤其有用。

Haskell对于解决这件事情具有先天的优势，它可以通过惰性求值的方式来处理它的List。

而在许多严格求值的语言中，亦可通过创建thunk的方式来实现这种按需求值的“List”，这种数据类型在ML和Scala中被称作Stream。它和Unix管道中所说的stream从理念上是非常接近的。

TIPS： 在所谓的“强函数式语言”中，所有的函数必须都是完整的（total），意即：函数对于其参数类型域中的每一个取值都必须有定义，这是一个程序总是能停机（即判定器）的必要非充分条件之一；在强函数式语言中，Church–Rosser定理完全成立。这使得在强函数式语言中，急性求值和惰性求值的结果将完全相同。

Idris是一个强函数式语言（而Haskell对惰性求值的某些处理方式决定了它不是强函数式的，这点可参见Idris FAQ：Why isn't Idris lazy?）。在强函数式语言中，为了实现类似于“惰性求值的List”（或Stream）的数据结构，需借助于codata类型：

codata Stream a = Nil | (::) a (Stream a) 

countFrom : Int -> Stream Int 
countFrom x = x :: countFrom (x + 1) 

take : Int -> Stream a -> List a 
take 0 _ = [] 
take n (x :: xs) = x :: take (n - 1) xs 
take n [] = [] 

main : IO () 
main = do print (take 10 (main.countFrom 10))

结合以上两点，可以考虑采用Stream对ls函数进行重新定义：

ls : List Option -> String -> IO Stream

（To be continued…）

Google Reader