Jenkins X 初体验

前言

Jenkins X 是一个高度集成化的CI/CD平台，基于Jenkins和Kubernetes实现，旨在解决微服务体系架构下的云原生应用的持续交付的问题，简化整个云原生应用的开发、运行和部署过程。

官方链接: http://jenkins-x.io/

安装（for macOS）

• install Jenkins X with brew

  brew tap jenkins-x/jx
  brew install jx
  

  

  

• 输入 jx 应该能看到如下输出

  

• create local cluster for test

  jx create cluster minikube
  

  

  这个过程比较长，有几个步骤

  1. 为 minikube 分配内存、CPU、driver

     

  2. 之后会下载 minikube 的镜像与 localKube 的 binary，并启动 kubernetes, 设置 RBAC

     

  3. jx 使用 helm 来管理 kubernetes 上的应用，所以会在 k8s 上初始 helm 的 server(tiller)。

     

  4. 安装 NGINX Ingress Controller

     

  5. 设置 Github 的 API Token，点击生成的 URL，生成一个 API Token

     

  6. 设置 Jenkins 的 API Token

     

  7. 等待一段时间，jx 会在 k8s 上部署包括 jenkins、nexus等应用，部署完成会出现

     

使用

这里可以参考官方 demo: demonstration of Jenkins X

感受

在使用 Jenkins X 的时候，感觉还是有些坑的，我简单地罗列了一下：

1. 确保你的 kubectl 的版本要 >= 1.6
2. 对于较高版本的 macOS，需要升级 homebrew
3. 在使用 minikube delete 的时候遇到了一下系统权限的问题，可能是 Bug

其实 jx 是简单地整合了 CI & CD 在云原生应用上的工具链，包括 Helm 、k8s、Draft，对于用户而言，隐藏了很多繁琐的配置。但从目前的版本上看，jx才刚刚起步，我们可以看到在其官方的 roadmap 中，关于 Tools、Git Providers、Issue Trackers 方面还有很多路要走，这肯定需要开源社区的努力，另外在企业定制化方面可能也需要有更多的思考，这是一个通用的工具链不得不面对的问题。

关于 jx 的未来，我们拭目以待。

EDSL With Typed Lambda Calculus Implemented In Haskell

Abstract

Haskell是一种丰富的语言，它具有各种扩展功能。另外，我们可以将我们定义的语言(比如DSLs)中的lambda表达式embed到或者映射到Haskell中的lambda表达式中，这就是所谓的HOAS(Higher Order Abstract Syntax)。同时我们可以利用FInally Tagless，可以将HOAS表示成SKI Combinator的形式，最后可以添加Y Combinator实现带类型的计算，同时还能拥有很好的extensibility与类型安全。

Binding

Lambda演算虽然非常简单，但是在计算与实现Lambda表达式规约上却有很多方法，主要是在计算策略上的不同，按模型主要分为三类：

1. Call-by-value:arguments are evaluated before a function is entered
2. Call-by-name:arguments passed unevaluated
3. Call-by-need:arguments passed unevaluated but an expression is only evaluated once and shared upon subsequent references

在不同模型下的规约步骤不同:

Call-by-value:

1. Evaluate x to v
2. Evaluate f to λy.e
3. Evaluate [y/v]e

Call-by-name:

1. Evaluate f to λy.e
2. Evaluate [y/x]e

Call-by-need:

1. Allocate a thunk v for x
2. Evaluate f to λy.e
3. Evaluate [y/v]e

不管是哪种模型什么策略，都会遇到一个问题，即最后一步做substitution的时候，该如何正确地表示binding。最朴素的想法，substitution就是替换，我们完全可以将后面的expression看做字符串去替换前面变量所有的出现，这样就是一个简单的字符串匹配的问题了，用Haskell强大的模式匹配很快就能解决，代码如下:

data Expr = Var String | Abs String Expr | App Expr Expr deriving (Show, Eq)

eval :: Expr -> Expr 
eval (Var x) = Var x 
eval (Abs x e) = Abs x (eval e)
eval (App l@(Var _) r) = App l (eval r)
eval (App l@(App _ _) r) = eval (App (eval l) (eval r))
eval (App (Abs x l) r) = 
    eval (subst l) where
    subst (Var x') | x == x' = r
    subst (Var x') | x /= x' = Var x'
    subst (Abs x' y) | x == x' = Abs x' y
    subst (Abs x' y) | x /= x' = Abs x' (subst y)
    subst (App ll lr) = App (subst ll) (subst lr)

考虑这样的一个Lambda表达式\y(\x\y x)y

term = Abs "y" (App (Abs "x" (Abs "y" (Var "x"))) (Var "y"))
main = putStr $ show $ eval term

运行结果为Abs "y" (Abs "y" (Var "y"))，这样语义就改变了(\x \y x -> \y y变成了与y变量有关的函数)。

所以单纯的字符串替换是不行的，他不能看到一个Lambda表达式中的语义信息所以会出现改变语义的substitution，我们需要需求一种替换，不会出现语义改变的问题，这种替换被称为capture-avoiding substitution（CAS）。

一种主流的方法是将语言embed到另一种metalanguage中，这样我们就借来了metalanguage中的binding，这叫做HOAS。

data Expr = Lam (Expr -> Expr) | App Expr Expr

我们定义Expr方式也与定义普通的Lambda function类似，同时对表达式的计算也变得简单了，可以简单地使用Haskell来计算。

y = Lam (\f -> let e = Lam (\x -> App f (App x x)) in App e e)

eval (Lam l) = Lam l
eval (App (Lam l) r) = eval (l r)
eval (App l r) = eval (App (eval l) r)

这样的形式目前看来很不错，很好并且很优雅地解决了binding的问题，但是这样的形式是不是完美的呢？很显然存在很多麻烦之处。

首先，我们需要更多时间考虑怎么把一个expression转换成这种的形式，因为我们需要使用Haskell本身的Lambda binder。另外，由于所有的机制都包在Haskell的实现里面，所以即使像PretyPrint/Optimization/writing transformation passes这种简单的操作都会变得异常困难，我们很难看到一个函数本身的结构。所以这种形式只是适合计算的一种很好的形式，并不适合通用的转换。那么我们能不能找到一种方法在保留HOAS优势的同时简单地支持这些操作呢？

Expression problem

首先来看一个expression的问题。这里用经典的“Hutton’s Razor”作为例子，它是使用加法运算+从整数文字建立的简单算术表达式的语言，在Haskell中可以这么表示：

data Exp = Lit Int | Add Exp Exp

这样，比如表达式(1+(2+3))就可以写成：

e1 = Add (Lit 1)
         (Add (Lit 2)
               (Lit 3))

给他写一个eval能够计算形如上面的表达式的值:

eval :: Exp -> Int
eval (Lit n)   = n
eval (Add x y) = eval x + eval y

我们可以很简单的为我们的Exp增加一个函数（比如pretty printing）:

prettyprint :: Exp -> String
prettyprint (Lit n) = show n 
prettyprint (Add x y) = "(" ++ prettyprint x ++ "x" ++
                        prettyprint y ++ ")"

并且不会影响到Exp的extensibility与type safe(我们根本不需要对Exp的constructor进行改变)。但是，当我们试着对我们定义的这个语言表达式做运算符的拓展的时候(比如添加一个乘法运算*)，事情好像就比较麻烦了。首先需要在数据类型Exp中增加一个Mult的constructor，我们还需要在每个涉及到Exp的function中添加case，比如上面的eval与prettyprint。真实世界事件的规模比我们举的这个例子大很多，存在多涉及到类似定义的数据类型的function，作为一个代码的维护者，必须极其小心检查每个function并为每个function加上独特的case——十分煎熬。所以这样的方法不能在为数据类型增加constructor的时候同时保持我们语言的extensibility与type safe。

这是用函数式语言会遇到的问题，我们再尝试用OO的语言实现，看有没有相同的问题。

在Java中定义一个Exp的接口，提供一个抽象方法eval()，上面每个constructor都可以写成继承这个Exp的类，并且实现它的抽象方法:

interface Exp {
    int eval();
}

class Lit implements Exp {
    int n;
    Lit(int n) { this.n = n; }
    int eval() { return n; }
}

class Add implements Exp {
    Exp x, y;
    Add(Exp l, Exp r) { this.x = l; this.y = r; }
    int eval() { return x.eval() + y.eval(); }
}

尝试为其添加一个*运算，会发现简单很多，简单地再继承一下：

class Mult implements Exp {
  Exp x, y;
  Mult(Exp l, Exp r) { this.x = l; this.y = r; }
  int eval() { return x.eval() * y.eval(); }
}

我们不需要碰到其他地方，只用简单地再增加实现一个类就行了。这么看来刚刚函数式语言的问题得到了很好的解决，但是同时带来了新的问题，添加新的方法（比如prettyprint）显得很困难，我们需要对每个class分别实现，即问题完全反过来了。

这种问题被称作expression problem，有一种很直观的解释。

考虑这样的长方形表格，列代表操作，行代表表达式的类型。表格中的元素代表相关类型的相关操作。

	Eval
Lit
Add

在函数式语言中，这个表格中元素的定义是以列为单位的。一列所代表的函数表示一个对所有表达式类型的操作。所以在添加一个新的操作(function)的时候即添加新一列的时候很简单。但是在表达式类型即行这个维度上的可扩展性就没这么强了，因为对每列添加一个新行，每个交都是一个新的case，所以很困难。

	Eval	Prettyprint
Lit
Add
Mult

在面向对象的语言中，表格中元素的定义是由行组织的。每行所代表的表达式类型包含了这个类型下所有的操作(function)。所以对于面向对象语言而言，对于表达式类型的扩展是比较简单的，事实上只要添加一个新的Class。然而添加新的操作即在表格中添加一列比较困难，因为我们要在每个相关的class里面添加这个方法。

于是expression problem呼之欲出：能否在这个表格的横纵两个维度上都保持很好的扩展性同时又不失static guarantees且无需修改已有的代码呢？

Object algebras & finally tagless

Object algebras是一个比较新的用来解决expression problem的OO设计模式。它是在“Extensiblity for the Masses”这篇文章中提出的，之所以收到推崇是因为他用相当简洁优雅的方式解决了expression problem，不需要对现有语言本身做拓展，在主流语言Java或者C#中就能实现。

Object algebras的主要想法与软件工程中的抽象工厂模式很像，即定义一个接口与其中的抽象方法，这样我们就可以用这个工厂来表示表达式，并生产具体的操作工厂。Java代码如下：

interface ExpAlg<T> {
    T lit(int n);
    T add(T x, T y);
}

interface Eval { int eval(); }

class EvalExp implements ExpAlg<Eval> {
    Eval lit(final int n) {
        return new Eval() {
            int eval() {
                return n;
            }
        };
    }
    Eval add(final Eval x, final Eval y) {
         return new Eval() {
             int eval() {
                 return x.eval() + y.eval();
             }
         };
    }
}

这样表达式(1 + (2 + 3)) 可以表示为:

<T> T e1(ExpAlg<T> f) {
    return f.add(
        f.lit(1),
        f.add(
            f.lit(2),
            f.lit(3)));
}

很简单地来计算e1的值:

int v1 = e1(new EvalExp()).eval();

首先来看看怎么在我们的语言中添加新的表达式类型‘乘法’。第一个想到的方法当然是在我们所定义的接口ExpAlg<T>中添加新的方法Mult，那么就回到了我们刚刚遇到的问题。

不改变原有的代码，考虑定义一个新的interface来 extends 我们之前定义的“工厂”：

interface MulAlg<T> extends ExpAlg<T> {
    T mul(T x, T y);
}

同时对这个新的表达式类型的计算该怎么实现呢，也很简单与前面类似extends EvalExp类即可：

class EvalMul extends EvalExp implements MulAlg<Eval> {
    Eval mul(final Eval x, final Eval y) {
        return new Eval() {
            int eval() {
                return x.eval() * y.eval();
            }
        };
    }
}

这样我们做到了在完全不触碰到原有的代码情况下添加了新的表达式类型‘乘法’。

再来看看如何添加新的操作(function)，比如prettyprint。定义一个新的接口，并且实现用它生产具体的工厂：

interface Prettyprint { String prettyprint(); }

class PrettyprintExp implements ExpAlg<Prettyprint> {
    Prettyprint lit(final int n) {
        return new Prettyprint() {
            String Prettyprint() {
                return Integer.toString(n);
            }
        };
    }
    ...
}
class PrettyprintMul extends PrettyprintExp implements MulAlg<Prettyprint> {
    Prettyprint mult(final Prettyprint x, final Prettyprint y) {
        return new Prettyprint() {
            String Prettyprint() {
                return "(" + x.Prettyprint() + " * " + y.Prettyprint() + ")";
            }
        };
    }
}

这里抽象工厂接口ExpAlg<T>被称为对象代数接口，实现它的具体工厂称为对象代数。这个方法是受抽象代数的启发，抽象代数中代数结构由签名描述，签名作为一个接口，说明了在代数结构的基础集上定义的操作类型，一个代数提供这些操作的具体定义，类似于实现接口的类。

我们现在把上面的例子从Java代码转成Haskell代码，从而实现finally tagless。这个方法是在“Finally Tagless, Partially Evaluated”这篇文章中提出的。

Java中的interface对应Haskell中的Typeclass,class对应instance：

class ExpAlg t where
    lit :: Int -> t
    add :: t -> t -> t

newtype Eval = Eval { eval :: Int }

instance ExpAlg Eval where
    lit n   = Eval n
    add x y = Eval $ eval x + eval y

现在可以两边扩展了：

instance MulAlg Eval where
    mul x y = Eval $ eval x * eval y

newtype Prettyprint = Prettyprint { prettyprint :: String }

instance ExpAlg Prettyprint where
    lit n   = Prettyprint $ show n
    add x y = Prettyprint $ "(" ++ prettyprint x ++ " + " ++ prettyprint y ++ ")"

instance MulAlg Prettyprint where
    mul x y = View $ "(" ++ prettyprint x ++ " * " ++ prettyprint y ++ ")"

这里的形式已经和“Finally Tagless, Partially Evaluated”中所提出的基本相同了，只不过在Haskell中不需要将MulAlg定义成ExpAlg的subclass，我们可以直接独立的定义这个typeclass：

class MulAlg t where
    mul :: t -> t -> t

这样所有含有乘法类型的表达式的类型值为(ExpAlg t, MulAlg t) => t。我们同样不需要更改已有的代码便能实现两边的扩展。

这里用到的“Hutton’s Razor”的例子所涉及到的都是Int类型，如果我们想在这个语言里面加入double，该如何实现呢？

答案是用Phantom types。我们给ExpAlg一个类型变量这样t从Type变成了Type->Type.

class ExpAlg t where
    litI :: Int -> t Int
    plusI :: t Int -> t Int -> t Int
    litD :: Double -> t Double
    plusD :: t Double -> t Double -> t Double

注意到表达式ExpAlg并没有t这个值，所以我们称其为phantom type，它只是个假变量用来限制表达式的类型。

The very beginning problem

那么我们能不能找到一种方法在保留HOAS优势的同时简单地支持这些操作呢？

现在我们有这样一个typeclass:

class Language t where 
    app :: t (a -> b) -> t a -> t b
    ...(more method)

而且我们需要这样一个函数lam:

lam :: Language t => (t a -> t b) -> t (a -> b)

在language class中并没有接受这个函数的constructor，或许我们可以实现instance Language PrettyPrint？

很明显方法是不可行的，我们没有办法得到一个t (a -> b)这么个东西，Theorems for Free!这篇文章中给了具体的证明。

所以想法变成了能不能改变t这个类型签名，而且我们为了要生成一个t (a->b)给app，所以假设新的类型签名为unknown，则现在lam：

lam :: (unknown a -> unknown b) -> t (a -> b)

而且我们是可以生成unknown a的，通过得到一个unknown b就可以转换为t (a -> b)。

unknown的类型呼之欲出：unknown x = t (a -> x)。

根据自反性，我们很快得到一个unknown a(t (a -> a))。

我们也可以通过一个unknown b生成t (a -> b)（本身即是）。

现在我们可以写出unknown了把它取名为Next：

newtype Next t a b = Next { unNext :: t (a -> b)}

lam :: SKI t => (Next t a a -> Next t a b) -> t (a -> b)
lam f = unNext $ f (Next i)

再来看看我们需要在我们的Language中添加什么，首先我们需要一个unknown a，即t (a -> a)，返回自身的一个method。同时为了用户能在lam中用到原来的term需要再添加一个conv:: t a -> Next t b a，在Language中添加一个t a -> t (b -> a)。现在看看我们的Language是不是完备了：

class Language t where
    app :: t (a -> b) -> t a -> t b
    i :: t (a -> a)
    k :: t (a -> b -> a)

instance Language t => Language (Next t a) where
    app :: Next t a (b -> c) -> Next t a b -> Next t a c
    app = undefined
    i = conv i
    k = conv k

conv :: Language t => t a -> Next t b a
conv x = Next (app k x)

理论上来说我们要把原来class中的基本construct lisft到Next里面去，现在i与k都可以实现，但是会发现app无法lift进Next里的。这里unwrap掉app的类型，会得到：

app :: t (a -> b -> c) -> t (a -> b) -> t (a -> c)

如果对组合逻辑熟悉的话，可以发现这其实就是SKI组合子中的S，所以只要把这个类型作为基础method加入我们的Language里，然后用conv实现就可以了。这样我们的Language整个就是SKI Combinator。它对于无类型的Lambda演算来是完备的，如果我们的language是有类型的话，可以手动再加上一个Y Combinator。事实上这并不是minimal的系统，因为I还可以用S、K来表达：SKKx → Kx(Kx) → x

SKI组合子的实现:

{-# LANGUAGE
    MultiParamTypeClasses,
    RankNTypes,
    ScopedTypeVariables,
    FlexibleInstances,
    FlexibleContexts,
    UndecidableInstances,
    IncoherentInstances,
    PolyKinds #-}

class SKI t where
    app :: t (a -> b) -> t a -> t b
    s :: t ((a -> b -> c) -> (a -> b) -> a -> c)
    k :: t (a -> b -> a)
    i :: t (a -> a)

newtype Prettyprint x = Prettyprint { prettyprint :: String }

instance SKI Prettyprint where
    app f x = Prettyprint $ "(" ++ prettyprint f ++ " " ++ prettyprint x ++ ")"
    s = Prettyprint "S"
    k = Prettyprint "K"
    i = Prettyprint "I"

data Next t a b = Fast (t b) | Slow (t (a -> b))

unNext :: SKI t => Next t a b -> t (a -> b)
unNext (Slow x) = x
unNext (Fast x) = app k x

instance SKI t => SKI (Next t a) where
    app (Fast f) (Fast x) = Fast $ app f x
    app (Slow f) (Slow x) = Slow $ app (app s f) x
    app (Slow f) (Fast x) = app (Slow f) (Slow $ app k x)
    app (Fast f) (Slow x) = app (Slow $ app k f) (Slow x)
    s = Fast s
    k = Fast k
    i = Fast i

lam :: SKI t => (Next t a a -> Next t a b) -> t (a -> b)
lam f = unNext $ f (Slow i)

c :: SKI t => t ((a -> b -> c) -> b -> a -> c)
c = lam (\abc -> lam (\b -> lam (\a -> app (app (Fast $ Fast abc) a) $ Fast b)))

main :: IO ()
main = putStrLn $ prettyprint c

输出结果：

((S ((S (K S)) ((S (K K)) ((S (K S)) ((S ((S (K S)) ((S (K K)) I))) (K I)))))) (K ((S (K K)) I)))

现在我们再回到“Hutton’s Razor”这个例子并给他加上SKI Combinator：

class ExpAlg t where
    lit :: Int -> t Int
    add :: t (Int -> Int -> Int)

class SKI r where
    app :: r (a -> b) -> r a -> r b
    s :: r ((a -> b -> c) -> (a -> b) -> a -> c)
    k :: r (a -> b -> a)
    i :: r (a -> a)

newtype Prettyprint n = Prettyprint { prettyprint :: String }

instance ExpAlg Prettyprint where
    lit n   = Prettyprint $ show n
    add = Prettyprint "add"

instance SKI Prettyprint where
    app f x = Prettyprint $ "(" ++ prettyprint f ++ " " ++ prettyprint x ++ ")"
    s = Prettyprint "S"
    k = Prettyprint "K"
    i = Prettyprint "I"  

newtype Eval x = Eval { eval :: x }

instance ExpAlg Eval where
    lit n   = Eval n
    add = Eval $ (+)

instance SKI Eval where 
    app f x = Eval $ eval f $ eval x 
    s = Eval (\abc ab a -> abc a (ab a))
    k = Eval const
    i = Eval id

data Next t a b = Fast (t b) | Slow (t (a -> b))

unNext :: SKI t => Next t a b -> t (a -> b)
unNext (Slow x) = x
unNext (Fast x) = app k x

instance SKI t => SKI (Next t a) where
    app (Fast f) (Fast x) = Fast $ app f x
    app (Slow f) (Slow x) = Slow $ app (app s f) x
    app (Slow f) (Fast x) = app (Slow f) (Slow $ app k x)
    app (Fast f) (Slow x) = app (Slow $ app k f) (Slow x)
    s = Fast s
    k = Fast k
    i = Fast i

instance ExpAlg t => ExpAlg (Next t a) where
    lit x = Fast (lit x)
    add = Fast add

class NT l r where
    conv :: l t -> r t

instance NT l r => NT l (Next r a) where
    conv = Fast . conv

instance NT x x where
    conv = id

instance NT (Next r a) (Next r a) where
    conv = id

lam :: forall r a b. SKI r =>
 ((forall k. NT (Next r a) k => k a) -> (Next r a) b) -> r (a -> b)
lam f = unNext $ f (conv (Slow i :: Next r a a))

c :: SKI t => t ((a -> b -> c) -> b -> a -> c)
c = lam (\abc -> lam (\b -> lam (\a -> app (app abc a) b)))

double :: (SKI r , ExpAlg r )=> r (Int -> Int)
double = lam (\x -> app (app add x) x)

main :: IO ()
main = putStrLn $ prettyprint double

double这个函数将输入的数加倍，用我们的language输出为：

((S ((S (K add)) I)) I)

如果我们再加上Y Combinator就可以实现这个表达式的计算：

Fix (((S ((S (K add)) I)) I))

其中eval (Fix f) = (eval f) (eval (Fix f))。

Conclusion

为了实现一个embed domain specified language(EDSL)，我们首先考虑用Haskell这个metalanguage用HOAS来实现lambda表达式的binding。同时为了解决expression problem我们用tagless的方法将lambda表达式用SKI Combinator的方式来表示，让我们能“看进”一个lambda表达式，了解他的结构，实现诸如prettyprint的功能。

这样我们的EDSL拥有了如下的feature：

1. 支持typed的lambda calculus。
2. type safe，可以利用Haskell的类型系统。
3. 有很好的extensibility，方便地添加类型、方法，易于维护。

References

Expression problem

Extensibility for the Masses

Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages

From Object Algebras to Finally Tagless Interpreters

Haskell/GADT

Lambda calculus

macOS Sierra下配置spacemacs+proof-general+coq

1. 替换homebrew现有的上游，这里使用清华源。(如果之前已经配置过可以无视~)

   $ cd "$(brew --repo)"
   $ git remote set-url origin https://mirrors.tuna.tsinghua.edu.cn/git/homebrew/brew.git
   
   $ cd "$(brew --repo)/Library/Taps/homebrew/homebrew-core"
   $ git remote set-url origin https://mirrors.tuna.tsinghua.edu.cn/git/homebrew/homebrew-core.git
   
   $ brew update
   

2. 用homebrew下载proof-general

   $ brew install proof-general
   

3. 用homebrew下载emacs-plus

   $ brew tap d12frosted/emacs-plus
   $ brew install emacs-plus
   $ brew linkapps emacs-plus
   

4. 如果之前没有Emacs configuration，(可以看看有没有文件夹~/.emacs.d，没有的话就是之前没有配置过)，直接git clone spacemacs即可

   $ git clone https://github.com/syl20bnr/spacemacs ~/.emacs.d
   

   如果目录下已经有文件了，不想保存之前的配置的话，直接rm -rf删除文件夹即可，如果想保留之前的配置，这里)有详细的说明。

5. 先启动一次，更新一些配置，并且设置一些初始的选项，比如使用vim模式还是其他的等等，这里按照个人喜好即可。之后在根目录会生成spacemacs的配置文件.spacemacs。

   $ emacs --insecure
   

6. 下载spacemacs-coq layer，并在~/.spacemacs文件里的dotspacemacs-configuration-layers中添加coq的支持。

   git clone https://github.com/olivierverdier/spacemacs-coq ~/.emacs.d/private/coq
   

7. 更改emacs package的安装源，同样修改~/.spacemacs文件，user-init中添加：

   (setq configuration-layer--elpa-archives
     '(("melpai-cn" . "http://elpa.zilongshanren.com/melpa/")
       ("org-cn"   . "http://elpa.zilongshanren.com/org/")
       ("gnu-cn"   . "http://elpa.zilongshanren.com/gnu/")))
   

8. 重新启动emacs，等待自动安装Company-Coq，这样就配置完成啦。

PS：在此之前我已经安装了过了OCaml与CoqIDE

说一说‘Monads’

1.关于范畴论

范畴论是数学的一门学科，以抽象的方法来处理数学概念，将这些概念形式化成一组组“物件”及“态射”。范畴论是对数学的某些分支的更高阶的抽象化，所以被称为“一般化的抽象废话”。

• 函子

  将范畴再抽象一次（范畴自身也是数学结构的一种），寻找在某一意义下会保持其结构的过程，我们把这一过程称为函子，这实际上是定义了一个包含“范畴和函子”的范畴，元件为范畴，态射为函子。

  一个从范畴 C 到范畴 D 的函子 F 被定义为：

  • 对 C 中任意物件 X ，都有一个 D 中相应的物件 F(X) 与其对应；
  • 对 C 中任意态射 f : X → Y ，都有一个 D 中相应的态射 F(f) : F(X) → F(Y) 与其对应；

  并使下列性质成立：

  • 对 C 中任意的物件 X ，都有 F(idX) = idF(X) 。
  • 对 C 中任意两个态射 f : X → Y 和 g : Y → Z，都有 F(g · f) = F(g) · F(f) 。

  将范畴映射到自身的函子被称为“自函子(Endofunctor)”。

• 组成

  一个范畴‘C’是由三个部分组成：

  • 1.一个类ob(C)，里面的元素称为“物件”

  • 2.一个类hom(C)，其元素为“态射”或“箭号”。每个态射f 都只有一个“源物件”a 及一个“目标物件”b（其中a 和b 都在ob(C) 内），称之为“从a 至b 的态射”，标记为f : a → b。

  • 3.一个二元运算，称为“态射复合”，使得对任意三个物件a、b 及c，都会有hom(b, c) × hom(a, b) → hom(a, c)。两个态射f : a → b 及g : b → c 的复合写做g ∘ f 或gf，并会符合下列两个公理：

    • 结合律：若f : a → b、g : b → c及h : c → d，则h ∘ (g ∘ f) = (h ∘ g) ∘ f；
    • 单位元：对任意物件x，总存在一个态射1x : x → x（称为x 的单位态射），使得对每个态射f : a → b，都会有1b ∘ f = f = f ∘ 1a。

    （可以看出每个范畴只会有一个单位元，monad每个物件只会有一个单位态射）

2.Haskell与范畴论

Haskell中存在着这样的一种唯一的范畴Hask其满足我们上面所提到的范畴所满足的所有约定。

1. 物件就是Haskell中的类型，注意Haskell中的类型是一个类，即是一个集合。
2. 态射就是Haskell中的函数（function），如f :: Int -> Bool，函数f就是将Int这个物件的值映射到Bool物件的值上。
3. 态射复合就是Haskell中函数的组合，比如func = f.g。

​ 可以验证符合上面的两条公理。

由于Haskell中只有一个范畴，所以如果存在函子那么必然是映射到自身的自函子，那么Haskell中存不存在自函子呢？

1. 首先要满足第一个条件：存在物件与物件之间的映射。在Haskell中，type constructor可以利用一个typeclass构造出其他的typeclass来，例如以下的定义:

   Tree
   data Tree a = Tip | Node a (Tree a) (Tree a)
   

   这里Node作为一类类型可以构造出Tree这种类型来。

2. 第二个条件：态射与态射之间的映射。我们来看下面这种typeclass

   class Functor f where
     fmap:: (a -> b) -> f a -> f b
   

   typeclass fmap接受一个函数（物件与物件之间的映射），将其映射到另一个函数上（物件与物件的映射），所以说fmap是一个满足“态射与态射之间的映射”的一个typeclass。

3.monads

Monads是自函子范畴上的一个幺半群。

阿里电面（java研发）

1. 从下往上说一下OSI七个分层？

• 物理层、数据链路层、网络层、传输层、会话层、表示层、应用层。

1. TCP和UDP的区别？

   • TCP提供面向连接的、可靠的数据流传输，而UDP提供的是非面向连接的、不可靠的数据流传输。（TCP发出去还会问候核实一下以确保安全; UDP发出去就不管了 ）
   • TCP传输单位称为TCP报文段，UDP传输单位称为用户数据报。
   • TCP注重数据安全性，UDP数据传输快，因为不需要连接等待，少了许多操作，但是其安全性却一般。

2. 说说数据库连接（join）？

   • Inner join–产生的是AB两个集合的交集
   • left[outer]join–产生A的完全集，而B中匹配的则有值，没有匹配的则返回null
   • right[outer]join–产生B的完全集，而A中匹配的则有值，没有匹配的则返回null

3. 说说事务？

   • 所谓事务，它是一个操作序列，这些操作要么都执行，要么都不执行，它是一个不可分割的工作单位。

4. HashMap原理？

   • 底层是数组加链表实现的哈希表。允许null作为键，null作为值。线程不安全。

   • 为什么用数组+链表实现？

     利用拉链法解决冲突：把所有的同义词用单链表链接起来。该方法下，哈希表每个单元中存放的不再是元素本身，而是相应同义词单链表的头指针。

   • HashMap维护了一个Entry数组，Entry内部类有key,value，hash和next四个字段，其中next也是一个Entry类型。可以将Entry数组理解为一个个的散列桶。每一个桶实际上是一个单链表。当执行put操作时，会根据key的hashcode定位到相应的桶。 遍历单链表检查该key是否已经存在，如果存在，覆盖该value，反之，新建一个新的Entry，并放在单链表的头部。当通过传递key调用get方法时，它再次使用key.hashCode()来找到相应的散列桶，然后使用key.equals()方法找出单链表中正确的Entry，然后返回它的值。

   • HashMap：线程不同步。根据key的hashcode进行存储，内部使用静态内部类Node的数组进行存储，默认初始大小为16，每次扩大一倍。当发生Hash冲突时，采用拉链法（链表）。可以接受为null的键值(key)和值(value)。JDK1.8中：当单个桶中元素个数大于等于8时，链表实现改为红黑树实现；当元素个数小于6时，变回链表实现。由此来防止hashCode攻击。

   • Hashtable是线程安全的。ConcurrentHashMap 针对读操作做了大量的优化。通过 HashEntry 对象的不变性和用 volatile 型变量协调线程间的内存可见性，使得 大多数时候，读操作不需要加锁就可以正确获得值。这个特性使得 ConcurrentHashMap 的并发性能在分离锁的基础上又有了近一步的提高。ConcurrentHashMap 的高并发性主要来自于三个方面：

   • 用分离锁实现多个线程间的更深层次的共享访问。

   • 用 HashEntery 对象的不变性来降低执行读操作的线程在遍历链表期间对加锁的需求。
   • 通过对同一个 Volatile 变量的写 / 读访问，协调不同线程间读 / 写操作的内存可见性。

5. Java运行时数据区域？

   • 包括程序计数器、JVM栈、本地方法栈、方法区、堆

6. 方法区里存放什么？

   • 由于程序计数器、JVM栈、本地方法栈3个区域随线程而生随线程而灭，对这几个区域内存的回收和分配具有确定性。 而方法区和堆则不一样，程序需要在运行时才知道创建哪些对象，对这部分内存的分配是动态的，GC关注的也就是这部分内存。

• 本地方法栈：和jvm栈所发挥的作用类似，区别是jvm栈为jvm执行java方法（字节码）服务，而本地方法栈为jvm使用的native方法服务。
• JVM栈：局部变量表、操作数栈、动态链接、方法出口。
  • 方法区：用于存储已被虚拟机加载的类信息，常量、静态变量、即时编译器编译后的代码等。
  • 堆：存放对象实例。

1. 怎样判断是否需要收集？

   • 引用计数法：对象没有任何引用与之关联(无法解决循环引用)
   • 可达性分析法：通过一组称为GC Root的对象为起点,从这些节点向下搜索，如果某对象不能从这些根对象的一个(至少一个)所到达,则判定该对象应当回收。

2. 什么可作为GCRoot的对象？

   • 虚拟机栈中引用的对象。方法区中类静态属性引用的对象，方法区中类常量引用的对象，本地方法栈中JNI引用的对象。

3. Spring IOC/AOP？

• AOP（Aspect-OrientedProgramming，面向方面编程,可以说是OOP（Object-Oriented Programing，面向对象编程）的补充和完善。 OOP引入封装、继承和多态性等概念来建立一种对象层次结构，用以模拟公共行为的一个集合。当我们需要为分散的对象引入公共行为的时候，OOP则显得无能为力。 也就是说，OOP允许你定义从上到下的关系，但并不适合定义从左到右的关系。例如日志功能。日志代码往往水平地散布在所有对象层次中，而与它所散布到的对象的核心功能毫无关系。对于其他类型的代码，如安全性、异常处理和透明的持续性也是如此。这种散布在各处的无关的代码被称为横切（cross-cutting）代码， 在OOP设计中，它导致了大量代码的重复，而不利于各个模块的重用。依赖注入(Dependency Injection)和控制反转(Inversion of Control)是同一个概念.当某个角色(可能是一个Java实例，调用者)需要另一个角色(另一个Java实例，被调用者)的协助时，在传统的程序设计过程中，通常由调用者来创建被调用者的实例.但在Spring里，创建被调用者的工作不再由调用者来完成，因此称为控制反转;创建被调用者实例的工作通常由Spring容器来完成，然后注入调用者，因此也称为依赖注入.不管是依赖注入，还是控制反转，都说明Spring采用动态、灵活的方式来管理各种对象。对象与对象之间的具体实现互相透明。 在理解依赖注入之前，看如下这个问题在各种社会形态里如何解决:一个人(Java实例，调用者)需要一把斧子(Java实例，被调用者)。

1. 自己在应用中写过什么切面？

AOP使用场景：

• Authentication 权限
• Caching 缓存
  • Context passing 内容传递
  • Error handling 错误处理
  • Lazy loading　懒加载
  • Debugging　　调试
  • logging, tracing, profiling and monitoring　记录跟踪　优化　校准
  • Performance optimization　性能优化
  • Persistence　　持久化
  • Resource pooling　资源池
  • Synchronization　同步
  • Transactions 事务

1. JVM如何加载一个类的过程，双亲委派模型中有哪些方法？

   • 加载：定位要加载的类文件，并将其字节流装载到JVM中；
   • 链接：给要加载的类分配最基本的内存结构保存其信息，比如属性，方法以及引用的类。在该阶段，该类还处于不可用状态；验证：对加载的字节流进行验证，比如格式上的，安全方面的；内存分配：为该类准备内存空间来表示其属性，方法以及引用的类；解析：加载该类所引用的其它类，比如父类，实现的接口等。
   • 初始化：对类变量进行赋值。
   • getParent(),findLoadedClass(),LoadClass(),findBootstrapClassOrNull(),findClass(),resolveClass()

2. 进程间通信有哪几种方式？

   | 类型 | 无连接 | 可靠 | 流控制 | 优先级 |
   | ————- | —- | —- | —- | —- |
   | 消息队列 | N | Y | Y | Y |
   | 信号量 | N | Y | Y | Y |
   | 共享内存 | N | Y | Y | Y |
   | UNIX流SOCKET | N | Y | Y | N |
   | UNIX数据包SOCKET | Y | Y | N | N |
   | 普通PIPE | N | Y | Y | N |
   | 流PIPE | N | Y | Y | N |
   | 命名PIPE(FIFO) | N | Y | Y | N |

3. Linux下如何进行进程调度的？

   • 实时进程的调度

     不同调度策略的实时进程只有在相同优先级时才有可比性：

     • 对于FIFO的进程，意味着只有当前进程执行完毕才会轮到其他进程执行。由此可见相当霸道。
     • 对于RR的进程。一旦时间片消耗完毕，则会将该进程置于队列的末尾，然后运行其他相同优先级的进程，如果没有其他相同优先级的进程，则该进程会继续执行。

   • 非实时进程调度

     Linux对普通的进程，根据动态优先级进行调度。而动态优先级是由静态优先级（static_prio）调整而来（考虑了进程的属性）。Linux下，静态优先级是用户不可见的，隐藏在内核中。

   • 现代方法CFS

     不再单纯依靠进程优先级绝对值，而是参考其绝对值，综合考虑所有进程的时间，给出当前调度时间单位内其应有的权重，也就是，每个进程的权重X单位时间=应获cpu时间，但是这个应得的cpu时间不应太小（假设阈值为1ms），否则会因为切换得不偿失。但是，当进程足够多时候，肯定有很多不同权重的进程获得相同的时间——最低阈值1ms，所以，CFS只是近似完全公平。

4. 什么是一致性哈希？

   • 将 Item 均匀地分布（Even Distribution）到不同的 Bucket 中，也就是负载均衡（Load Balancing）。
   • 一致性哈希的实现：
     • 对所有的 Buckets 和 Items 应用相同的哈希函数 H，按照哈希值的顺序把它们排列到一条线上，然后将距离 Bucket 最近的 Items 都放入该 Bucket 中。
     • 另一种实现方式是把哈希值的最大值和最小值连接到一起，形成一个哈希环（Consistent Hashing Ring），按照顺时针方向将 Items 放入 Bucket 中。

5. linux中socket编程，底层实现？

   • 对于应用TCP/IP协议的应用程序，UNIX BSD提供了SOCKET的应用编程接口。
   • socket起源于Unix，而Unix/linux基本哲学之一就是“一切皆文件”，都可以用“打开open –> 读写write/read –> 关闭close”模式来操作。Socket就是该模式的一个实现， socket即是一种特殊的文件，一些socket函数就是对其进行的操作（读/写IO、打开、关闭）.说白了Socket是应用层与TCP/IP协议族通信的中间软件抽象层，它是一组接口。在设计模式中，Socket其实就是一个门面模式，它把复杂的TCP/IP协议族隐藏在Socket接口后面，对用户来说，一组简单的接口就是全部，让Socket去组织数据，以符合指定的协议。
   • 当应用程序要创建一个套接字时，操作系统就返回一个小整数作为描述符，应用程序则使用这个描述符来引用该套接字需要I/O请求的应用程序请求操作系统打开一个文件。操作系统就创建一个文件描述符提供给应用程序访问文件。从应用程序的角度看，文件描述符是一个整数，应用程序可以用它来读写文件。

6. socket连接数目的瓶颈？

   Server的内存

7. java中的软引用，弱引用？

   • 如果一个对象只具有软引用(SoftReference)，则内存空间足够，垃圾回收器就不会回收它；如果内存空间不足了，就会回收这些对象的内存。只要垃圾回收器没有回收它，该对象就可以被程序使用。软引用可用来实现内存敏感的高速缓存。

      String str=new String("abc");                                     // 强引用
      SoftReference<String> softRef=new SoftReference<String>(str);     // 软引用
     

   • 弱引用(WeakReference)与软引用的区别在于：只具有弱引用的对象拥有更短暂的生命周期。在垃圾回收器线程扫描它所管辖的内存区域的过程中，一旦发现了只具有弱引用的对象，不管当前内存空间足够与否，都会回收它的内存。不过，由于垃圾回收器是一个优先级很低的线程，因此不一定会很快发现那些只具有弱引用的对象。

     String str=new String("abc");    
     WeakReference<String> abcWeakRef = new WeakReference<String>(str);
     str=null;
     

8. 了解rpc吗？

   • RPC： 远程过程调用（Remote Procedure Call）
   • 远程过程调用采用客户机/服务器(C/S)模式。请求程序就是一个客户机，而服务提供程序就是一台服务器。和常规或本地过程调用一样，远程过程调用是同步操作，在远程过程结果返回之前，需要暂时中止请求程序。使用相同地址空间的低权进程或低权线程允许同时运行多个远程过程调用。

9. 什么是epoll？

   • epoll是linux内核为处理大批量文件描述符而作了改进的poll，是Linux下多路复用IO接口select/poll的增强版本，它能显著提高程序在大量并发连接中只有少量活跃的情况下的系统CPU利用率。另一点原因就是获取事件的时候，它无须遍历整个被侦听的描述符集，只要遍历那些被内核IO事件异步唤醒而加入Ready队列的描述符集合就行了。
   • 提供了边缘触发（Edge Triggered），这就使得用户空间程序有可能缓存IO状态，减少epoll_wait/epoll_pwait的调用，提高应用程序效率。
   • 优点：
     • 支持一个进程打开大数目的socket描述符
     • IO效率不随FD数目增加而线性下降
     • 使用mmap加速内核与用户空间的消息传递

---

​